:: SCMFSA8C semantic presentation

REAL is non empty V5() V34() V46() set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K32(REAL)
K32(REAL) is set
SCM+FSA is non empty V84(3) IC-Ins-separated strict V92(3) with_explicit_jumps IC-relocable V147(3) AMI-Struct over 3
3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V45() Element of NAT
the carrier of SCM+FSA is non empty set
NAT is non empty epsilon-transitive epsilon-connected ordinal set
K32(NAT) is set
K32(NAT) is set
9 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V45() Element of NAT
Segm 9 is Element of K32(NAT)
Int-Locations is non empty set
K300() is set
K32(K300()) is set
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V45() Element of NAT
K33(K300(),2) is Relation-like set
K32(K33(K300(),2)) is set
K302() is Relation-like K300() -defined 2 -valued Function-like V31(K300(),2) Element of K32(K33(K300(),2))
K303() is non empty Relation-like 2 -defined Function-like total set
K302() * K303() is Relation-like K300() -defined Function-like total set
K263((K302() * K303())) is set
K294() is non empty set
K139(K263((K302() * K303())),K263((K302() * K303()))) is set
K33(K294(),K139(K263((K302() * K303())),K263((K302() * K303())))) is Relation-like set
K32(K33(K294(),K139(K263((K302() * K303())),K263((K302() * K303()))))) is set
K32( the carrier of SCM+FSA) is set
the InstructionsF of SCM+FSA is non empty Relation-like standard-ins V54() J/A-independent V57() set
INT is non empty V5() V34() V46() set
Int-Locations is non empty Element of K32( the carrier of SCM+FSA)
K337(Int-Locations) is V99() set
K32(Int-Locations) is set
FinSeq-Locations is non empty V5() V34() V46() Element of K32( the carrier of SCM+FSA)
K337(FinSeq-Locations) is V99() set
K32(FinSeq-Locations) is set
K274(3,SCM+FSA) is non empty Relation-like non-empty non empty-yielding the carrier of SCM+FSA -defined Function-like total set
the Object-Kind of SCM+FSA is Relation-like the carrier of SCM+FSA -defined 3 -valued Function-like V31( the carrier of SCM+FSA,3) Element of K32(K33( the carrier of SCM+FSA,3))
K33( the carrier of SCM+FSA,3) is Relation-like set
K32(K33( the carrier of SCM+FSA,3)) is set
the U7 of SCM+FSA is non empty Relation-like 3 -defined Function-like total set
the Object-Kind of SCM+FSA * the U7 of SCM+FSA is non empty Relation-like the carrier of SCM+FSA -defined Function-like total set
COMPLEX is non empty V5() V34() V46() set
K406() is non empty V84(2) IC-Ins-separated strict strict V92(2) AMI-Struct over 2
the InstructionsF of K406() is non empty Relation-like standard-ins V54() J/A-independent V57() set
the carrier of K406() is non empty set
K274(2,K406()) is non empty Relation-like non-empty non empty-yielding the carrier of K406() -defined Function-like total set
the Object-Kind of K406() is Relation-like the carrier of K406() -defined 2 -valued Function-like V31( the carrier of K406(),2) Element of K32(K33( the carrier of K406(),2))
K33( the carrier of K406(),2) is Relation-like set
K32(K33( the carrier of K406(),2)) is set
the U7 of K406() is non empty Relation-like 2 -defined Function-like total set
the Object-Kind of K406() * the U7 of K406() is non empty Relation-like the carrier of K406() -defined Function-like total set
RAT is non empty V5() V34() V46() set
K33(NAT,K32(NAT)) is Relation-like set
K32(K33(NAT,K32(NAT))) is set
FinPartSt SCM+FSA is non empty Element of K32(K267(K274(3,SCM+FSA)))
K267(K274(3,SCM+FSA)) is set
K32(K267(K274(3,SCM+FSA))) is set
{ b₁ where b₁ is Element of K267(K274(3,SCM+FSA)) : b₁ is V34() } is set
K33((FinPartSt SCM+FSA),(FinPartSt SCM+FSA)) is Relation-like set
K32(K33((FinPartSt SCM+FSA),(FinPartSt SCM+FSA))) is set
1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V45() Element of NAT
{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() V28() V29() V34() V35() V38() V42() V43() V44() initial Function-yielding V109() set
0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() V28() V29() V34() V35() V38() V42() V43() V44() initial Function-yielding V109() Element of NAT
halt SCM+FSA is ins-loc-free V91(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V146(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
K15(0,{},{}) is set
Stop SCM+FSA is non empty V5() Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like constant T-Sequence-like V34() initial non halt-free V61( SCM+FSA ) V62( SCM+FSA ) keeping_0 good V149(3, SCM+FSA ) paraclosed parahalting set
K221((halt SCM+FSA)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() 1 -element initial set
4 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V45() Element of NAT
goto 2 is non ins-loc-free V58( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V146(3, SCM+FSA ) V148(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
intloc 0 is V95() read-only Element of the carrier of SCM+FSA
5 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V45() Element of NAT
6 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V45() Element of NAT
7 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V45() Element of NAT
10 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V45() Element of NAT
12 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V45() Element of NAT
8 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V45() Element of NAT
IC is V71( SCM+FSA ) Element of the carrier of SCM+FSA
K81(NAT,0,1) is non empty V34() Element of K32(NAT)
(intloc 0) .--> 1 is V5() Relation-like the carrier of SCM+FSA -defined {(intloc 0)} -defined {(intloc 0)} -defined NAT -valued Function-like one-to-one constant K274(3,SCM+FSA) -compatible V34() data-only set
{(intloc 0)} is non empty V34() set
{(intloc 0)} --> 1 is non empty Relation-like non-empty non empty-yielding {(intloc 0)} -defined NAT -valued {1} -valued Function-like constant total V31({(intloc 0)},{1}) V34() Element of K32(K33({(intloc 0)},{1}))
{1} is non empty V34() V45() V46() set
K33({(intloc 0)},{1}) is Relation-like V34() set
K32(K33({(intloc 0)},{1})) is V34() V38() set
Initialize ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible V34() 0 -started set
Start-At (0,SCM+FSA) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible V34() 0 -started set
(IC ) .--> 0 is V5() Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued Function-like one-to-one constant V34() Function-yielding V109() set
{(IC )} is non empty V34() set
{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued {0} -valued Function-like constant total V31({(IC )},{0}) V34() Function-yielding V109() Element of K32(K33({(IC )},{0}))
{0} is non empty functional V34() V38() set
K33({(IC )},{0}) is Relation-like V34() set
K32(K33({(IC )},{0})) is V34() V38() set
((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible V34() 0 -started set
dom (Initialize ((intloc 0) .--> 1)) is V34() set
K81( the carrier of SCM+FSA,(intloc 0),(IC )) is non empty V34() Element of K32( the carrier of SCM+FSA)
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Initialize s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
s +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
P +* a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
dom a is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V34() V45() V126() Element of K32(NAT)
pseudo-LifeSpan (s,P,a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
Comput ((P +* a),(Initialize s),(pseudo-LifeSpan (s,P,a))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput ((P +* a),(Initialize s),(pseudo-LifeSpan (s,P,a)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput ((P +* a),(Initialize s),(pseudo-LifeSpan (s,P,a)))) . (IC ) is set
card a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
dom a is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V34() V45() V126() set
b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
dom P is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V34() V45() V126() set
s is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
card s is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
dom s is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V34() V45() V126() set
(card P) + (card s) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
P ";" s is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
stop P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
K211(P,(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
CutLastLoc (stop P) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
Directed (CutLastLoc (stop P)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() halt-free set
card (CutLastLoc (stop P)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
dom (CutLastLoc (stop P)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V34() V126() set
Directed ((CutLastLoc (stop P)),(card (CutLastLoc (stop P)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() halt-free set
goto (card (CutLastLoc (stop P))) is non ins-loc-free V58( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V146(3, SCM+FSA ) V148(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(CutLastLoc (stop P)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop P))))) is Relation-like Function-like set
Reloc (s,(card P)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() set
IncAddr (s,(card P)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
K500((IncAddr (s,(card P))),(card P)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() set
(Directed (CutLastLoc (stop P))) +* (Reloc (s,(card P))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() set
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
a -' (card P) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
s . (a -' (card P)) is set
(P ";" s) . a is set
(card s) + (card P) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
a + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
a - (card P) is ext-real V27() V28() V29() set
(card s) - 0 is ext-real non negative V27() V28() V29() set
dom s is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V34() V45() V126() Element of K32(NAT)
b is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr (b,(card P)) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(a -' (card P)) + (card P) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(a - (card P)) + (card P) is ext-real V27() V28() V29() set
{ (b₁ + (card P)) where b₁ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT : b₁ in dom s } is set
dom (Reloc (s,(card P))) is V34() V126() set
(Reloc (s,(card P))) . a is set
a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
IExec (a,P,s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
P +* a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialized s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
Result ((P +* a),(Initialized s)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IExec (a,P,(Initialized s)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Initialized (Initialized s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
(Initialized s) +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
Result ((P +* a),(Initialized (Initialized s))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
s +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a +* P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialized s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
Initialize (Initialized s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
(Initialized s) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
{0,6,7,8} is V34() set
P is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
DataPart P is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
NonZero SCM+FSA is Element of K32( the carrier of SCM+FSA)
P | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
s is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
InsCode s is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
Exec (s,P) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like V31( the InstructionsF of SCM+FSA,K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K141( the InstructionsF of SCM+FSA,K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,s) is Element of K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K141( the InstructionsF of SCM+FSA,K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,s) . P is set
DataPart (Exec (s,P)) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Exec (s,P)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
a is V95() Element of the carrier of SCM+FSA
(Exec (s,P)) . a is ext-real V27() V28() V29() set
P . a is ext-real V27() V28() V29() set
b is FinSeq-Location
(Exec (s,P)) . b is Relation-like NAT -defined INT -valued Function-like V34() V42() V43() M7( INT )
P . b is Relation-like NAT -defined INT -valued Function-like V34() V42() V43() M7( INT )
a is V95() Element of the carrier of SCM+FSA
(Exec (s,P)) . a is ext-real V27() V28() V29() set
P . a is ext-real V27() V28() V29() set
b is FinSeq-Location
(Exec (s,P)) . b is Relation-like NAT -defined INT -valued Function-like V34() V42() V43() M7( INT )
P . b is Relation-like NAT -defined INT -valued Function-like V34() V42() V43() M7( INT )
c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
goto c is non ins-loc-free V58( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V146(3, SCM+FSA ) V148(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
a is V95() Element of the carrier of SCM+FSA
(Exec (s,P)) . a is ext-real V27() V28() V29() set
P . a is ext-real V27() V28() V29() set
b is FinSeq-Location
(Exec (s,P)) . b is Relation-like NAT -defined INT -valued Function-like V34() V42() V43() M7( INT )
P . b is Relation-like NAT -defined INT -valued Function-like V34() V42() V43() M7( INT )
c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
I2 is V95() Element of the carrier of SCM+FSA
I2 =0_goto c is non ins-loc-free V58( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V146(3, SCM+FSA ) V148(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
a is V95() Element of the carrier of SCM+FSA
(Exec (s,P)) . a is ext-real V27() V28() V29() set
P . a is ext-real V27() V28() V29() set
b is FinSeq-Location
(Exec (s,P)) . b is Relation-like NAT -defined INT -valued Function-like V34() V42() V43() M7( INT )
P . b is Relation-like NAT -defined INT -valued Function-like V34() V42() V43() M7( INT )
c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
I2 is V95() Element of the carrier of SCM+FSA
I2 >0_goto c is non ins-loc-free V58( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V146(3, SCM+FSA ) V148(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IExec ((Stop SCM+FSA),P,s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
P +* (Stop SCM+FSA) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like total non halt-free set
Initialized s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
Result ((P +* (Stop SCM+FSA)),(Initialized s)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
NonZero SCM+FSA is Element of K32( the carrier of SCM+FSA)
Initialize (Initialized s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
(Initialized s) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
Comput ((P +* (Stop SCM+FSA)),(Initialize (Initialized s)),0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Initialize (Initialized s)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Initialize (Initialized s)) . (IC ) is set
(P +* (Stop SCM+FSA)) /. (IC (Initialize (Initialized s))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(P +* (Stop SCM+FSA)) . (IC (Initialize (Initialized s))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Stop SCM+FSA) . 0 is set
dom (Stop SCM+FSA) is non empty V5() ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V34() V45() V126() Element of K32(NAT)
CurInstr ((P +* (Stop SCM+FSA)),(Initialize (Initialized s))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(P +* (Stop SCM+FSA)) . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
DataPart (IExec ((Stop SCM+FSA),P,s)) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(IExec ((Stop SCM+FSA),P,s)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
DataPart (Initialize (Initialized s)) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Initialize (Initialized s)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
DataPart (Initialized s) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Initialized s) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
I2 is set
dom (IExec ((Stop SCM+FSA),P,s)) is non empty set
(IExec ((Stop SCM+FSA),P,s)) . I2 is set
(Initialized s) . I2 is set
(IExec ((Stop SCM+FSA),P,s)) . I2 is set
(Initialized s) . I2 is set
dom (Start-At (0,SCM+FSA)) is non empty V34() set
(IExec ((Stop SCM+FSA),P,s)) . I2 is set
(Start-At (0,SCM+FSA)) . (IC ) is set
s +* ((intloc 0) .--> 1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
(s +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
((s +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) . I2 is set
(s +* (Initialize ((intloc 0) .--> 1))) . I2 is set
(Initialized s) . I2 is set
dom (Initialized s) is non empty set
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
dom a is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V34() V45() V126() Element of K32(NAT)
P +* a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialize s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
s +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
Comput ((P +* a),(Initialize s),0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput ((P +* a),(Initialize s),0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput ((P +* a),(Initialize s),0)) . (IC ) is set
b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
DataPart a is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
NonZero SCM+FSA is Element of K32( the carrier of SCM+FSA)
a | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
b is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
b . (IC ) is set
DataPart b is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
b | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
c is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
dom c is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V34() V45() V126() Element of K32(NAT)
Initialize a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
a +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
dom (Start-At (0,SCM+FSA)) is non empty V34() set
IC a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
a . (IC ) is set
P . (IC a) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
c . 0 is set
P +* c is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Comput (P,a,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (P,a,0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (P,a,0)) . (IC ) is set
IC (Start-At (0,SCM+FSA)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Start-At (0,SCM+FSA)) . (IC ) is set
I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
Reloc (c,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() set
IncAddr (c,I) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
K500((IncAddr (c,I)),I) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() set
D is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
Comput (P,a,D) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (P,a,D)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (P,a,D)) . (IC ) is set
(IC (Comput (P,a,D))) + I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
Comput (s,b,D) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (s,b,D)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (s,b,D)) . (IC ) is set
CurInstr (P,(Comput (P,a,D))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P /. (IC (Comput (P,a,D))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (P,(Comput (P,a,D)))),I) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (s,(Comput (s,b,D))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s /. (IC (Comput (s,b,D))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
DataPart (Comput (P,a,D)) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Comput (P,a,D)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
DataPart (Comput (s,b,D)) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Comput (s,b,D)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
DataPart (Comput (P,a,0)) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Comput (P,a,0)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
Comput (s,b,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
DataPart (Comput (s,b,0)) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Comput (s,b,0)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
sa is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
Comput (P,a,sa) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (P,a,sa)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (P,a,sa)) . (IC ) is set
(IC (Comput (P,a,sa))) + I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
Comput (s,b,sa) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (s,b,sa)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (s,b,sa)) . (IC ) is set
CurInstr (P,(Comput (P,a,sa))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P /. (IC (Comput (P,a,sa))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (P,(Comput (P,a,sa)))),I) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (s,(Comput (s,b,sa))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s /. (IC (Comput (s,b,sa))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
DataPart (Comput (P,a,sa)) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Comput (P,a,sa)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
DataPart (Comput (s,b,sa)) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Comput (s,b,sa)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
sa + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V45() Element of NAT
Comput (P,a,(sa + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (P,a,(sa + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (P,a,(sa + 1))) . (IC ) is set
(IC (Comput (P,a,(sa + 1)))) + I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
Comput (s,b,(sa + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (s,b,(sa + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (s,b,(sa + 1))) . (IC ) is set
CurInstr (P,(Comput (P,a,(sa + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P /. (IC (Comput (P,a,(sa + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (P,(Comput (P,a,(sa + 1))))),I) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (s,(Comput (s,b,(sa + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s /. (IC (Comput (s,b,(sa + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
DataPart (Comput (P,a,(sa + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Comput (P,a,(sa + 1))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
DataPart (Comput (s,b,(sa + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Comput (s,b,(sa + 1))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
Following (P,(Comput (P,a,sa))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P,(Comput (P,a,sa)))),(Comput (P,a,sa))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like V31( the InstructionsF of SCM+FSA,K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K141( the InstructionsF of SCM+FSA,K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P,(Comput (P,a,sa))))) is Element of K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K141( the InstructionsF of SCM+FSA,K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P,(Comput (P,a,sa))))) . (Comput (P,a,sa)) is set
Following (s,(Comput (s,b,sa))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Exec ((CurInstr (s,(Comput (s,b,sa)))),(Comput (s,b,sa))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
K141( the InstructionsF of SCM+FSA,K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (s,(Comput (s,b,sa))))) is Element of K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K141( the InstructionsF of SCM+FSA,K139(K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K263(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (s,(Comput (s,b,sa))))) . (Comput (s,b,sa)) is set
dom (Reloc (c,I)) is V34() V126() set
s is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
s0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P . (IC (Comput (P,a,(sa + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
c . s is set
s + I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Reloc (c,I)) . (s + I) is set
s . (IC (Comput (s,b,(sa + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
0 + I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
dom (Reloc (c,I)) is V34() V126() set
P /. (IC a) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s /. (IC b) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s . (IC b) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (P,(Comput (P,a,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P /. (IC (Comput (P,a,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (P,(Comput (P,a,0)))),I) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Reloc (c,I)) . (0 + I) is set
CurInstr (s,(Comput (s,b,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (s,b,0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (s,b,0)) . (IC ) is set
s /. (IC (Comput (s,b,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(IC (Comput (P,a,0))) + I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
DataPart a is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
NonZero SCM+FSA is Element of K32( the carrier of SCM+FSA)
a | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
b is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
DataPart b is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
b | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
c is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
Reloc (c,0) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() set
IncAddr (c,0) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
K500((IncAddr (c,0)),0) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() set
I2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
Comput (P,a,I2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (P,a,I2)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (P,a,I2)) . (IC ) is set
Comput (s,b,I2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (s,b,I2)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (s,b,I2)) . (IC ) is set
CurInstr (P,(Comput (P,a,I2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P /. (IC (Comput (P,a,I2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (s,(Comput (s,b,I2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s /. (IC (Comput (s,b,I2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
DataPart (Comput (P,a,I2)) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Comput (P,a,I2)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
DataPart (Comput (s,b,I2)) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Comput (s,b,I2)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
dom (Start-At (0,SCM+FSA)) is non empty V34() set
(IC (Comput (P,a,I2))) + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
IC b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
b . (IC ) is set
Initialize b is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
b +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
IC (Initialize b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Initialize b) . (IC ) is set
IC (Start-At (0,SCM+FSA)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Start-At (0,SCM+FSA)) . (IC ) is set
IncAddr ((CurInstr (P,(Comput (P,a,I2)))),0) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
DataPart a is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
NonZero SCM+FSA is Element of K32( the carrier of SCM+FSA)
a | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
b is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
DataPart b is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
b | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
LifeSpan (P,a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
LifeSpan (s,b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
c is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
P +* c is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialize a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
a +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
I2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
Comput (s,b,I2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
CurInstr (s,(Comput (s,b,I2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (s,b,I2)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (s,b,I2)) . (IC ) is set
s /. (IC (Comput (s,b,I2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (P,a,I2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
CurInstr (P,(Comput (P,a,I2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (P,a,I2)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (P,a,I2)) . (IC ) is set
P /. (IC (Comput (P,a,I2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (P,a,(LifeSpan (P,a))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
CurInstr (P,(Comput (P,a,(LifeSpan (P,a))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (P,a,(LifeSpan (P,a)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (P,a,(LifeSpan (P,a)))) . (IC ) is set
P /. (IC (Comput (P,a,(LifeSpan (P,a))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (s,b,(LifeSpan (P,a))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
CurInstr (s,(Comput (s,b,(LifeSpan (P,a))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (s,b,(LifeSpan (P,a)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (s,b,(LifeSpan (P,a)))) . (IC ) is set
s /. (IC (Comput (s,b,(LifeSpan (P,a))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
a . (intloc 0) is ext-real V27() V28() V29() set
b is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
NonZero SCM+FSA is Element of K32( the carrier of SCM+FSA)
I2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
IExec (I2,P,a) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
P +* I2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialized a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
a +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
Result ((P +* I2),(Initialized a)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
DataPart (IExec (I2,P,a)) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(IExec (I2,P,a)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
IExec (I2,s,b) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
s +* I2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialized b is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
b +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
Result ((s +* I2),(Initialized b)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
DataPart (IExec (I2,s,b)) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(IExec (I2,s,b)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
Initialize a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
a +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
DataPart (Initialized a) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Initialized a) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
DataPart a is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
a | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
s0 is V95() non read-only Element of the carrier of SCM+FSA
(Initialized a) . s0 is ext-real V27() V28() V29() set
a . s0 is ext-real V27() V28() V29() set
b . s0 is ext-real V27() V28() V29() set
(Initialized b) . s0 is ext-real V27() V28() V29() set
s0 is FinSeq-Location
(Initialized a) . s0 is Relation-like NAT -defined INT -valued Function-like V34() V42() V43() M7( INT )
a . s0 is Relation-like NAT -defined INT -valued Function-like V34() V42() V43() M7( INT )
b . s0 is Relation-like NAT -defined INT -valued Function-like V34() V42() V43() M7( INT )
(Initialized b) . s0 is Relation-like NAT -defined INT -valued Function-like V34() V42() V43() M7( INT )
(Initialized a) . (intloc 0) is ext-real V27() V28() V29() set
(Initialize ((intloc 0) .--> 1)) . (intloc 0) is set
(Initialized b) . (intloc 0) is ext-real V27() V28() V29() set
DataPart (Initialized b) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Initialized b) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
LifeSpan ((P +* I2),(Initialized a)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
Comput ((P +* I2),(Initialized a),(LifeSpan ((P +* I2),(Initialized a)))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
CurInstr ((P +* I2),(Comput ((P +* I2),(Initialized a),(LifeSpan ((P +* I2),(Initialized a)))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((P +* I2),(Initialized a),(LifeSpan ((P +* I2),(Initialized a))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput ((P +* I2),(Initialized a),(LifeSpan ((P +* I2),(Initialized a))))) . (IC ) is set
(P +* I2) /. (IC (Comput ((P +* I2),(Initialized a),(LifeSpan ((P +* I2),(Initialized a)))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput ((s +* I2),(Initialized b),(LifeSpan ((P +* I2),(Initialized a)))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
CurInstr ((s +* I2),(Comput ((s +* I2),(Initialized b),(LifeSpan ((P +* I2),(Initialized a)))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((s +* I2),(Initialized b),(LifeSpan ((P +* I2),(Initialized a))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput ((s +* I2),(Initialized b),(LifeSpan ((P +* I2),(Initialized a))))) . (IC ) is set
(s +* I2) /. (IC (Comput ((s +* I2),(Initialized b),(LifeSpan ((P +* I2),(Initialized a)))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
LifeSpan ((s +* I2),(Initialized b)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
DataPart (Result ((P +* I2),(Initialized a))) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Result ((P +* I2),(Initialized a))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
DataPart (Comput ((P +* I2),(Initialized a),(LifeSpan ((P +* I2),(Initialized a))))) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Comput ((P +* I2),(Initialized a),(LifeSpan ((P +* I2),(Initialized a))))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
DataPart (Comput ((s +* I2),(Initialized b),(LifeSpan ((P +* I2),(Initialized a))))) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Comput ((s +* I2),(Initialized b),(LifeSpan ((P +* I2),(Initialized a))))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
DataPart (Result ((s +* I2),(Initialized b))) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Result ((s +* I2),(Initialized b))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
a . (intloc 0) is ext-real V27() V28() V29() set
DataPart a is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
NonZero SCM+FSA is Element of K32( the carrier of SCM+FSA)
a | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
b is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
DataPart b is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
b | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
I2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
IExec (I2,P,a) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
P +* I2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialized a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
a +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
Result ((P +* I2),(Initialized a)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
DataPart (IExec (I2,P,a)) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(IExec (I2,P,a)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
IExec (I2,s,b) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
s +* I2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialized b is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
b +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
Result ((s +* I2),(Initialized b)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
DataPart (IExec (I2,s,b)) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(IExec (I2,s,b)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
Initialize a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
a +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
DataPart (Initialized a) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Initialized a) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
b . (intloc 0) is ext-real V27() V28() V29() set
Initialize b is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
b +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
DataPart (Initialized b) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Initialized b) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
LifeSpan ((P +* I2),(Initialized a)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
Comput ((P +* I2),(Initialized a),(LifeSpan ((P +* I2),(Initialized a)))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
CurInstr ((P +* I2),(Comput ((P +* I2),(Initialized a),(LifeSpan ((P +* I2),(Initialized a)))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((P +* I2),(Initialized a),(LifeSpan ((P +* I2),(Initialized a))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput ((P +* I2),(Initialized a),(LifeSpan ((P +* I2),(Initialized a))))) . (IC ) is set
(P +* I2) /. (IC (Comput ((P +* I2),(Initialized a),(LifeSpan ((P +* I2),(Initialized a)))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput ((s +* I2),(Initialized b),(LifeSpan ((P +* I2),(Initialized a)))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
CurInstr ((s +* I2),(Comput ((s +* I2),(Initialized b),(LifeSpan ((P +* I2),(Initialized a)))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((s +* I2),(Initialized b),(LifeSpan ((P +* I2),(Initialized a))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput ((s +* I2),(Initialized b),(LifeSpan ((P +* I2),(Initialized a))))) . (IC ) is set
(s +* I2) /. (IC (Comput ((s +* I2),(Initialized b),(LifeSpan ((P +* I2),(Initialized a)))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
LifeSpan ((s +* I2),(Initialized b)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
DataPart (Result ((P +* I2),(Initialized a))) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Result ((P +* I2),(Initialized a))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
DataPart (Comput ((P +* I2),(Initialized a),(LifeSpan ((P +* I2),(Initialized a))))) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Comput ((P +* I2),(Initialized a),(LifeSpan ((P +* I2),(Initialized a))))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
DataPart (Comput ((s +* I2),(Initialized b),(LifeSpan ((P +* I2),(Initialized a))))) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Comput ((s +* I2),(Initialized b),(LifeSpan ((P +* I2),(Initialized a))))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
DataPart (Result ((s +* I2),(Initialized b))) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
(Result ((s +* I2),(Initialized b))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Initialize s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
s +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V34() initial set
P +* a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
pseudo-LifeSpan (s,P,a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
pseudo-LifeSpan ((Initialize s),(P +* a),a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
Initialize (Initialize s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
(Initialize s) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
(P +* a) +* a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
dom a is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V34() V45() V126() Element of K32(NAT)
I2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
Comput (((P +* a) +* a),(Initialize (Initialize s)),I2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (((P +* a) +* a),(Initialize (Initialize s)),I2)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (((P +* a) +* a),(Initialize (Initialize s)),I2)) . (IC ) is set
I2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
Comput (((P +* a) +* a),(Initialize (Initialize s)),I2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (((P +* a) +* a),(Initialize (Initialize s)),I2)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (((P +* a) +* a),(Initialize (Initialize s)),I2)) . (IC ) is set
Comput (((P +* a) +* a),(Initialize (Initialize s)),(pseudo-LifeSpan (s,P,a))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (((P +* a) +* a),(Initialize (Initialize s)),(pseudo-LifeSpan (s,P,a)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
(Comput (((P +* a) +* a),(Initialize (Initialize s)),(pseudo-LifeSpan (s,P,a)))) . (IC ) is set
card a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
dom a is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() V34() V45() V126() set
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
DataPart a is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
NonZero SCM+FSA is Element of K32( the carrier of SCM+FSA)
a | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible set
b is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V29() Element of NAT
b . (IC ) is set
DataPart b is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible data-only set
b | (NonZero SCM+FSA) is