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

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

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