:: SCMFSA8B semantic presentation

REAL is non empty V5() V35() V47() set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K32(REAL)

K32(REAL) is set

SCM+FSA is non empty V85(3) IC-Ins-separated strict V93(3) with_explicit_jumps IC-relocable V145(3) AMI-Struct over 3

3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer V46() Element of NAT

the carrier of SCM+FSA is non empty set

COMPLEX is non empty V5() V35() V47() 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() V32() integer V46() Element of NAT

Segm 9 is Element of K32(NAT)

Int-Locations is non empty set

K321() is set

K32(K321()) is set

2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer V46() Element of NAT

K33(K321(),2) is Relation-like set

K32(K33(K321(),2)) is set

K323() is Relation-like K321() -defined 2 -valued Function-like V29(K321(),2) Element of K32(K33(K321(),2))

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

K323() * K324() is Relation-like K321() -defined Function-like set

K284((K323() * K324())) is set

K315() is non empty set

K122(K284((K323() * K324())),K284((K323() * K324()))) is set

K33(K315(),K122(K284((K323() * K324())),K284((K323() * K324())))) is Relation-like set

K32(K33(K315(),K122(K284((K323() * K324())),K284((K323() * K324()))))) is set

K32( the carrier of SCM+FSA) is set

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

INT is non empty V5() V35() V47() set

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

K358(Int-Locations) is V100() set

K32(Int-Locations) is set

FinSeq-Locations is non empty V5() V35() V47() Element of K32( the carrier of SCM+FSA)

K358(FinSeq-Locations) is V100() set

K32(FinSeq-Locations) is set

