REAL is non empty V5() V29() V67() set
NAT is non empty V5() epsilon-transitive epsilon-connected ordinal limit_ordinal V29() cardinal limit_cardinal V67() Element of K19(REAL)
K19(REAL) is non empty V5() V29() V67() set
SCM+FSA is non empty V85(3) IC-Ins-separated strict halting V146(3) with_explicit_jumps IC-relocable AMI-Struct over 3
3 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
the carrier of SCM+FSA is non empty set
NAT is non empty V5() epsilon-transitive epsilon-connected ordinal limit_ordinal V29() cardinal limit_cardinal V67() set
K19(NAT) is non empty V5() V29() V67() set
K19(NAT) is non empty V5() V29() V67() set
9 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
Segm 9 is Element of K19(NAT)
Int-Locations is non empty set
K186() is set
K19(K186()) is set
2 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
K20(K186(),2) is Relation-like set
K19(K20(K186(),2)) is set
K188() is Relation-like Function-like V41(K186(),2) Element of K19(K20(K186(),2))
K189() is non empty Relation-like 2 -defined Function-like total set
K188() * K189() is Relation-like Function-like set
K162((K188() * K189())) is set
K180() is non empty set
K141(K162((K188() * K189())),K162((K188() * K189()))) is set
K20(K180(),K141(K162((K188() * K189())),K162((K188() * K189())))) is Relation-like set
K19(K20(K180(),K141(K162((K188() * K189())),K162((K188() * K189()))))) is set
K19( the carrier of SCM+FSA) is set
the InstructionsF of SCM+FSA is non empty Relation-like standard-ins V75() J/A-independent V78() set
INT is non empty V5() V29() V67() set
Int-Locations is non empty Element of K19( the carrier of SCM+FSA)
K324(Int-Locations) is V99() set
K19(Int-Locations) is set
FinSeq-Locations is non empty V5() V29() V67() Element of K19( the carrier of SCM+FSA)
K324(FinSeq-Locations) is V99() set
K19(FinSeq-Locations) is non empty V5() V29() V67() set
K274(3,SCM+FSA) is non empty Relation-like non-empty non empty-yielding the carrier of SCM+FSA -defined Function-like total set
the Object-Kind of SCM+FSA is Relation-like Function-like V41( the carrier of SCM+FSA,3) Element of K19(K20( the carrier of SCM+FSA,3))
K20( the carrier of SCM+FSA,3) is Relation-like set
K19(K20( 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 Function-like set
COMPLEX is non empty V5() V29() V67() set
RAT is non empty V5() V29() V67() set
{} is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V29() V30() V33() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered integer V69() initial V118() Function-yielding V141() V156() set
1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
{{},1} is non empty V29() V33() set
K568() is non empty V85(2) IC-Ins-separated strict strict halting AMI-Struct over 2
the InstructionsF of K568() is non empty Relation-like standard-ins V75() J/A-independent V78() set
the carrier of K568() is non empty set
K274(2,K568()) is non empty Relation-like non-empty non empty-yielding the carrier of K568() -defined Function-like total set
the Object-Kind of K568() is Relation-like Function-like V41( the carrier of K568(),2) Element of K19(K20( the carrier of K568(),2))
K20( the carrier of K568(),2) is Relation-like set
K19(K20( the carrier of K568(),2)) is set
the U7 of K568() is non empty Relation-like 2 -defined Function-like total set
the Object-Kind of K568() * the U7 of K568() is Relation-like Function-like set
K20(NAT,K19(NAT)) is non empty V5() Relation-like V29() V67() set
K19(K20(NAT,K19(NAT))) is non empty V5() V29() V67() set
FinPartSt SCM+FSA is non empty Element of K19(K166(K274(3,SCM+FSA)))
K166(K274(3,SCM+FSA)) is set
K19(K166(K274(3,SCM+FSA))) is set
{ b1 where b1 is Element of K166(K274(3,SCM+FSA)) : b1 is V29() } is set
K20((FinPartSt SCM+FSA),(FinPartSt SCM+FSA)) is Relation-like set
K19(K20((FinPartSt SCM+FSA),(FinPartSt SCM+FSA))) is set
0 is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V29() V30() V33() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered integer V69() initial V118() Function-yielding V141() V156() Element of NAT
intloc 0 is V65() read-only Element of the carrier of SCM+FSA
K577(0) is V65() Element of the carrier of K568()
halt SCM+FSA is ins-loc-free ins-loc-free halting V145(3, SCM+FSA ) with_explicit_jumps IC-relocable 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
<%(halt SCM+FSA)%> is non empty V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like constant V29() 1 -element initial V83( SCM+FSA ) set
0 .--> (halt SCM+FSA) is non empty V5() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V29() 1 -element V83( SCM+FSA ) set
{0} is non empty V5() functional V29() V33() 1 -element set
{0} --> (halt SCM+FSA) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41({0},{(halt SCM+FSA)}) Element of K19(K20({0},{(halt SCM+FSA)}))
{(halt SCM+FSA)} is non empty V5() V29() 1 -element set
K20({0},{(halt SCM+FSA)}) is Relation-like V29() set
K19(K20({0},{(halt SCM+FSA)})) is V29() V33() set
the InstructionsF of SCM+FSA ^omega is non empty functional set
intloc 1 is V65() Element of the carrier of SCM+FSA
K577(1) is V65() Element of the carrier of K568()
intloc 2 is V65() Element of the carrier of SCM+FSA
K577(2) is V65() Element of the carrier of K568()
12 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
4 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
5 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
6 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
7 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
8 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
10 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
11 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
IC is V52( SCM+FSA ) Element of the carrier of SCM+FSA
{0,1} is non empty V29() V33() Element of K19(NAT)
{{}} is non empty V5() functional V29() V33() 1 -element set
(intloc 0) .--> 1 is non empty V5() Relation-like the carrier of SCM+FSA -defined {(intloc 0)} -defined {(intloc 0)} -defined NAT -valued Function-like one-to-one constant K274(3,SCM+FSA) -compatible V29() 1 -element data-only set
{(intloc 0)} is non empty V5() V29() 1 -element set
{(intloc 0)} --> 1 is non empty Relation-like non-empty non empty-yielding {(intloc 0)} -defined NAT -valued Function-like constant V29() total V41({(intloc 0)},{1}) Element of K19(K20({(intloc 0)},{1}))
{1} is non empty V5() V29() V33() 1 -element V66() V67() set
K20({(intloc 0)},{1}) is Relation-like V29() set
K19(K20({(intloc 0)},{1})) is V29() V33() set
Initialize ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible V29() 0 -started set
Start-At (0,SCM+FSA) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible V29() 0 -started set
(IC ) .--> 0 is non empty V5() Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued Function-like one-to-one constant V29() 1 -element Function-yielding V141() set
{(IC )} is non empty V5() V29() 1 -element set
{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued Function-like constant V29() total V41({(IC )},{0}) Function-yielding V141() Element of K19(K20({(IC )},{0}))
K20({(IC )},{0}) is Relation-like V29() set
K19(K20({(IC )},{0})) is V29() V33() set
((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible V29() 0 -started set
dom (Initialize ((intloc 0) .--> 1)) is V29() set
{(intloc 0),(IC )} is non empty V29() Element of K19( the carrier of SCM+FSA)
(Initialize ((intloc 0) .--> 1)) . (intloc 0) is set
goto 2 is non ins-loc-free V79( the InstructionsF of SCM+FSA) non halting V145(3, SCM+FSA ) V147(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K574(2) is Element of the InstructionsF of K568()
id the InstructionsF of SCM+FSA is non empty Relation-like the InstructionsF of SCM+FSA -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one total Element of K19(K20( the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA))
K20( the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA) is Relation-like set
K19(K20( the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA)) is set
dom (id the InstructionsF of SCM+FSA) is non empty set
a is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Macro a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
Load a is non empty V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like constant V29() 1 -element initial V83( SCM+FSA ) set
0 .--> a is non empty V5() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V29() 1 -element V83( SCM+FSA ) set
{0} --> a is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41({0},{a}) Element of K19(K20({0},{a}))
{a} is non empty V5() V29() 1 -element set
K20({0},{a}) is Relation-like V29() set
K19(K20({0},{a})) is V29() V33() set
K271(SCM+FSA,(Load a)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
Stop SCM+FSA is non empty V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() 1 -element initial non halt-free V82( SCM+FSA ) V83( SCM+FSA ) V148(3, SCM+FSA ) set
<%(halt SCM+FSA)%> is non empty V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like constant V29() 1 -element initial V83( SCM+FSA ) set
(Load a) ^ (Stop SCM+FSA) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
Directed (Macro a) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial halt-free V83( SCM+FSA ) set
card (Macro a) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
dom (Macro a) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
Directed ((Macro a),(card (Macro a))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() halt-free set
goto (card (Macro a)) is non ins-loc-free V79( the InstructionsF of SCM+FSA) non halting V145(3, SCM+FSA ) V147(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K574((card (Macro a))) is Element of the InstructionsF of K568()
(Macro a) +~ ((halt SCM+FSA),(goto (card (Macro a)))) is Relation-like Function-like set
(Directed (Macro a)) . 0 is set
(Macro a) . 0 is set
dom (Macro a) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of K19(NAT)
(halt SCM+FSA) .--> (goto 2) is non empty V5() Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V29() 1 -element set
{(halt SCM+FSA)} --> (goto 2) is non empty Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41({(halt SCM+FSA)},{(goto 2)}) Element of K19(K20({(halt SCM+FSA)},{(goto 2)}))
{(goto 2)} is non empty V5() V29() 1 -element set
K20({(halt SCM+FSA)},{(goto 2)}) is Relation-like V29() set
K19(K20({(halt SCM+FSA)},{(goto 2)})) is V29() V33() set
dom ((halt SCM+FSA) .--> (goto 2)) is non empty V5() V29() 1 -element set
{(halt SCM+FSA)} is non empty V5() Relation-like V29() 1 -element Element of K19( the InstructionsF of SCM+FSA)
K19( the InstructionsF of SCM+FSA) is set
rng (Macro a) is non empty V29() set
Replace ((id the InstructionsF of SCM+FSA),(halt SCM+FSA),(goto 2)) is Relation-like the InstructionsF of SCM+FSA -valued Function-like set
(Macro a) * (Replace ((id the InstructionsF of SCM+FSA),(halt SCM+FSA),(goto 2))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() set
((Macro a) * (Replace ((id the InstructionsF of SCM+FSA),(halt SCM+FSA),(goto 2)))) . 0 is set
(id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2)) is non empty Relation-like the InstructionsF of SCM+FSA -defined the InstructionsF of SCM+FSA -valued Function-like total set
(Macro a) * ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() set
((Macro a) * ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2)))) . 0 is set
((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2))) . a is set
((halt SCM+FSA) .--> (goto 2)) . a is set
(id the InstructionsF of SCM+FSA) . a is set
a is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Macro a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
Load a is non empty V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like constant V29() 1 -element initial V83( SCM+FSA ) set
0 .--> a is non empty V5() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V29() 1 -element V83( SCM+FSA ) set
{0} --> a is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41({0},{a}) Element of K19(K20({0},{a}))
{a} is non empty V5() V29() 1 -element set
K20({0},{a}) is Relation-like V29() set
K19(K20({0},{a})) is V29() V33() set
K271(SCM+FSA,(Load a)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
Stop SCM+FSA is non empty V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() 1 -element initial non halt-free V82( SCM+FSA ) V83( SCM+FSA ) V148(3, SCM+FSA ) set
<%(halt SCM+FSA)%> is non empty V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like constant V29() 1 -element initial V83( SCM+FSA ) set
(Load a) ^ (Stop SCM+FSA) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
Directed (Macro a) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial halt-free V83( SCM+FSA ) set
card (Macro a) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
dom (Macro a) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
Directed ((Macro a),(card (Macro a))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() halt-free set
goto (card (Macro a)) is non ins-loc-free V79( the InstructionsF of SCM+FSA) non halting V145(3, SCM+FSA ) V147(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K574((card (Macro a))) is Element of the InstructionsF of K568()
(Macro a) +~ ((halt SCM+FSA),(goto (card (Macro a)))) is Relation-like Function-like set
(Directed (Macro a)) . 1 is set
(Macro a) . 1 is set
dom (Macro a) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of K19(NAT)
(halt SCM+FSA) .--> (goto 2) is non empty V5() Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V29() 1 -element set
{(halt SCM+FSA)} --> (goto 2) is non empty Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41({(halt SCM+FSA)},{(goto 2)}) Element of K19(K20({(halt SCM+FSA)},{(goto 2)}))
{(goto 2)} is non empty V5() V29() 1 -element set
K20({(halt SCM+FSA)},{(goto 2)}) is Relation-like V29() set
K19(K20({(halt SCM+FSA)},{(goto 2)})) is V29() V33() set
dom ((halt SCM+FSA) .--> (goto 2)) is non empty V5() V29() 1 -element set
{(halt SCM+FSA)} is non empty V5() Relation-like V29() 1 -element Element of K19( the InstructionsF of SCM+FSA)
K19( the InstructionsF of SCM+FSA) is set
id the InstructionsF of SCM+FSA is non empty Relation-like the InstructionsF of SCM+FSA -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one total Element of K19(K20( the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA))
K20( the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA) is Relation-like set
K19(K20( the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA)) is set
dom (id the InstructionsF of SCM+FSA) is non empty set
rng (Macro a) is non empty V29() set
Replace ((id the InstructionsF of SCM+FSA),(halt SCM+FSA),(goto 2)) is Relation-like the InstructionsF of SCM+FSA -valued Function-like set
(Macro a) * (Replace ((id the InstructionsF of SCM+FSA),(halt SCM+FSA),(goto 2))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() set
((Macro a) * (Replace ((id the InstructionsF of SCM+FSA),(halt SCM+FSA),(goto 2)))) . 1 is set
(id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2)) is non empty Relation-like the InstructionsF of SCM+FSA -defined the InstructionsF of SCM+FSA -valued Function-like total set
(Macro a) * ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() set
((Macro a) * ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2)))) . 1 is set
((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2))) . (halt SCM+FSA) is set
((halt SCM+FSA) .--> (goto 2)) . (halt SCM+FSA) is set
a is V65() Element of the carrier of SCM+FSA
k is ext-real V14() V15() integer set
a := k is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() set
aSeq (a,k) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
(aSeq (a,k)) ^ <%(halt SCM+FSA)%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
a . (IC ) is set
k is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
dom k is non empty V118() set
i is V65() Element of the carrier of SCM+FSA
k1 is ext-real V14() V15() integer set
i := k1 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
i := (intloc 0) is ins-loc-free V79( the InstructionsF of SCM+FSA) non halting V147(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<%(i := (intloc 0))%> is non empty V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like constant V29() 1 -element initial V83( SCM+FSA ) set
0 .--> (i := (intloc 0)) is non empty V5() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V29() 1 -element V83( SCM+FSA ) set
{0} --> (i := (intloc 0)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41({0},{(i := (intloc 0))}) Element of K19(K20({0},{(i := (intloc 0))}))
{(i := (intloc 0))} is non empty V5() V29() 1 -element set
K20({0},{(i := (intloc 0))}) is Relation-like V29() set
K19(K20({0},{(i := (intloc 0))})) is V29() V33() set
AddTo (i,(intloc 0)) is ins-loc-free V79( the InstructionsF of SCM+FSA) non halting V147(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
k + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
k --> (AddTo (i,(intloc 0))) is T-Sequence-like Relation-like k -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41(k, the InstructionsF of SCM+FSA) initial Element of K19(K20(k, the InstructionsF of SCM+FSA))
K20(k, the InstructionsF of SCM+FSA) is Relation-like set
K19(K20(k, the InstructionsF of SCM+FSA)) is set
{(AddTo (i,(intloc 0)))} is non empty V5() V29() 1 -element set
K20(k,{(AddTo (i,(intloc 0)))}) is Relation-like V29() set
<%(i := (intloc 0))%> ^ (k --> (AddTo (i,(intloc 0)))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
(<%(i := (intloc 0))%> ^ (k --> (AddTo (i,(intloc 0))))) ^ <%(halt SCM+FSA)%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
len (<%(i := (intloc 0))%> ^ (k --> (AddTo (i,(intloc 0))))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
dom (<%(i := (intloc 0))%> ^ (k --> (AddTo (i,(intloc 0))))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
len <%(i := (intloc 0))%> is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
dom <%(i := (intloc 0))%> is ext-real positive non negative non empty V5() epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal 1 -element integer V66() V118() set
len (k --> (AddTo (i,(intloc 0)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom (k --> (AddTo (i,(intloc 0)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() set
(len <%(i := (intloc 0))%>) + (len (k --> (AddTo (i,(intloc 0))))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
1 + (len (k --> (AddTo (i,(intloc 0))))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
((<%(i := (intloc 0))%> ^ (k --> (AddTo (i,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . 0 is set
(k --> (AddTo (i,(intloc 0)))) ^ <%(halt SCM+FSA)%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
<%(i := (intloc 0))%> ^ ((k --> (AddTo (i,(intloc 0)))) ^ <%(halt SCM+FSA)%>) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
(<%(i := (intloc 0))%> ^ ((k --> (AddTo (i,(intloc 0)))) ^ <%(halt SCM+FSA)%>)) . 0 is set
len ((<%(i := (intloc 0))%> ^ (k --> (AddTo (i,(intloc 0))))) ^ <%(halt SCM+FSA)%>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
dom ((<%(i := (intloc 0))%> ^ (k --> (AddTo (i,(intloc 0))))) ^ <%(halt SCM+FSA)%>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
len <%(halt SCM+FSA)%> is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
dom <%(halt SCM+FSA)%> is ext-real positive non negative non empty V5() epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal 1 -element integer V66() V118() set
(len (<%(i := (intloc 0))%> ^ (k --> (AddTo (i,(intloc 0)))))) + (len <%(halt SCM+FSA)%>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
h is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
h + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom ((<%(i := (intloc 0))%> ^ (k --> (AddTo (i,(intloc 0))))) ^ <%(halt SCM+FSA)%>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of K19(NAT)
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
k . q is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((<%(i := (intloc 0))%> ^ (k --> (AddTo (i,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . q is set
k . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (k,a,q) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
CurInstr (k,(Comput (k,a,q))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (k,a,q)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k,a,q)) . (IC ) is set
k /. (IC (Comput (k,a,q))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
q + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
Comput (k,a,(q + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Following (k,(Comput (k,a,q))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Exec ((CurInstr (k,(Comput (k,a,q)))),(Comput (k,a,q))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V41( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K19(K20( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K20( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K19(K20( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
the Execution of SCM+FSA . (CurInstr (k,(Comput (k,a,q)))) is Element of K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (CurInstr (k,(Comput (k,a,q))))) . (Comput (k,a,q)) is set
Exec ((i := (intloc 0)),a) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . (i := (intloc 0)) is Element of K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (i := (intloc 0))) . a is set
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
q - 1 is ext-real V14() V15() integer set
h - 1 is ext-real V14() V15() integer set
q0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom (<%(i := (intloc 0))%> ^ (k --> (AddTo (i,(intloc 0))))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of K19(NAT)
((<%(i := (intloc 0))%> ^ (k --> (AddTo (i,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . q is set
(<%(i := (intloc 0))%> ^ (k --> (AddTo (i,(intloc 0))))) . q is set
(k --> (AddTo (i,(intloc 0)))) . (q - 1) is set
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
0 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
k . q is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((<%(i := (intloc 0))%> ^ (k --> (AddTo (i,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . q is set
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (k,a,q) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k,a,q)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k,a,q)) . (IC ) is set
q0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (k,a,q0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k,a,q0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k,a,q0)) . (IC ) is set
q0 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
Comput (k,a,(q0 + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k,a,(q0 + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k,a,(q0 + 1))) . (IC ) is set
(Exec ((i := (intloc 0)),a)) . (IC ) is set
succ q0 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
q0 + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
CurInstr (k,(Comput (k,a,q0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k /. (IC (Comput (k,a,q0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k . q0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Following (k,(Comput (k,a,q0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Exec ((CurInstr (k,(Comput (k,a,q0)))),(Comput (k,a,q0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . (CurInstr (k,(Comput (k,a,q0)))) is Element of K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (CurInstr (k,(Comput (k,a,q0))))) . (Comput (k,a,q0)) is set
Exec ((AddTo (i,(intloc 0))),(Comput (k,a,q0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . (AddTo (i,(intloc 0))) is Element of K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (AddTo (i,(intloc 0)))) . (Comput (k,a,q0)) is set
succ (IC (Comput (k,a,q0))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
Comput (k,a,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k,a,0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k,a,0)) . (IC ) is set
h + (len <%(halt SCM+FSA)%>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
((<%(i := (intloc 0))%> ^ (k --> (AddTo (i,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . h is set
h - h is ext-real V14() V15() integer set
<%(halt SCM+FSA)%> . (h - h) is set
Comput (k,a,h) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
CurInstr (k,(Comput (k,a,h))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (k,a,h)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k,a,h)) . (IC ) is set
k /. (IC (Comput (k,a,h))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k . (IC (Comput (k,a,h))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k . h is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
- k1 is ext-real V14() V15() integer set
i := (intloc 0) is ins-loc-free V79( the InstructionsF of SCM+FSA) non halting V147(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<%(i := (intloc 0))%> is non empty V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like constant V29() 1 -element initial V83( SCM+FSA ) set
0 .--> (i := (intloc 0)) is non empty V5() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V29() 1 -element V83( SCM+FSA ) set
{0} --> (i := (intloc 0)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41({0},{(i := (intloc 0))}) Element of K19(K20({0},{(i := (intloc 0))}))
{(i := (intloc 0))} is non empty V5() V29() 1 -element set
K20({0},{(i := (intloc 0))}) is Relation-like V29() set
K19(K20({0},{(i := (intloc 0))})) is V29() V33() set
SubFrom (i,(intloc 0)) is ins-loc-free V79( the InstructionsF of SCM+FSA) non halting V147(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
l + k1 is ext-real V14() V15() integer set
l --> (SubFrom (i,(intloc 0))) is T-Sequence-like Relation-like l -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41(l, the InstructionsF of SCM+FSA) initial Element of K19(K20(l, the InstructionsF of SCM+FSA))
K20(l, the InstructionsF of SCM+FSA) is Relation-like set
K19(K20(l, the InstructionsF of SCM+FSA)) is set
{(SubFrom (i,(intloc 0)))} is non empty V5() V29() 1 -element set
K20(l,{(SubFrom (i,(intloc 0)))}) is Relation-like V29() set
<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0)))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
(<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0))))) ^ <%(halt SCM+FSA)%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
len (<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0))))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
dom (<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0))))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
len <%(i := (intloc 0))%> is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
dom <%(i := (intloc 0))%> is ext-real positive non negative non empty V5() epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal 1 -element integer V66() V118() set
len (l --> (SubFrom (i,(intloc 0)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom (l --> (SubFrom (i,(intloc 0)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() set
(len <%(i := (intloc 0))%>) + (len (l --> (SubFrom (i,(intloc 0))))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
1 + (len (l --> (SubFrom (i,(intloc 0))))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
k + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
(k + 1) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
((<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . 0 is set
(l --> (SubFrom (i,(intloc 0)))) ^ <%(halt SCM+FSA)%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
<%(i := (intloc 0))%> ^ ((l --> (SubFrom (i,(intloc 0)))) ^ <%(halt SCM+FSA)%>) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
(<%(i := (intloc 0))%> ^ ((l --> (SubFrom (i,(intloc 0)))) ^ <%(halt SCM+FSA)%>)) . 0 is set
len ((<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0))))) ^ <%(halt SCM+FSA)%>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
dom ((<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0))))) ^ <%(halt SCM+FSA)%>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
len <%(halt SCM+FSA)%> is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
dom <%(halt SCM+FSA)%> is ext-real positive non negative non empty V5() epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal 1 -element integer V66() V118() set
(len (<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0)))))) + (len <%(halt SCM+FSA)%>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
((k + 1) + 1) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom ((<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0))))) ^ <%(halt SCM+FSA)%>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of K19(NAT)
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
k . q is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . q is set
k . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (k,a,q) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
CurInstr (k,(Comput (k,a,q))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (k,a,q)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k,a,q)) . (IC ) is set
k /. (IC (Comput (k,a,q))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
q + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
Comput (k,a,(q + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Following (k,(Comput (k,a,q))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Exec ((CurInstr (k,(Comput (k,a,q)))),(Comput (k,a,q))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V41( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K19(K20( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K20( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K19(K20( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
the Execution of SCM+FSA . (CurInstr (k,(Comput (k,a,q)))) is Element of K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (CurInstr (k,(Comput (k,a,q))))) . (Comput (k,a,q)) is set
Exec ((i := (intloc 0)),a) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . (i := (intloc 0)) is Element of K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (i := (intloc 0))) . a is set
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
q - 1 is ext-real V14() V15() integer set
l + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
(l + 1) - 1 is ext-real V14() V15() integer set
q0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom (<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0))))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of K19(NAT)
((<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . q is set
(<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0))))) . q is set
(l --> (SubFrom (i,(intloc 0)))) . (q - 1) is set
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
0 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
k . q is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . q is set
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (k,a,q) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k,a,q)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k,a,q)) . (IC ) is set
q0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (k,a,q0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k,a,q0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k,a,q0)) . (IC ) is set
q0 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
Comput (k,a,(q0 + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k,a,(q0 + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k,a,(q0 + 1))) . (IC ) is set
(Exec ((i := (intloc 0)),a)) . (IC ) is set
succ q0 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
q0 + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
CurInstr (k,(Comput (k,a,q0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k /. (IC (Comput (k,a,q0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k . q0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Following (k,(Comput (k,a,q0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Exec ((CurInstr (k,(Comput (k,a,q0)))),(Comput (k,a,q0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . (CurInstr (k,(Comput (k,a,q0)))) is Element of K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (CurInstr (k,(Comput (k,a,q0))))) . (Comput (k,a,q0)) is set
Exec ((SubFrom (i,(intloc 0))),(Comput (k,a,q0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . (SubFrom (i,(intloc 0))) is Element of K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (SubFrom (i,(intloc 0)))) . (Comput (k,a,q0)) is set
succ (IC (Comput (k,a,q0))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
Comput (k,a,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k,a,0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k,a,0)) . (IC ) is set
((<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . ((k + 1) + 1) is set
((k + 1) + 1) - (len (<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0)))))) is ext-real V14() V15() integer set
<%(halt SCM+FSA)%> . (((k + 1) + 1) - (len (<%(i := (intloc 0))%> ^ (l --> (SubFrom (i,(intloc 0))))))) is set
Comput (k,a,((k + 1) + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
CurInstr (k,(Comput (k,a,((k + 1) + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (k,a,((k + 1) + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k,a,((k + 1) + 1))) . (IC ) is set
k /. (IC (Comput (k,a,((k + 1) + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k . (IC (Comput (k,a,((k + 1) + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k . ((k + 1) + 1) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
a is V65() Element of the carrier of SCM+FSA
k is ext-real V14() V15() integer set
a := k is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
dom (Start-At (0,SCM+FSA)) is non empty V29() set
i is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
k1 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
IC i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
i . (IC ) is set
IC (Start-At (0,SCM+FSA)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Start-At (0,SCM+FSA)) . (IC ) is set
a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
k is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
i is V65() non read-only Element of the carrier of SCM+FSA
k1 is ext-real V14() V15() integer set
i := k1 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial paraclosed parahalting set
IExec ((i := k1),a,k) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
a +* (i := k1) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialized k is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
k +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
Result ((a +* (i := k1)),(Initialized k)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
(IExec ((i := k1),a,k)) . i is ext-real V14() V15() integer set
(k +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) is ext-real V14() V15() integer set
l is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
Result ((a +* (i := k1)),l) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
(Result ((a +* (i := k1)),l)) . i is ext-real V14() V15() integer set
h is V65() non read-only Element of the carrier of SCM+FSA
(IExec ((i := k1),a,k)) . h is ext-real V14() V15() integer set
(Result ((a +* (i := k1)),l)) . h is ext-real V14() V15() integer set
l . h is ext-real V14() V15() integer set
k . h is ext-real V14() V15() integer set
h is FinSeq-Location
(IExec ((i := k1),a,k)) . h is Relation-like NAT -defined INT -valued Function-like V29() FinSequence-like FinSubsequence-like FinSequence of INT
k . h is Relation-like NAT -defined INT -valued Function-like V29() FinSequence-like FinSubsequence-like FinSequence of INT
(Result ((a +* (i := k1)),l)) . h is Relation-like NAT -defined INT -valued Function-like V29() FinSequence-like FinSubsequence-like FinSequence of INT
l . h is Relation-like NAT -defined INT -valued Function-like V29() FinSequence-like FinSubsequence-like FinSequence of INT
a is T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
k is T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
a ^ k is T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
i is T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
(a ^ k) ^ i is T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
k1 is T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
((a ^ k) ^ i) ^ k1 is T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
k ^ i is T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
(k ^ i) ^ k1 is T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
a ^ ((k ^ i) ^ k1) is T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
a ^ (k ^ i) is T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
(a ^ (k ^ i)) ^ k1 is T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
k is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total a -started set
i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
dom i is non empty V118() set
IC k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
k . (IC ) is set
k1 is V65() Element of the carrier of SCM+FSA
k is ext-real V14() V15() integer set
aSeq (k1,k) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
len (aSeq (k1,k)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom (aSeq (k1,k)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() set
dom (aSeq (k1,k)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of K19(NAT)
l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(aSeq (k1,k)) . l is set
a + l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
i . (a + l) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
aSeq (k1,l) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
k1 := (intloc 0) is ins-loc-free V79( the InstructionsF of SCM+FSA) non halting V147(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<%(k1 := (intloc 0))%> is non empty V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like constant V29() 1 -element initial V83( SCM+FSA ) set
0 .--> (k1 := (intloc 0)) is non empty V5() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V29() 1 -element V83( SCM+FSA ) set
{0} --> (k1 := (intloc 0)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41({0},{(k1 := (intloc 0))}) Element of K19(K20({0},{(k1 := (intloc 0))}))
{(k1 := (intloc 0))} is non empty V5() V29() 1 -element set
K20({0},{(k1 := (intloc 0))}) is Relation-like V29() set
K19(K20({0},{(k1 := (intloc 0))})) is V29() V33() set
AddTo (k1,(intloc 0)) is ins-loc-free V79( the InstructionsF of SCM+FSA) non halting V147(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
h is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
h + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
h --> (AddTo (k1,(intloc 0))) is T-Sequence-like Relation-like h -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41(h, the InstructionsF of SCM+FSA) initial Element of K19(K20(h, the InstructionsF of SCM+FSA))
K20(h, the InstructionsF of SCM+FSA) is Relation-like set
K19(K20(h, the InstructionsF of SCM+FSA)) is set
{(AddTo (k1,(intloc 0)))} is non empty V5() V29() 1 -element set
K20(h,{(AddTo (k1,(intloc 0)))}) is Relation-like V29() set
<%(k1 := (intloc 0))%> ^ (h --> (AddTo (k1,(intloc 0)))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
len (aSeq (k1,l)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom (aSeq (k1,l)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() set
len <%(k1 := (intloc 0))%> is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
dom <%(k1 := (intloc 0))%> is ext-real positive non negative non empty V5() epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal 1 -element integer V66() V118() set
len (h --> (AddTo (k1,(intloc 0)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom (h --> (AddTo (k1,(intloc 0)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() set
(len <%(k1 := (intloc 0))%>) + (len (h --> (AddTo (k1,(intloc 0))))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
1 + (len (h --> (AddTo (k1,(intloc 0))))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
q - 1 is ext-real V14() V15() integer set
q0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
q0 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
(aSeq (k1,l)) . q is set
(h --> (AddTo (k1,(intloc 0)))) . (q - 1) is set
dom (aSeq (k1,l)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of K19(NAT)
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
0 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
a + q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
i . (a + q) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(aSeq (k1,l)) . q is set
a + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
i . (a + 0) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(aSeq (k1,l)) . 0 is set
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (i,k,q) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
CurInstr (i,(Comput (i,k,q))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (i,k,q)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (i,k,q)) . (IC ) is set
i /. (IC (Comput (i,k,q))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i . (IC (Comput (i,k,q))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
q + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
Comput (i,k,(q + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Following (i,(Comput (i,k,q))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Exec ((CurInstr (i,(Comput (i,k,q)))),(Comput (i,k,q))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K141(K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V41( the