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
{ b1 where b1 is Element of K288(K295(3,SCM+FSA)) : b1 is V35() } is set
K33((FinPartSt SCM+FSA),(FinPartSt SCM+FSA)) is Relation-like set
K32(K33((FinPartSt SCM+FSA),(FinPartSt SCM+FSA))) is set
1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() 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