K295(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 V29( 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 Relation-like the carrier of SCM+FSA -defined Function-like set

RAT is non empty V5() V35() V47() 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(K288(K295(3,SCM+FSA)))

K288(K295(3,SCM+FSA)) is set

K32(K288(K295(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() V32() integer V46() 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() V32() integer V35() V36() V39() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V151() 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() V32() integer V35() V36() V39() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V151() Element of NAT

12 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer V46() Element of NAT

4 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer V46() Element of NAT

5 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer V46() Element of NAT

6 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer V46() Element of NAT

7 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer V46() Element of NAT

8 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer V46() Element of NAT

10 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer V46() Element of NAT

11 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer V46() Element of NAT

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

the ZeroF of SCM+FSA is Element of the carrier of SCM+FSA

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

goto 2 is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V144(3, SCM+FSA ) V146(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

Stop SCM+FSA is non empty V5() Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant V35() V53() non halt-free V62( SCM+FSA ) V63( SCM+FSA ) V147(3, SCM+FSA ) paraclosed set

K242((halt SCM+FSA)) is set

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

(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 K295(3,SCM+FSA) -compatible V35() data-only set

{(intloc 0)} is non empty V35() 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 V29({(intloc 0)},{1}) V35() Element of K32(K33({(intloc 0)},{1}))

{1} is non empty V35() V46() V47() set

K33({(intloc 0)},{1}) is Relation-like V35() set

K32(K33({(intloc 0)},{1})) is V35() V39() set

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

Start-At (0,SCM+FSA) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible V35() 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 V35() Function-yielding V151() set

{(IC )} is non empty V35() set

{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued {0} -valued Function-like constant total V29({(IC )},{0}) V35() Function-yielding V151() Element of K32(K33({(IC )},{0}))

{0} is non empty functional V35() V39() set

K33({(IC )},{0}) is Relation-like V35() set

K32(K33({(IC )},{0})) is V35() V39() 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 K295(3,SCM+FSA) -compatible K295(3,SCM+FSA) -compatible V35() 0 -started set

K81(NAT,0,1) is non empty V35() Element of K32(NAT)

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

K81( the carrier of SCM+FSA,(intloc 0),(IC )) is non empty V35() Element of K32( the carrier of SCM+FSA)

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

[#] SCM+FSA is non empty non proper Element of K32( the carrier of SCM+FSA)

([#] SCM+FSA) \ {(IC )} is Element of K32( the carrier of SCM+FSA)

s is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

Reloc (s,(card P)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

IncAddr (s,(card P)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

K441((IncAddr (s,(card P))),(card P)) is Relation-like Function-like set

P ";" s is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

K271(SCM+FSA,P) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

K232(P,(Stop SCM+FSA)) is Relation-like Function-like T-Sequence-like set

K443(K271(SCM+FSA,P)) is Relation-like Function-like set

Directed K443(K271(SCM+FSA,P)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

(Directed K443(K271(SCM+FSA,P))) +* (Reloc (s,(card P))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() 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 V35() V53() set

dom s is non empty V35() set

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

dom (Start-At (0,SCM+FSA)) is non empty V35() set

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

Initialize I is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total 0 -started set

I +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible K295(3,SCM+FSA) -compatible total 0 -started set

Comput ((P +* s),(Initialize I),0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput ((P +* s),(Initialize I),0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((P +* s),(Initialize I),0)) . (IC ) is set

(Initialize I) . (IC ) is set

IC (Start-At (0,SCM+FSA)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Start-At (0,SCM+FSA)) . (IC ) is 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

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

DataPart I is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

I | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible set

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

DataPart J is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

J | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible set

a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

Initialize I is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total 0 -started set

I +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible K295(3,SCM+FSA) -compatible total 0 -started set

Initialize J is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total 0 -started set

J +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible K295(3,SCM+FSA) -compatible total 0 -started set

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

Comput ((P +* a),(Initialize I),0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

DataPart (Comput ((P +* a),(Initialize I),0)) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput ((P +* a),(Initialize I),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 K295(3,SCM+FSA) -compatible set

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

Comput ((s +* a),(Initialize J),0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

DataPart (Comput ((s +* a),(Initialize J),0)) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput ((s +* a),(Initialize J),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 K295(3,SCM+FSA) -compatible set

dom a is non empty V35() set

II is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

II + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer V46() Element of NAT

Comput ((s +* a),(Initialize J),(II + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

Comput ((s +* a),(Initialize J),II) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

Following ((s +* a),(Comput ((s +* a),(Initialize J),II))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

CurInstr ((s +* a),(Comput ((s +* a),(Initialize J),II))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IC (Comput ((s +* a),(Initialize J),II)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((s +* a),(Initialize J),II)) . (IC ) is set

(s +* a) /. (IC (Comput ((s +* a),(Initialize J),II))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

Exec ((CurInstr ((s +* a),(Comput ((s +* a),(Initialize J),II)))),(Comput ((s +* a),(Initialize J),II))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set

K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( 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 K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like V29( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))

K33( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set

K32(K33( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set

K124( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((s +* a),(Comput ((s +* a),(Initialize J),II))))) is Element of K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

K124( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((s +* a),(Comput ((s +* a),(Initialize J),II))))) . (Comput ((s +* a),(Initialize J),II)) is Relation-like Function-like set

Comput ((P +* a),(Initialize I),II) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput ((P +* a),(Initialize I),II)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((P +* a),(Initialize I),II)) . (IC ) is set

CurInstr ((P +* a),(Comput ((P +* a),(Initialize I),II))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(P +* a) /. (IC (Comput ((P +* a),(Initialize I),II))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

DataPart (Comput ((P +* a),(Initialize I),II)) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput ((P +* a),(Initialize I),II)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible set

DataPart (Comput ((s +* a),(Initialize J),II)) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput ((s +* a),(Initialize J),II)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible set

i is FinSeq-Location

(Comput ((P +* a),(Initialize I),II)) . i is Relation-like NAT -defined INT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of INT

(Comput ((s +* a),(Initialize J),II)) . i is Relation-like NAT -defined INT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of INT

i is V96() Element of the carrier of SCM+FSA

(Comput ((P +* a),(Initialize I),II)) . i is ext-real V27() V32() integer set

(Comput ((s +* a),(Initialize J),II)) . i is ext-real V27() V32() integer set

Comput ((P +* a),(Initialize I),(II + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput ((P +* a),(Initialize I),(II + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((P +* a),(Initialize I),(II + 1))) . (IC ) is set

Following ((P +* a),(Comput ((P +* a),(Initialize I),II))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

Exec ((CurInstr ((P +* a),(Comput ((P +* a),(Initialize I),II)))),(Comput ((P +* a),(Initialize I),II))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

K124( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* a),(Comput ((P +* a),(Initialize I),II))))) is Element of K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

K124( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* a),(Comput ((P +* a),(Initialize I),II))))) . (Comput ((P +* a),(Initialize I),II)) is Relation-like Function-like set

IC (Comput ((s +* a),(Initialize J),(II + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((s +* a),(Initialize J),(II + 1))) . (IC ) is set

(P +* a) /. (IC (Comput ((P +* a),(Initialize I),(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(P +* a) . (IC (Comput ((P +* a),(Initialize I),(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(s +* a) /. (IC (Comput ((s +* a),(Initialize J),(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(s +* a) . (IC (Comput ((s +* a),(Initialize J),(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

CurInstr ((P +* a),(Comput ((P +* a),(Initialize I),(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

a . (IC (Comput ((P +* a),(Initialize I),(II + 1)))) is set

CurInstr ((s +* a),(Comput ((s +* a),(Initialize J),(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

DataPart (Comput ((P +* a),(Initialize I),(II + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput ((P +* a),(Initialize I),(II + 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 K295(3,SCM+FSA) -compatible set

DataPart (Comput ((s +* a),(Initialize J),(II + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput ((s +* a),(Initialize J),(II + 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 K295(3,SCM+FSA) -compatible set

IC (Comput ((P +* a),(Initialize I),0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((P +* a),(Initialize I),0)) . (IC ) is set

(P +* a) /. (IC (Comput ((P +* a),(Initialize I),0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(P +* a) . (IC (Comput ((P +* a),(Initialize I),0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IC (Comput ((s +* a),(Initialize J),0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((s +* a),(Initialize J),0)) . (IC ) is set

(s +* a) /. (IC (Comput ((s +* a),(Initialize J),0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(s +* a) . (IC (Comput ((s +* a),(Initialize J),0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

dom (Start-At (0,SCM+FSA)) is non empty V35() set

IC (Start-At (0,SCM+FSA)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Start-At (0,SCM+FSA)) . (IC ) is set

CurInstr ((P +* a),(Comput ((P +* a),(Initialize I),0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

a . 0 is set

CurInstr ((s +* a),(Comput ((s +* a),(Initialize J),0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

II is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

Comput ((P +* a),(Initialize I),II) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput ((P +* a),(Initialize I),II)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((P +* a),(Initialize I),II)) . (IC ) is set

Comput ((s +* a),(Initialize J),II) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput ((s +* a),(Initialize J),II)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((s +* a),(Initialize J),II)) . (IC ) is set

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

DataPart P is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

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 K295(3,SCM+FSA) -compatible set

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

DataPart s is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

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 K295(3,SCM+FSA) -compatible set

Initialize P is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total 0 -started set

P +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible K295(3,SCM+FSA) -compatible total 0 -started set

Initialize s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(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 K295(3,SCM+FSA) -compatible K295(3,SCM+FSA) -compatible total 0 -started 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

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

DataPart I is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

I | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible set

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

DataPart J is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

J | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible set

a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

Initialize I is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total 0 -started set

I +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible K295(3,SCM+FSA) -compatible total 0 -started set

Initialize J is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total 0 -started set

J +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible K295(3,SCM+FSA) -compatible total 0 -started set

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

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

dom (Start-At (0,SCM+FSA)) is non empty V35() set

Comput ((P +* a),(Initialize I),0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput ((P +* a),(Initialize I),0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((P +* a),(Initialize I),0)) . (IC ) is set

IC (Start-At (0,SCM+FSA)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Start-At (0,SCM+FSA)) . (IC ) is set

Comput ((s +* a),(Initialize J),0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput ((s +* a),(Initialize J),0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((s +* a),(Initialize J),0)) . (IC ) is set

II is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

II + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer V46() Element of NAT

Comput ((s +* a),(Initialize J),(II + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

Comput ((s +* a),(Initialize J),II) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

Following ((s +* a),(Comput ((s +* a),(Initialize J),II))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

CurInstr ((s +* a),(Comput ((s +* a),(Initialize J),II))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IC (Comput ((s +* a),(Initialize J),II)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((s +* a),(Initialize J),II)) . (IC ) is set

(s +* a) /. (IC (Comput ((s +* a),(Initialize J),II))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

Exec ((CurInstr ((s +* a),(Comput ((s +* a),(Initialize J),II)))),(Comput ((s +* a),(Initialize J),II))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set

K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( 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 K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like V29( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))

K33( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set

K32(K33( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set

K124( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((s +* a),(Comput ((s +* a),(Initialize J),II))))) is Element of K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

K124( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((s +* a),(Comput ((s +* a),(Initialize J),II))))) . (Comput ((s +* a),(Initialize J),II)) is Relation-like Function-like set

Comput ((P +* a),(Initialize I),II) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput ((P +* a),(Initialize I),II)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((P +* a),(Initialize I),II)) . (IC ) is set

CurInstr ((P +* a),(Comput ((P +* a),(Initialize I),II))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(P +* a) /. (IC (Comput ((P +* a),(Initialize I),II))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

DataPart (Comput ((P +* a),(Initialize I),II)) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput ((P +* a),(Initialize I),II)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible set

DataPart (Comput ((s +* a),(Initialize J),II)) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput ((s +* a),(Initialize J),II)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible set

i is FinSeq-Location

(Comput ((P +* a),(Initialize I),II)) . i is Relation-like NAT -defined INT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of INT

(Comput ((s +* a),(Initialize J),II)) . i is Relation-like NAT -defined INT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of INT

i is V96() Element of the carrier of SCM+FSA

(Comput ((P +* a),(Initialize I),II)) . i is ext-real V27() V32() integer set

(Comput ((s +* a),(Initialize J),II)) . i is ext-real V27() V32() integer set

Comput ((P +* a),(Initialize I),(II + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput ((P +* a),(Initialize I),(II + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((P +* a),(Initialize I),(II + 1))) . (IC ) is set

dom a is non empty V35() set

Following ((P +* a),(Comput ((P +* a),(Initialize I),II))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

Exec ((CurInstr ((P +* a),(Comput ((P +* a),(Initialize I),II)))),(Comput ((P +* a),(Initialize I),II))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

K124( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* a),(Comput ((P +* a),(Initialize I),II))))) is Element of K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

K124( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* a),(Comput ((P +* a),(Initialize I),II))))) . (Comput ((P +* a),(Initialize I),II)) is Relation-like Function-like set

IC (Comput ((s +* a),(Initialize J),(II + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((s +* a),(Initialize J),(II + 1))) . (IC ) is set

(P +* a) /. (IC (Comput ((P +* a),(Initialize I),(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(P +* a) . (IC (Comput ((P +* a),(Initialize I),(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(s +* a) /. (IC (Comput ((s +* a),(Initialize J),(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(s +* a) . (IC (Comput ((s +* a),(Initialize J),(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

CurInstr ((P +* a),(Comput ((P +* a),(Initialize I),(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

a . (IC (Comput ((P +* a),(Initialize I),(II + 1)))) is set

CurInstr ((s +* a),(Comput ((s +* a),(Initialize J),(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

DataPart (Comput ((P +* a),(Initialize I),(II + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput ((P +* a),(Initialize I),(II + 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 K295(3,SCM+FSA) -compatible set

DataPart (Comput ((s +* a),(Initialize J),(II + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput ((s +* a),(Initialize J),(II + 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 K295(3,SCM+FSA) -compatible set

II is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

Comput ((P +* a),(Initialize I),II) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

CurInstr ((P +* a),(Comput ((P +* a),(Initialize I),II))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IC (Comput ((P +* a),(Initialize I),II)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((P +* a),(Initialize I),II)) . (IC ) is set

(P +* a) /. (IC (Comput ((P +* a),(Initialize I),II))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(P +* a) /. (IC (Comput ((P +* a),(Initialize I),0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(P +* a) . (IC (Comput ((P +* a),(Initialize I),0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(s +* a) /. (IC (Comput ((s +* a),(Initialize J),0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(s +* a) . (IC (Comput ((s +* a),(Initialize J),0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

CurInstr ((P +* a),(Comput ((P +* a),(Initialize I),0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

a . 0 is set

CurInstr ((s +* a),(Comput ((s +* a),(Initialize J),0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

DataPart (Comput ((P +* a),(Initialize I),0)) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput ((P +* a),(Initialize I),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 K295(3,SCM+FSA) -compatible set

DataPart (Comput ((s +* a),(Initialize J),0)) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput ((s +* a),(Initialize J),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 K295(3,SCM+FSA) -compatible set

i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

Comput ((P +* a),(Initialize I),i) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput ((P +* a),(Initialize I),i)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((P +* a),(Initialize I),i)) . (IC ) is set

Comput ((s +* a),(Initialize J),i) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput ((s +* a),(Initialize J),i)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((s +* a),(Initialize J),i)) . (IC ) is set

Comput ((s +* a),(Initialize J),II) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

CurInstr ((s +* a),(Comput ((s +* a),(Initialize J),II))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IC (Comput ((s +* a),(Initialize J),II)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput ((s +* a),(Initialize J),II)) . (IC ) is set

(s +* a) /. (IC (Comput ((s +* a),(Initialize J),II))) 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 the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

Initialized s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(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 K295(3,SCM+FSA) -compatible K295(3,SCM+FSA) -compatible total 0 -started set

I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

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

DataPart (Initialized s) is Relation-like the carrier of SCM+FSA -defined Function-like K295(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 K295(3,SCM+FSA) -compatible set

DataPart (s +* (Initialize ((intloc 0) .--> 1))) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(s +* (Initialize ((intloc 0) .--> 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 K295(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 K295(3,SCM+FSA) -compatible total 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 K295(3,SCM+FSA) -compatible K295(3,SCM+FSA) -compatible total 0 -started set

I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

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

DataPart s is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

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 K295(3,SCM+FSA) -compatible set

Initialize s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total 0 -started set

DataPart (Initialize s) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Initialize 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 K295(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

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

DataPart I is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

I | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible set

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

IC J is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

J . (IC ) is set

DataPart J is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

J | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible set

a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

Reloc (a,b) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

IncAddr (a,b) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

K441((IncAddr (a,b)),b) is Relation-like Function-like set

dom (Start-At (0,SCM+FSA)) is non empty V35() set

Comput (P,I,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput (P,I,0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput (P,I,0)) . (IC ) is set

IC I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

I . (IC ) is set

IC (Start-At (0,SCM+FSA)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Start-At (0,SCM+FSA)) . (IC ) is set

dom a is non empty V35() set

0 + b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

dom (Reloc (a,b)) is V35() set

P . (IC I) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

P . (IC (Start-At (0,SCM+FSA))) 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

a . 0 is set

DataPart (Comput (P,I,0)) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput (P,I,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 K295(3,SCM+FSA) -compatible set

Comput (s,J,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

DataPart (Comput (s,J,0)) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput (s,J,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 K295(3,SCM+FSA) -compatible set

JJ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

Comput (P,I,JJ) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput (P,I,JJ)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput (P,I,JJ)) . (IC ) is set

(IC (Comput (P,I,JJ))) + b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

Comput (s,J,JJ) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput (s,J,JJ)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput (s,J,JJ)) . (IC ) is set

CurInstr (P,(Comput (P,I,JJ))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

P /. (IC (Comput (P,I,JJ))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IncAddr ((CurInstr (P,(Comput (P,I,JJ)))),b) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

CurInstr (s,(Comput (s,J,JJ))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

s /. (IC (Comput (s,J,JJ))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

DataPart (Comput (P,I,JJ)) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput (P,I,JJ)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible set

DataPart (Comput (s,J,JJ)) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput (s,J,JJ)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible set

s /. (IC J) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

s . (IC J) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

CurInstr (P,I) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

P /. (IC I) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

CurInstr (P,(Comput (P,I,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

P /. (IC (Comput (P,I,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IncAddr ((CurInstr (P,(Comput (P,I,0)))),b) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IncAddr ((CurInstr (P,I)),b) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(Reloc (a,b)) . (0 + b) is set

CurInstr (s,J) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

CurInstr (s,(Comput (s,J,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IC (Comput (s,J,0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput (s,J,0)) . (IC ) is set

s /. (IC (Comput (s,J,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(IC (Comput (P,I,0))) + b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

II is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

Comput (P,I,II) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput (P,I,II)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput (P,I,II)) . (IC ) is set

(IC (Comput (P,I,II))) + b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

Comput (s,J,II) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput (s,J,II)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput (s,J,II)) . (IC ) is set

CurInstr (P,(Comput (P,I,II))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

P /. (IC (Comput (P,I,II))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IncAddr ((CurInstr (P,(Comput (P,I,II)))),b) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

CurInstr (s,(Comput (s,J,II))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

s /. (IC (Comput (s,J,II))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

DataPart (Comput (P,I,II)) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput (P,I,II)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible set

DataPart (Comput (s,J,II)) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput (s,J,II)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible set

II + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer V46() Element of NAT

Comput (P,I,(II + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput (P,I,(II + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput (P,I,(II + 1))) . (IC ) is set

(IC (Comput (P,I,(II + 1)))) + b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

Comput (s,J,(II + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IC (Comput (s,J,(II + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Comput (s,J,(II + 1))) . (IC ) is set

CurInstr (P,(Comput (P,I,(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

P /. (IC (Comput (P,I,(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IncAddr ((CurInstr (P,(Comput (P,I,(II + 1))))),b) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

CurInstr (s,(Comput (s,J,(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

s /. (IC (Comput (s,J,(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

DataPart (Comput (P,I,(II + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput (P,I,(II + 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 K295(3,SCM+FSA) -compatible set

DataPart (Comput (s,J,(II + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible data-only set

(Comput (s,J,(II + 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 K295(3,SCM+FSA) -compatible set

Following (P,(Comput (P,I,II))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

Exec ((CurInstr (P,(Comput (P,I,II)))),(Comput (P,I,II))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set

K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( 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 K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like V29( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))

K33( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set

K32(K33( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set

K124( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P,(Comput (P,I,II))))) is Element of K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

K124( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P,(Comput (P,I,II))))) . (Comput (P,I,II)) is Relation-like Function-like set

Following (s,(Comput (s,J,II))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

Exec ((CurInstr (s,(Comput (s,J,II)))),(Comput (s,J,II))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

K124( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (s,(Comput (s,J,II))))) is Element of K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

K124( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (s,(Comput (s,J,II))))) . (Comput (s,J,II)) is Relation-like Function-like set

Initialize I is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total 0 -started set

I +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible K295(3,SCM+FSA) -compatible total 0 -started set

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

i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

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

P . (IC (Comput (P,I,(II + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

a . i is set

i + b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(Reloc (a,b)) . (i + b) is set

s . (IC (Comput (s,J,(II + 1)))) 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 the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

Initialized s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(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 K295(3,SCM+FSA) -compatible K295(3,SCM+FSA) -compatible total 0 -started set

I is parahalting keeping_0 with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

Exec (I,(Initialized s)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set

K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( 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 K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like V29( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))

K33( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set

K32(K33( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set

K124( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,I) is Element of K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

K124( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,I) . (Initialized s) is Relation-like Function-like set

J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() paraclosed parahalting set

I ";" J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() paraclosed parahalting set

Macro I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like V35() V53() keeping_0 paraclosed parahalting set

K270(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

K271(SCM+FSA,K270(SCM+FSA,I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

(Macro I) ";" J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() paraclosed parahalting set

K271(SCM+FSA,(Macro I)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

K232((Macro I),(Stop SCM+FSA)) is Relation-like Function-like T-Sequence-like set

K443(K271(SCM+FSA,(Macro I))) is Relation-like Function-like set

Directed K443(K271(SCM+FSA,(Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

card (Macro I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

Reloc (J,(card (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

IncAddr (J,(card (Macro I))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

K441((IncAddr (J,(card (Macro I)))),(card (Macro I))) is Relation-like Function-like set

(Directed K443(K271(SCM+FSA,(Macro I)))) +* (Reloc (J,(card (Macro I)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

IExec ((I ";" J),P,s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IExec (J,P,(Exec (I,(Initialized s)))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

a is V96() Element of the carrier of SCM+FSA

(IExec ((I ";" J),P,s)) . a is ext-real V27() V32() integer set

(IExec (J,P,(Exec (I,(Initialized s))))) . a is ext-real V27() V32() integer set

IExec ((Macro I),P,s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IExec (J,P,(IExec ((Macro I),P,s))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

(IExec (J,P,(IExec ((Macro I),P,s)))) . a is ext-real V27() V32() integer 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 K295(3,SCM+FSA) -compatible total set

Initialized s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(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 K295(3,SCM+FSA) -compatible K295(3,SCM+FSA) -compatible total 0 -started set

I is parahalting keeping_0 with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

Exec (I,(Initialized s)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set

K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( 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 K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like V29( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))

K33( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set

K32(K33( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set

K124( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,I) is Element of K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

K124( the InstructionsF of SCM+FSA,K122(K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K284(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,I) . (Initialized s) is Relation-like Function-like set

J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() paraclosed parahalting set

I ";" J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() paraclosed parahalting set

Macro I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like V35() V53() keeping_0 paraclosed parahalting set

K270(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

K271(SCM+FSA,K270(SCM+FSA,I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

(Macro I) ";" J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() paraclosed parahalting set

K271(SCM+FSA,(Macro I)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

K232((Macro I),(Stop SCM+FSA)) is Relation-like Function-like T-Sequence-like set

K443(K271(SCM+FSA,(Macro I))) is Relation-like Function-like set

Directed K443(K271(SCM+FSA,(Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

card (Macro I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

Reloc (J,(card (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

IncAddr (J,(card (Macro I))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

K441((IncAddr (J,(card (Macro I)))),(card (Macro I))) is Relation-like Function-like set

(Directed K443(K271(SCM+FSA,(Macro I)))) +* (Reloc (J,(card (Macro I)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

IExec ((I ";" J),P,s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IExec (J,P,(Exec (I,(Initialized s)))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

a is FinSeq-Location

(IExec ((I ";" J),P,s)) . a is Relation-like NAT -defined INT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of INT

(IExec (J,P,(Exec (I,(Initialized s))))) . a is Relation-like NAT -defined INT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of INT

IExec ((Macro I),P,s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

IExec (J,P,(IExec ((Macro I),P,s))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K295(3,SCM+FSA) -compatible total set

(IExec (J,P,(IExec ((Macro I),P,s)))) . a is Relation-like NAT -defined INT -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of INT

I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

card I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(card I) + 3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer V46() Element of NAT

P is V96() Element of the carrier of SCM+FSA

P =0_goto ((card I) + 3) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V144(3, SCM+FSA ) V146(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(P =0_goto ((card I) + 3)) ";" I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

Macro (P =0_goto ((card I) + 3)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

K270(SCM+FSA,(P =0_goto ((card I) + 3))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

K271(SCM+FSA,K270(SCM+FSA,(P =0_goto ((card I) + 3)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

(Macro (P =0_goto ((card I) + 3))) ";" I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

K271(SCM+FSA,(Macro (P =0_goto ((card I) + 3)))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

K232((Macro (P =0_goto ((card I) + 3))),(Stop SCM+FSA)) is Relation-like Function-like T-Sequence-like set

K443(K271(SCM+FSA,(Macro (P =0_goto ((card I) + 3))))) is Relation-like Function-like set

Directed K443(K271(SCM+FSA,(Macro (P =0_goto ((card I) + 3))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

card (Macro (P =0_goto ((card I) + 3))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

Reloc (I,(card (Macro (P =0_goto ((card I) + 3))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

IncAddr (I,(card (Macro (P =0_goto ((card I) + 3))))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

K441((IncAddr (I,(card (Macro (P =0_goto ((card I) + 3)))))),(card (Macro (P =0_goto ((card I) + 3))))) is Relation-like Function-like set

(Directed K443(K271(SCM+FSA,(Macro (P =0_goto ((card I) + 3)))))) +* (Reloc (I,(card (Macro (P =0_goto ((card I) + 3)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() set

s is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

card s is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer Element of NAT

(card s) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V32() integer V46() Element of NAT

Goto ((card s) + 1) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V35() V53() set

((P =0_goto ((card I) + 3)) ";" I) ";" (Goto ((card s) + 1)) is non empty Relation-like NAT -defined the