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 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 (i,(Comput (i,k,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 (i,(Comput (i,k,q))))) . (Comput (i,k,q)) is set
Exec ((k1 := (intloc 0)),k) 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 . (k1 := (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 . (k1 := (intloc 0))) . k 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
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
a + 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 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
IC (Comput (i,k,(q + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (i,k,(q + 1))) . (IC ) is set
a + (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
(Exec ((k1 := (intloc 0)),k)) . (IC ) is set
succ a is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
(succ a) + q 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 + 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 + 1) + q 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 + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
CurInstr (i,(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
i . (a + q) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
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
the Execution of SCM+FSA . (CurInstr (i,(Comput (i,k,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 (i,(Comput (i,k,q))))) . (Comput (i,k,q)) is set
Exec ((AddTo (k1,(intloc 0))),(Comput (i,k,q))) 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 (k1,(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 (k1,(intloc 0)))) . (Comput (i,k,q)) is set
succ (IC (Comput (i,k,q))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
(a + 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
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
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
a + q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (i,k,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (i,k,0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (i,k,0)) . (IC ) 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
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
a + q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
- k is ext-real V14() V15() integer set
l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
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 positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
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
SubFrom (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 + k is ext-real V14() V15() integer set
h --> (SubFrom (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
{(SubFrom (k1,(intloc 0)))} is non empty V5() V29() 1 -element set
K20(h,{(SubFrom (k1,(intloc 0)))}) is Relation-like V29() set
<%(k1 := (intloc 0))%> ^ (h --> (SubFrom (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 <%(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 --> (SubFrom (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 --> (SubFrom (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 --> (SubFrom (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 --> (SubFrom (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
((l + 1) + 1) - 1 is ext-real V14() V15() integer set
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
(aSeq (k1,k)) . q is set
(h --> (SubFrom (k1,(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
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,k)) . 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,k)) . 0 is set
Exec ((k1 := (intloc 0)),k) 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 . (k1 := (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 . (k1 := (intloc 0))) . k 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
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
i . (IC (Comput (i,k,q))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
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
the Execution of SCM+FSA . (CurInstr (i,(Comput (i,k,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 (i,(Comput (i,k,q))))) . (Comput (i,k,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 (i,k,q) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
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
a + 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 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
IC (Comput (i,k,(q + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (i,k,(q + 1))) . (IC ) is set
a + (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
(Exec ((k1 := (intloc 0)),k)) . (IC ) is set
succ (a + q) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
(a + 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
q + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
CurInstr (i,(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
i . (a + q) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
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
the Execution of SCM+FSA . (CurInstr (i,(Comput (i,k,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 (i,(Comput (i,k,q))))) . (Comput (i,k,q)) is set
Exec ((SubFrom (k1,(intloc 0))),(Comput (i,k,q))) 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 (k1,(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 (k1,(intloc 0)))) . (Comput (i,k,q)) is set
succ (IC (Comput (i,k,q))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
(a + 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
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
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
a + q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (i,k,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (i,k,0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (i,k,0)) . (IC ) 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
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
a + q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
k is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
i is V65() Element of the carrier of SCM+FSA
k1 is ext-real V14() V15() integer set
aSeq (i,k1) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
len (aSeq (i,k1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom (aSeq (i,k1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() set
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom (aSeq (i,k1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of K19(NAT)
0 + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
k . (0 + k) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(aSeq (i,k1)) . k is set
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (k,a,k) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k,a,k)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k,a,k)) . (IC ) is set
0 + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
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
dom k1 is non empty V118() set
l is FinSeq-Location
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 the InstructionsF of SCM+FSA -valued Function-like V29() set
len h is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
aSeq ((intloc 1),(len h)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
l :=<0,...,0> (intloc 1) is 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
<*(intloc 1),l*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
<*(intloc 1)*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,(intloc 1)] is set
{1,(intloc 1)} is non empty V29() set
{{1,(intloc 1)},{1}} is non empty V29() V33() V66() V67() set
{[1,(intloc 1)]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*l*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,l] is set
{1,l} is non empty V29() set
{{1,l},{1}} is non empty V29() V33() V66() V67() set
{[1,l]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*(intloc 1)*> ^ <*l*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
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
K68(12,{},<*(intloc 1),l*>) is set
<%(l :=<0,...,0> (intloc 1))%> 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 .--> (l :=<0,...,0> (intloc 1)) 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} --> (l :=<0,...,0> (intloc 1)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41({0},{(l :=<0,...,0> (intloc 1))}) Element of K19(K20({0},{(l :=<0,...,0> (intloc 1))}))
{(l :=<0,...,0> (intloc 1))} is non empty V5() V29() 1 -element set
K20({0},{(l :=<0,...,0> (intloc 1))}) is Relation-like V29() set
K19(K20({0},{(l :=<0,...,0> (intloc 1))})) is V29() V33() set
(aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
aSeq (l,h) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (aSeq (l,h)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
(((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (aSeq (l,h))) ^ <%(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 ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (aSeq (l,h))) ^ <%(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 ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (aSeq (l,h))) ^ <%(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
pp is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (aSeq (l,h))) ^ <%(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)
k1 . pp is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (aSeq (l,h))) ^ <%(halt SCM+FSA)%>) . pp is set
(l,(intloc 1)) := (intloc 2) is 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
<*(intloc 2),l,(intloc 1)*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*(intloc 2)*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,(intloc 2)] is set
{1,(intloc 2)} is non empty V29() set
{{1,(intloc 2)},{1}} is non empty V29() V33() V66() V67() set
{[1,(intloc 2)]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*(intloc 2)*> ^ <*l*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
(<*(intloc 2)*> ^ <*l*>) ^ <*(intloc 1)*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(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
K68(10,{},<*(intloc 2),l,(intloc 1)*>) is set
<%((l,(intloc 1)) := (intloc 2))%> 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 .--> ((l,(intloc 1)) := (intloc 2)) 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} --> ((l,(intloc 1)) := (intloc 2)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41({0},{((l,(intloc 1)) := (intloc 2))}) Element of K19(K20({0},{((l,(intloc 1)) := (intloc 2))}))
{((l,(intloc 1)) := (intloc 2))} is non empty V5() V29() 1 -element set
K20({0},{((l,(intloc 1)) := (intloc 2))}) is Relation-like V29() set
K19(K20({0},{((l,(intloc 1)) := (intloc 2))})) is V29() V33() set
pp is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like V29() initial Function-yielding V141() set
len pp is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom pp is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() set
FlattenSeq pp is T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp) is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)) 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 (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))) + 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 is T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
i is set
<%i%> is non empty V5() T-Sequence-like Relation-like NAT -defined Function-like constant V29() 1 -element initial set
0 .--> i is non empty V5() Relation-like NAT -defined {0} -defined Function-like one-to-one constant V29() 1 -element set
{0} --> i is non empty Relation-like {0} -defined Function-like constant V29() total V41({0},{i}) Element of K19(K20({0},{i}))
{i} is non empty V5() V29() 1 -element set
K20({0},{i}) is Relation-like V29() set
K19(K20({0},{i})) is V29() V33() set
k ^ <%i%> is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
len k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() set
len <%i%> 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%> 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 ^ <%i%>) 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 (k ^ <%i%>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
(len 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
dom (k ^ <%i%>) 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)
dom pp is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of K19(NAT)
h . ((len k) + 1) is set
pp . (len k) is Relation-like Function-like set
aSeq ((intloc 1),((len k) + 1)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
pr1 is ext-real V14() V15() integer set
aSeq ((intloc 2),pr1) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
(aSeq ((intloc 1),((len k) + 1))) ^ (aSeq ((intloc 2),pr1)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
((aSeq ((intloc 1),((len k) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((l,(intloc 1)) := (intloc 2))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
pp0 is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like V29() initial Function-yielding V141() set
FlattenSeq pp0 is T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0) is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) 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 (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
pp0 is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like V29() initial Function-yielding V141() set
FlattenSeq pp0 is T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0) is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) 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 (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
(((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))) is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len 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
dom ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
Comput (k1,i,(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,i,(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,i,(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . (IC ) is set
(k ^ <%i%>) . (len k) is set
pp0 ^ <%i%> is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
pp1 is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like V29() initial Function-yielding V141() set
FlattenSeq pp1 is T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1) is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) 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 (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
x is T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
<%x%> is non empty V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like constant V29() 1 -element initial Function-yielding V141() set
0 .--> x is non empty V5() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA ^omega -valued Function-like one-to-one constant V29() 1 -element Function-yielding V141() set
{0} --> x is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA ^omega -valued Function-like constant V29() total V41({0},{x}) Function-yielding V141() Element of K19(K20({0},{x}))
{x} is non empty V5() functional V29() V33() 1 -element set
K20({0},{x}) is Relation-like V29() set
K19(K20({0},{x})) is V29() V33() set
FlattenSeq <%x%> is T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
(FlattenSeq pp0) ^ (FlattenSeq <%x%>) is T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
(FlattenSeq pp0) ^ x is T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
Comput (k1,i,(len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
(aSeq ((intloc 2),pr1)) ^ <%((l,(intloc 1)) := (intloc 2))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
(aSeq ((intloc 1),((len k) + 1))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((l,(intloc 1)) := (intloc 2))%>) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
len ((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 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
dom ((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
len (FlattenSeq pp1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom (FlattenSeq pp1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() set
(len ((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>)) + (len (FlattenSeq pp1)) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
(FlattenSeq pp0) ^ (aSeq ((intloc 1),((len k) + 1))) is T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
((FlattenSeq pp0) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((l,(intloc 1)) := (intloc 2))%>) is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
len (((FlattenSeq pp0) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((l,(intloc 1)) := (intloc 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
dom (((FlattenSeq pp0) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((l,(intloc 1)) := (intloc 2))%>)) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
(len ((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>)) + (len (((FlattenSeq pp0) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((l,(intloc 1)) := (intloc 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
((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (((FlattenSeq pp0) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((l,(intloc 1)) := (intloc 2))%>)) is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (((FlattenSeq pp0) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((l,(intloc 1)) := (intloc 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
dom (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (((FlattenSeq pp0) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((l,(intloc 1)) := (intloc 2))%>))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((l,(intloc 1)) := (intloc 2))%>) is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((l,(intloc 1)) := (intloc 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
dom (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((l,(intloc 1)) := (intloc 2))%>)) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
len ((aSeq ((intloc 2),pr1)) ^ <%((l,(intloc 1)) := (intloc 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
dom ((aSeq ((intloc 2),pr1)) ^ <%((l,(intloc 1)) := (intloc 2))%>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
(len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + (len ((aSeq ((intloc 2),pr1)) ^ <%((l,(intloc 1)) := (intloc 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
len (aSeq ((intloc 2),pr1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom (aSeq ((intloc 2),pr1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() set
len <%((l,(intloc 1)) := (intloc 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
dom <%((l,(intloc 1)) := (intloc 2))%> 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 (aSeq ((intloc 2),pr1))) + (len <%((l,(intloc 1)) := (intloc 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
(len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + ((len (aSeq ((intloc 2),pr1))) + (len <%((l,(intloc 1)) := (intloc 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
(len (aSeq ((intloc 2),pr1))) + 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
(len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + ((len (aSeq ((intloc 2),pr1))) + 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
(len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + (len (aSeq ((intloc 2),pr1))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
((len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + (len (aSeq ((intloc 2),pr1)))) + 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
c3 is T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
(FlattenSeq pp0) ^ c3 is T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ ((FlattenSeq pp0) ^ c3) is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
(((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ c3 is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
len (aSeq ((intloc 1),((len k) + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom (aSeq ((intloc 1),((len k) + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() set
c3 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(aSeq ((intloc 1),((len k) + 1))) . c3 is set
(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c3 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
k1 . ((len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c3) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom (aSeq ((intloc 1),((len k) + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of K19(NAT)
dom ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len 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 K19(NAT)
((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) . ((len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c3) is set
((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (aSeq (l,h))) ^ <%(halt SCM+FSA)%>) . ((len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c3) is set
((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1)) is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1))) 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 (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + (len (aSeq ((intloc 1),((len 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
(((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
s1 is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) -started set
Comput (k1,s1,(len (aSeq ((intloc 1),((len k) + 1))))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,i,(len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,i,(len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))))) . (IC ) is set
rq is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(aSeq ((intloc 2),pr1)) . rq is set
(len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + rq is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
k1 . ((len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + rq) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom (aSeq ((intloc 2),pr1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of K19(NAT)
dom (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1))) 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)
(((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((aSeq ((intloc 1),((len k) + 1))) ^ (aSeq ((intloc 2),pr1))) is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
(((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1))) . ((len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + rq) is set
((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (aSeq (l,h))) ^ <%(halt SCM+FSA)%>) . ((len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + rq) is set
rq is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + rq is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() Element of NAT
s2 is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) -started set
Comput (k1,s2,rq) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,s2,rq)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,s2,rq)) . (IC ) is set
Comput (k1,i,((len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + rq)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,i,((len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + rq))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,i,((len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + rq))) . (IC ) is set
rq is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + rq 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 (k1,s1,rq) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,s1,rq)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,s1,rq)) . (IC ) is set
Comput (k1,i,((len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + rq)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,i,((len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + rq))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,i,((len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + rq))) . (IC ) is set
rq is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (k1,i,rq) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,i,rq)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,i,rq)) . (IC ) is set
(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + 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
(len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len 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
((len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + 1) - (len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) is ext-real V14() V15() integer set
rq - (len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) is ext-real V14() V15() integer set
(len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) - (len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) is ext-real V14() V15() integer set
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i 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 (k1,i,((len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,i,((len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,i,((len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i))) . (IC ) is set
((len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + 1) - (len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) is ext-real V14() V15() integer set
rq - (len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) is ext-real V14() V15() integer set
((len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + (len (aSeq ((intloc 2),pr1)))) - (len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) is ext-real V14() V15() integer set
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + i 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 (k1,i,((len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + i)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,i,((len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + i))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,i,((len ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1))))) + i))) . (IC ) is set
rq is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x) ^ rq is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
dom ((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x) 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)
dom <%((l,(intloc 1)) := (intloc 2))%> is ext-real positive non negative non empty V5() epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal 1 -element integer V66() V118() Element of K19(NAT)
len (((aSeq ((intloc 1),((len k) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((l,(intloc 1)) := (intloc 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
dom (((aSeq ((intloc 1),((len k) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((l,(intloc 1)) := (intloc 2))%>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
len ((aSeq ((intloc 1),((len k) + 1))) ^ (aSeq ((intloc 2),pr1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom ((aSeq ((intloc 1),((len k) + 1))) ^ (aSeq ((intloc 2),pr1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() set
(len ((aSeq ((intloc 1),((len k) + 1))) ^ (aSeq ((intloc 2),pr1)))) + 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
dom (((aSeq ((intloc 1),((len k) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((l,(intloc 1)) := (intloc 2))%>) 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)
((len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + (len (aSeq ((intloc 1),((len k) + 1))))) + (len (aSeq ((intloc 2),pr1))) 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 (k1,i,(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1))))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,i,(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1)))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,i,(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1)))))) . (IC ) is set
k1 /. (IC (Comput (k1,i,(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k1 . (IC (Comput (k1,i,(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (k1,(Comput (k1,i,(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k1 . (len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (aSeq (l,h))) ^ <%(halt SCM+FSA)%>) . (len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1)))) is set
(len (aSeq ((intloc 1),((len k) + 1)))) + (len (aSeq ((intloc 2),pr1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + ((len (aSeq ((intloc 1),((len k) + 1)))) + (len (aSeq ((intloc 2),pr1)))) 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 ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x) . ((len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + ((len (aSeq ((intloc 1),((len k) + 1)))) + (len (aSeq ((intloc 2),pr1))))) is set
(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + (len ((aSeq ((intloc 1),((len k) + 1))) ^ (aSeq ((intloc 2),pr1)))) 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 ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x) . ((len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + (len ((aSeq ((intloc 1),((len k) + 1))) ^ (aSeq ((intloc 2),pr1))))) is set
(len ((aSeq ((intloc 1),((len k) + 1))) ^ (aSeq ((intloc 2),pr1)))) + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(((aSeq ((intloc 1),((len k) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((l,(intloc 1)) := (intloc 2))%>) . ((len ((aSeq ((intloc 1),((len k) + 1))) ^ (aSeq ((intloc 2),pr1)))) + 0) is set
<%((l,(intloc 1)) := (intloc 2))%> . 0 is set
(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1)))) + 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 (k1,i,((len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1)))) + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Following (k1,(Comput (k1,i,(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Exec ((CurInstr (k1,(Comput (k1,i,(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1)))))))),(Comput (k1,i,(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) 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 (k1,(Comput (k1,i,(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1)))))))) 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 (k1,(Comput (k1,i,(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1))))))))) . (Comput (k1,i,(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1)))))) is set
Exec (((l,(intloc 1)) := (intloc 2)),(Comput (k1,i,(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) 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 . ((l,(intloc 1)) := (intloc 2)) 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 . ((l,(intloc 1)) := (intloc 2))) . (Comput (k1,i,(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1)))))) is set
Comput (k1,i,(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,i,(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,i,(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . (IC ) is set
(Exec (((l,(intloc 1)) := (intloc 2)),(Comput (k1,i,(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1)))))))) . (IC ) is set
succ (IC (Comput (k1,i,(len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
succ (len (((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len k) + 1)))) ^ (aSeq ((intloc 2),pr1)))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (k1,i,i) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,i,i)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,i,i)) . (IC ) is set
len (aSeq ((intloc 1),(len h))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
dom (aSeq ((intloc 1),(len h))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() set
len ((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 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
dom ((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
(len (aSeq ((intloc 1),(len 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
(aSeq (l,h)) ^ <%(halt SCM+FSA)%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ ((aSeq (l,h)) ^ <%(halt SCM+FSA)%>) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
<%(l :=<0,...,0> (intloc 1))%> ^ ((aSeq (l,h)) ^ <%(halt SCM+FSA)%>) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
(aSeq ((intloc 1),(len h))) ^ (<%(l :=<0,...,0> (intloc 1))%> ^ ((aSeq (l,h)) ^ <%(halt SCM+FSA)%>)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
<%> ( the InstructionsF of SCM+FSA ^omega) 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 the InstructionsF of SCM+FSA ^omega -valued 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
FlattenSeq (<%> ( the InstructionsF of SCM+FSA ^omega)) is T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq (<%> ( the InstructionsF of SCM+FSA ^omega))) is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq (<%> ( the InstructionsF of SCM+FSA ^omega)))) 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 (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq (<%> ( the InstructionsF of SCM+FSA ^omega)))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
len ((aSeq (l,h)) ^ <%(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 ((aSeq (l,h)) ^ <%(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 ((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>)) + (len ((aSeq (l,h)) ^ <%(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 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (k1,i,i) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,i,i)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,i,i)) . (IC ) is set
dom ((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) 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)
Comput (k1,i,(len (aSeq ((intloc 1),(len h))))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,i,(len (aSeq ((intloc 1),(len h)))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,i,(len (aSeq ((intloc 1),(len h)))))) . (IC ) is set
CurInstr (k1,(Comput (k1,i,(len (aSeq ((intloc 1),(len h))))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k1 /. (IC (Comput (k1,i,(len (aSeq ((intloc 1),(len h))))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k1 . (len (aSeq ((intloc 1),(len h)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (aSeq (l,h))) ^ <%(halt SCM+FSA)%>) . (len (aSeq ((intloc 1),(len h)))) is set
((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) . (len (aSeq ((intloc 1),(len h)))) is set
Comput (k1,i,(len ((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Following (k1,(Comput (k1,i,(len (aSeq ((intloc 1),(len h))))))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Exec ((CurInstr (k1,(Comput (k1,i,(len (aSeq ((intloc 1),(len h)))))))),(Comput (k1,i,(len (aSeq ((intloc 1),(len h))))))) 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 (k1,(Comput (k1,i,(len (aSeq ((intloc 1),(len h)))))))) 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 (k1,(Comput (k1,i,(len (aSeq ((intloc 1),(len h))))))))) . (Comput (k1,i,(len (aSeq ((intloc 1),(len h)))))) is set
Exec ((l :=<0,...,0> (intloc 1)),(Comput (k1,i,(len (aSeq ((intloc 1),(len h))))))) 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 . (l :=<0,...,0> (intloc 1)) 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 . (l :=<0,...,0> (intloc 1))) . (Comput (k1,i,(len (aSeq ((intloc 1),(len h)))))) is set
IC (Comput (k1,i,(len ((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,i,(len ((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>)))) . (IC ) is set
succ (IC (Comput (k1,i,(len (aSeq ((intloc 1),(len h))))))) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (k1,i,i) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,i,i)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,i,i)) . (IC ) is set
<%> the InstructionsF of SCM+FSA 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 the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like one-to-one constant functional V29() V30() V33() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered integer V69() initial halt-free V118() Function-yielding V141() V156() set
((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (<%> the InstructionsF of SCM+FSA) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ {} is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (k1,i,i) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,i,i)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,i,i)) . (IC ) is set
Comput (k1,i,(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (k1,i,(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (k1,i,(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))))) . (IC ) is set
i is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like V29() initial Function-yielding V141() set
FlattenSeq i is T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq i) is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial Element of the InstructionsF of SCM+FSA ^omega
len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq i)) 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 (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq i)) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V66() V118() set
CurInstr (k1,(Comput (k1,i,(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k1 /. (IC (Comput (k1,i,(len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k1 . (len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (aSeq (l,h))) ^ <%(halt SCM+FSA)%>) . (len (((aSeq ((intloc 1),(len h))) ^ <%(l :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))) is set
a is FinSeq-Location
k is Relation-like NAT -defined INT -valued Function-like V29() FinSequence-like FinSubsequence-like FinSequence of INT
a := k is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() set
len k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
aSeq ((intloc 1),(len k)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
a :=<0,...,0> (intloc 1) is 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
<*(intloc 1),a*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
<*(intloc 1)*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,(intloc 1)] is set
{1,(intloc 1)} is non empty V29() set
{{1,(intloc 1)},{1}} is non empty V29() V33() V66() V67() set
{[1,(intloc 1)]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is set
{1,a} is non empty V29() set
{{1,a},{1}} is non empty V29() V33() V66() V67() set
{[1,a]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*(intloc 1)*> ^ <*a*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
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
K68(12,{},<*(intloc 1),a*>) is set
<%(a :=<0,...,0> (intloc 1))%> 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 :=<0,...,0> (intloc 1)) 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 :=<0,...,0> (intloc 1)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41({0},{(a :=<0,...,0> (intloc 1))}) Element of K19(K20({0},{(a :=<0,...,0> (intloc 1))}))
{(a :=<0,...,0> (intloc 1))} is non empty V5() V29() 1 -element set
K20({0},{(a :=<0,...,0> (intloc 1))}) is Relation-like V29() set
K19(K20({0},{(a :=<0,...,0> (intloc 1))})) is V29() V33() set
(aSeq ((intloc 1),(len k))) ^ <%(a :=<0,...,0> (intloc 1))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
aSeq (a,k) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
((aSeq ((intloc 1),(len k))) ^ <%(a :=<0,...,0> (intloc 1))%>) ^ (aSeq (a,k)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
(((aSeq ((intloc 1),(len k))) ^ <%(a :=<0,...,0> (intloc 1))%>) ^ (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 FinSeq-Location
k is Relation-like NAT -defined INT -valued Function-like V29() FinSequence-like FinSubsequence-like FinSequence of INT
a := k is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
len k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
aSeq ((intloc 1),(len k)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
a :=<0,...,0> (intloc 1) is 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
<*(intloc 1),a*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
<*a*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is set
{1,a} is non empty V29() set
{{1,a},{1}} is non empty V29() V33() V66() V67() set
{[1,a]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*(intloc 1)*> ^ <*a*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
K68(12,{},<*(intloc 1),a*>) is set
<%(a :=<0,...,0> (intloc 1))%> 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 :=<0,...,0> (intloc 1)) 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 :=<0,...,0> (intloc 1)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41({0},{(a :=<0,...,0> (intloc 1))}) Element of K19(K20({0},{(a :=<0,...,0> (intloc 1))}))
{(a :=<0,...,0> (intloc 1))} is non empty V5() V29() 1 -element set
K20({0},{(a :=<0,...,0> (intloc 1))}) is Relation-like V29() set
K19(K20({0},{(a :=<0,...,0> (intloc 1))})) is V29() V33() set
(aSeq ((intloc 1),(len k))) ^ <%(a :=<0,...,0> (intloc 1))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
aSeq (a,k) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
((aSeq ((intloc 1),(len k))) ^ <%(a :=<0,...,0> (intloc 1))%>) ^ (aSeq (a,k)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
(((aSeq ((intloc 1),(len k))) ^ <%(a :=<0,...,0> (intloc 1))%>) ^ (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
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
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 FinSeq-Location
k1 is Relation-like NAT -defined INT -valued Function-like V29() FinSequence-like FinSubsequence-like FinSequence of INT
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
len k1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
aSeq ((intloc 1),(len k1)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
i :=<0,...,0> (intloc 1) is 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
<*(intloc 1),i*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
<*i*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,i] is set
{1,i} is non empty V29() set
{{1,i},{1}} is non empty V29() V33() V66() V67() set
{[1,i]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*(intloc 1)*> ^ <*i*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
K68(12,{},<*(intloc 1),i*>) is set
<%(i :=<0,...,0> (intloc 1))%> 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 :=<0,...,0> (intloc 1)) 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 :=<0,...,0> (intloc 1)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41({0},{(i :=<0,...,0> (intloc 1))}) Element of K19(K20({0},{(i :=<0,...,0> (intloc 1))}))
{(i :=<0,...,0> (intloc 1))} is non empty V5() V29() 1 -element set
K20({0},{(i :=<0,...,0> (intloc 1))}) is Relation-like V29() set
K19(K20({0},{(i :=<0,...,0> (intloc 1))})) is V29() V33() set
(aSeq ((intloc 1),(len k1))) ^ <%(i :=<0,...,0> (intloc 1))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
aSeq (i,k1) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
((aSeq ((intloc 1),(len k1))) ^ <%(i :=<0,...,0> (intloc 1))%>) ^ (aSeq (i,k1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
(((aSeq ((intloc 1),(len k1))) ^ <%(i :=<0,...,0> (intloc 1))%>) ^ (aSeq (i,k1))) ^ <%(halt SCM+FSA)%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial 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 Relation-like NAT -defined INT -valued Function-like V29() FinSequence-like FinSubsequence-like FinSequence of INT
(k +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) is ext-real V14() V15() integer set
k 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)),k) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
(Result ((a +* (i := k1)),k)) . i is Relation-like NAT -defined INT -valued Function-like V29() FinSequence-like FinSubsequence-like FinSequence of INT
l is V65() non read-only Element of the carrier of SCM+FSA
(IExec ((i := k1),a,k)) . l is ext-real V14() V15() integer set
Result ((a +* (i := k1)),(k +* (Initialize ((intloc 0) .--> 1)))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
(Result ((a +* (i := k1)),(k +* (Initialize ((intloc 0) .--> 1))))) . l is ext-real V14() V15() integer set
k . l is ext-real V14() V15() integer set
k . l is ext-real V14() V15() integer set
l is FinSeq-Location
(IExec ((i := k1),a,k)) . l is Relation-like NAT -defined INT -valued Function-like V29() FinSequence-like FinSubsequence-like FinSequence of INT
k . l is Relation-like NAT -defined INT -valued Function-like V29() FinSequence-like FinSubsequence-like FinSequence of INT
(Result ((a +* (i := k1)),(k +* (Initialize ((intloc 0) .--> 1))))) . l is Relation-like NAT -defined INT -valued Function-like V29() FinSequence-like FinSubsequence-like FinSequence of INT
k . l is Relation-like NAT -defined INT -valued Function-like V29() FinSequence-like FinSubsequence-like FinSequence of INT
a is V65() Element of the carrier of SCM+FSA
k is V65() Element of the carrier of SCM+FSA
a := k 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 is V65() Element of the carrier of SCM+FSA
AddTo (a,i) 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 is V65() Element of the carrier of SCM+FSA
SubFrom (a,k1) 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 V65() Element of the carrier of SCM+FSA
MultBy (a,k) 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 V65() Element of the carrier of SCM+FSA
Divide (a,l) 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 V65() Element of the carrier of SCM+FSA
Divide (h,a) 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
q is V65() Element of the carrier of SCM+FSA
q0 is FinSeq-Location
a := (q0,q) is 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
<*a,q0,q*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*a*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is set
{1,a} is non empty V29() set
{{1,a},{1}} is non empty V29() V33() V66() V67() set
{[1,a]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*q0*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,q0] is set
{1,q0} is non empty V29() set
{{1,q0},{1}} is non empty V29() V33() V66() V67() set
{[1,q0]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*q0*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*q*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,q] is set
{1,q} is non empty V29() set
{{1,q},{1}} is non empty V29() V33() V66() V67() set
{[1,q]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*a*> ^ <*q0*>) ^ <*q*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(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
K68(9,{},<*a,q0,q*>) is set
q is FinSeq-Location
a :=len q is 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
<*a,q*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
<*q*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,q] is set
{1,q} is non empty V29() set
{{1,q},{1}} is non empty V29() V33() V66() V67() set
{[1,q]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*q*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
K68(11,{},<*a,q*>) is set
a is V65() Element of the carrier of SCM+FSA
k is V65() Element of the carrier of SCM+FSA
i is V65() Element of the carrier of SCM+FSA
k := i 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 is V65() Element of the carrier of SCM+FSA
a := k1 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
InsCode (k := i) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() V144(3, SCM+FSA ) Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
AddTo (a,k1) 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
SubFrom (a,k1) 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
MultBy (a,k1) 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
Divide (a,k1) 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
Divide (k1,a) 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 FinSeq-Location
a := (l,k1) is 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
<*a,l,k1*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*a*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is set
{1,a} is non empty V29() set
{{1,a},{1}} is non empty V29() V33() V66() V67() set
{[1,a]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*l*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,l] is set
{1,l} is non empty V29() set
{{1,l},{1}} is non empty V29() V33() V66() V67() set
{[1,l]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*l*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*k1*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k1] is set
{1,k1} is non empty V29() set
{{1,k1},{1}} is non empty V29() V33() V66() V67() set
{[1,k1]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*a*> ^ <*l*>) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(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
K68(9,{},<*a,l,k1*>) is set
a :=len l is 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
<*a,l*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
K68(11,{},<*a,l*>) is set
a is V65() Element of the carrier of SCM+FSA
k is V65() Element of the carrier of SCM+FSA
i is V65() Element of the carrier of SCM+FSA
AddTo (k,i) 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
InsCode (AddTo (k,i)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() V144(3, SCM+FSA ) Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k1 is V65() Element of the carrier of SCM+FSA
a := k1 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
AddTo (a,k1) 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
SubFrom (a,k1) 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
MultBy (a,k1) 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
Divide (a,k1) 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
Divide (k1,a) 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 FinSeq-Location
a := (l,k1) is 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
<*a,l,k1*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*a*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is set
{1,a} is non empty V29() set
{{1,a},{1}} is non empty V29() V33() V66() V67() set
{[1,a]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*l*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,l] is set
{1,l} is non empty V29() set
{{1,l},{1}} is non empty V29() V33() V66() V67() set
{[1,l]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*l*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*k1*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k1] is set
{1,k1} is non empty V29() set
{{1,k1},{1}} is non empty V29() V33() V66() V67() set
{[1,k1]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*a*> ^ <*l*>) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(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
K68(9,{},<*a,l,k1*>) is set
a :=len l is 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
<*a,l*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
K68(11,{},<*a,l*>) is set
a is V65() Element of the carrier of SCM+FSA
k is V65() Element of the carrier of SCM+FSA
i is V65() Element of the carrier of SCM+FSA
SubFrom (k,i) 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
InsCode (SubFrom (k,i)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() V144(3, SCM+FSA ) Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k1 is V65() Element of the carrier of SCM+FSA
a := k1 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
AddTo (a,k1) 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
SubFrom (a,k1) 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
MultBy (a,k1) 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
Divide (a,k1) 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
Divide (k1,a) 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 FinSeq-Location
a := (l,k1) is 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
<*a,l,k1*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*a*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is set
{1,a} is non empty V29() set
{{1,a},{1}} is non empty V29() V33() V66() V67() set
{[1,a]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*l*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,l] is set
{1,l} is non empty V29() set
{{1,l},{1}} is non empty V29() V33() V66() V67() set
{[1,l]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*l*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*k1*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k1] is set
{1,k1} is non empty V29() set
{{1,k1},{1}} is non empty V29() V33() V66() V67() set
{[1,k1]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*a*> ^ <*l*>) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(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
K68(9,{},<*a,l,k1*>) is set
a :=len l is 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
<*a,l*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
K68(11,{},<*a,l*>) is set
a is V65() Element of the carrier of SCM+FSA
k is V65() Element of the carrier of SCM+FSA
i is V65() Element of the carrier of SCM+FSA
MultBy (k,i) 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
InsCode (MultBy (k,i)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() V144(3, SCM+FSA ) Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k1 is V65() Element of the carrier of SCM+FSA
a := k1 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
AddTo (a,k1) 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
SubFrom (a,k1) 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
MultBy (a,k1) 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
Divide (a,k1) 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
Divide (k1,a) 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 FinSeq-Location
a := (l,k1) is 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
<*a,l,k1*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*a*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is set
{1,a} is non empty V29() set
{{1,a},{1}} is non empty V29() V33() V66() V67() set
{[1,a]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*l*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,l] is set
{1,l} is non empty V29() set
{{1,l},{1}} is non empty V29() V33() V66() V67() set
{[1,l]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*l*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*k1*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k1] is set
{1,k1} is non empty V29() set
{{1,k1},{1}} is non empty V29() V33() V66() V67() set
{[1,k1]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*a*> ^ <*l*>) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(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
K68(9,{},<*a,l,k1*>) is set
a :=len l is 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
<*a,l*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
K68(11,{},<*a,l*>) is set
a is V65() Element of the carrier of SCM+FSA
k is V65() Element of the carrier of SCM+FSA
i is V65() Element of the carrier of SCM+FSA
Divide (k,i) 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
InsCode (Divide (k,i)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() V144(3, SCM+FSA ) Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k1 is V65() Element of the carrier of SCM+FSA
a := k1 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
AddTo (a,k1) 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
SubFrom (a,k1) 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
MultBy (a,k1) 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
Divide (k1,a) 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
Divide (a,k1) 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 FinSeq-Location
a := (l,k1) is 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
<*a,l,k1*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*a*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is set
{1,a} is non empty V29() set
{{1,a},{1}} is non empty V29() V33() V66() V67() set
{[1,a]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*l*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,l] is set
{1,l} is non empty V29() set
{{1,l},{1}} is non empty V29() V33() V66() V67() set
{[1,l]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*l*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*k1*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k1] is set
{1,k1} is non empty V29() set
{{1,k1},{1}} is non empty V29() V33() V66() V67() set
{[1,k1]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*a*> ^ <*l*>) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(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
K68(9,{},<*a,l,k1*>) is set
a :=len l is 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
<*a,l*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
K68(11,{},<*a,l*>) is set
a is V65() Element of the carrier of SCM+FSA
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
goto k 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(k) is Element of the InstructionsF of K568()
i is V65() Element of the carrier of SCM+FSA
a := i 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 is V65() Element of the carrier of SCM+FSA
AddTo (a,k1) 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 V65() Element of the carrier of SCM+FSA
SubFrom (a,k) 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 V65() Element of the carrier of SCM+FSA
MultBy (a,l) 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 V65() Element of the carrier of SCM+FSA
Divide (a,h) 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
q is V65() Element of the carrier of SCM+FSA
Divide (q,a) 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
q0 is V65() Element of the carrier of SCM+FSA
q is FinSeq-Location
a := (q,q0) is 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
<*a,q,q0*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*a*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is set
{1,a} is non empty V29() set
{{1,a},{1}} is non empty V29() V33() V66() V67() set
{[1,a]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*q*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,q] is set
{1,q} is non empty V29() set
{{1,q},{1}} is non empty V29() V33() V66() V67() set
{[1,q]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*q*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*q0*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,q0] is set
{1,q0} is non empty V29() set
{{1,q0},{1}} is non empty V29() V33() V66() V67() set
{[1,q0]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*a*> ^ <*q*>) ^ <*q0*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(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
K68(9,{},<*a,q,q0*>) is set
pp is FinSeq-Location
a :=len pp is 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
<*a,pp*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
<*pp*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,pp] is set
{1,pp} is non empty V29() set
{{1,pp},{1}} is non empty V29() V33() V66() V67() set
{[1,pp]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*pp*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
K68(11,{},<*a,pp*>) is set
k is V65() Element of the carrier of SCM+FSA
a is V65() Element of the carrier of SCM+FSA
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
k =0_goto i 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
k1 is V65() Element of the carrier of SCM+FSA
a := k1 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 V65() Element of the carrier of SCM+FSA
AddTo (a,k) 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 V65() Element of the carrier of SCM+FSA
SubFrom (a,l) 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 V65() Element of the carrier of SCM+FSA
MultBy (a,h) 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
q is V65() Element of the carrier of SCM+FSA
Divide (a,q) 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
q0 is V65() Element of the carrier of SCM+FSA
Divide (q0,a) 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
q is V65() Element of the carrier of SCM+FSA
pp is FinSeq-Location
a := (pp,q) is 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
<*a,pp,q*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*a*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is set
{1,a} is non empty V29() set
{{1,a},{1}} is non empty V29() V33() V66() V67() set
{[1,a]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*pp*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,pp] is set
{1,pp} is non empty V29() set
{{1,pp},{1}} is non empty V29() V33() V66() V67() set
{[1,pp]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*pp*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*q*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,q] is set
{1,q} is non empty V29() set
{{1,q},{1}} is non empty V29() V33() V66() V67() set
{[1,q]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*a*> ^ <*pp*>) ^ <*q*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(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
K68(9,{},<*a,pp,q*>) is set
k is FinSeq-Location
a :=len k is 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
<*a,k*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
<*k*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k] is set
{1,k} is non empty V29() set
{{1,k},{1}} is non empty V29() V33() V66() V67() set
{[1,k]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*k*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
K68(11,{},<*a,k*>) is set
k is V65() Element of the carrier of SCM+FSA
a is V65() Element of the carrier of SCM+FSA
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
k >0_goto i 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
k1 is V65() Element of the carrier of SCM+FSA
a := k1 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 V65() Element of the carrier of SCM+FSA
AddTo (a,k) 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 V65() Element of the carrier of SCM+FSA
SubFrom (a,l) 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 V65() Element of the carrier of SCM+FSA
MultBy (a,h) 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
q is V65() Element of the carrier of SCM+FSA
Divide (a,q) 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
q0 is V65() Element of the carrier of SCM+FSA
Divide (q0,a) 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
q is V65() Element of the carrier of SCM+FSA
pp is FinSeq-Location
a := (pp,q) is 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
<*a,pp,q*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*a*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is set
{1,a} is non empty V29() set
{{1,a},{1}} is non empty V29() V33() V66() V67() set
{[1,a]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*pp*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,pp] is set
{1,pp} is non empty V29() set
{{1,pp},{1}} is non empty V29() V33() V66() V67() set
{[1,pp]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*pp*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*q*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,q] is set
{1,q} is non empty V29() set
{{1,q},{1}} is non empty V29() V33() V66() V67() set
{[1,q]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*a*> ^ <*pp*>) ^ <*q*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(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
K68(9,{},<*a,pp,q*>) is set
k is FinSeq-Location
a :=len k is 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
<*a,k*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
<*k*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k] is set
{1,k} is non empty V29() set
{{1,k},{1}} is non empty V29() V33() V66() V67() set
{[1,k]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*k*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
K68(11,{},<*a,k*>) is set
a is V65() Element of the carrier of SCM+FSA
k is V65() Element of the carrier of SCM+FSA
i is V65() Element of the carrier of SCM+FSA
k1 is FinSeq-Location
k := (k1,i) is 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
<*k,k1,i*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*k*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k] is set
{1,k} is non empty V29() set
{{1,k},{1}} is non empty V29() V33() V66() V67() set
{[1,k]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*k1*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k1] is set
{1,k1} is non empty V29() set
{{1,k1},{1}} is non empty V29() V33() V66() V67() set
{[1,k1]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*k*> ^ <*k1*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*i*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,i] is set
{1,i} is non empty V29() set
{{1,i},{1}} is non empty V29() V33() V66() V67() set
{[1,i]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*k*> ^ <*k1*>) ^ <*i*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(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
K68(9,{},<*k,k1,i*>) is set
InsCode (k := (k1,i)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() V144(3, SCM+FSA ) Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k is V65() Element of the carrier of SCM+FSA
a := k 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
AddTo (a,k) 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
SubFrom (a,k) 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
MultBy (a,k) 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
Divide (a,k) 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
Divide (k,a) 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 FinSeq-Location
a := (h,k) is 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
<*a,h,k*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*a*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is set
{1,a} is non empty V29() set
{{1,a},{1}} is non empty V29() V33() V66() V67() set
{[1,a]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*h*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,h] is set
{1,h} is non empty V29() set
{{1,h},{1}} is non empty V29() V33() V66() V67() set
{[1,h]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*h*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*k*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k] is set
{1,k} is non empty V29() set
{{1,k},{1}} is non empty V29() V33() V66() V67() set
{[1,k]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*a*> ^ <*h*>) ^ <*k*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
K68(9,{},<*a,h,k*>) is set
a :=len h is 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
<*a,h*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
K68(11,{},<*a,h*>) is set
k is V65() Element of the carrier of SCM+FSA
i is V65() Element of the carrier of SCM+FSA
a is V65() Element of the carrier of SCM+FSA
k1 is FinSeq-Location
(k1,i) := k is 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
<*k,k1,i*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*k*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k] is set
{1,k} is non empty V29() set
{{1,k},{1}} is non empty V29() V33() V66() V67() set
{[1,k]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*k1*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k1] is set
{1,k1} is non empty V29() set
{{1,k1},{1}} is non empty V29() V33() V66() V67() set
{[1,k1]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*k*> ^ <*k1*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*i*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,i] is set
{1,i} is non empty V29() set
{{1,i},{1}} is non empty V29() V33() V66() V67() set
{[1,i]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*k*> ^ <*k1*>) ^ <*i*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(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
K68(10,{},<*k,k1,i*>) is set
InsCode ((k1,i) := k) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() V144(3, SCM+FSA ) Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k is V65() Element of the carrier of SCM+FSA
a := k 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
AddTo (a,k) 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
SubFrom (a,k) 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
MultBy (a,k) 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
Divide (k,a) 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
Divide (a,k) 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 FinSeq-Location
a := (l,k) is 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
<*a,l,k*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*a*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is set
{1,a} is non empty V29() set
{{1,a},{1}} is non empty V29() V33() V66() V67() set
{[1,a]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*l*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,l] is set
{1,l} is non empty V29() set
{{1,l},{1}} is non empty V29() V33() V66() V67() set
{[1,l]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*l*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*k*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k] is set
{1,k} is non empty V29() set
{{1,k},{1}} is non empty V29() V33() V66() V67() set
{[1,k]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*a*> ^ <*l*>) ^ <*k*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
K68(9,{},<*a,l,k*>) is set
a :=len l is 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
<*a,l*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
K68(11,{},<*a,l*>) is set
a is V65() Element of the carrier of SCM+FSA
k is V65() Element of the carrier of SCM+FSA
i is FinSeq-Location
k :=len i is 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
<*k,i*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
<*k*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k] is set
{1,k} is non empty V29() set
{{1,k},{1}} is non empty V29() V33() V66() V67() set
{[1,k]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*i*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,i] is set
{1,i} is non empty V29() set
{{1,i},{1}} is non empty V29() V33() V66() V67() set
{[1,i]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*k*> ^ <*i*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
K68(11,{},<*k,i*>) is set
InsCode (k :=len i) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() V144(3, SCM+FSA ) Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k1 is V65() Element of the carrier of SCM+FSA
a := k1 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
AddTo (a,k1) 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
SubFrom (a,k1) 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
MultBy (a,k1) 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
Divide (a,k1) 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
Divide (k1,a) 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 FinSeq-Location
a := (k,k1) is 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
<*a,k,k1*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*a*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is set
{1,a} is non empty V29() set
{{1,a},{1}} is non empty V29() V33() V66() V67() set
{[1,a]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*k*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k] is set
{1,k} is non empty V29() set
{{1,k},{1}} is non empty V29() V33() V66() V67() set
{[1,k]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*k*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*k1*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k1] is set
{1,k1} is non empty V29() set
{{1,k1},{1}} is non empty V29() V33() V66() V67() set
{[1,k1]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*a*> ^ <*k*>) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(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
K68(9,{},<*a,k,k1*>) is set
a :=len k is 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
<*a,k*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
K68(11,{},<*a,k*>) is set
k is V65() Element of the carrier of SCM+FSA
a is V65() Element of the carrier of SCM+FSA
i is FinSeq-Location
i :=<0,...,0> k is 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
<*k,i*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
<*k*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k] is set
{1,k} is non empty V29() set
{{1,k},{1}} is non empty V29() V33() V66() V67() set
{[1,k]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*i*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,i] is set
{1,i} is non empty V29() set
{{1,i},{1}} is non empty V29() V33() V66() V67() set
{[1,i]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*k*> ^ <*i*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
K68(12,{},<*k,i*>) is set
InsCode (i :=<0,...,0> k) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() V144(3, SCM+FSA ) Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k1 is V65() Element of the carrier of SCM+FSA
a := k1 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
AddTo (a,k1) 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
SubFrom (a,k1) 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
MultBy (a,k1) 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
Divide (a,k1) 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
Divide (k1,a) 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 FinSeq-Location
a := (k,k1) is 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
<*a,k,k1*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*a*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is set
{1,a} is non empty V29() set
{{1,a},{1}} is non empty V29() V33() V66() V67() set
{[1,a]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*k*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k] is set
{1,k} is non empty V29() set
{{1,k},{1}} is non empty V29() V33() V66() V67() set
{[1,k]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*a*> ^ <*k*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*k1*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k1] is set
{1,k1} is non empty V29() set
{{1,k1},{1}} is non empty V29() V33() V66() V67() set
{[1,k1]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*a*> ^ <*k*>) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(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
K68(9,{},<*a,k,k1*>) is set
a :=len k is 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
<*a,k*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
K68(11,{},<*a,k*>) is set
a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
k is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
i +* a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialize k is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
k +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
k1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput ((i +* a),(Initialize k),k1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput ((i +* a),(Initialize k),k1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput ((i +* a),(Initialize k),k1)) . (IC ) is set
dom 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)
k is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
K360(NAT,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)
i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
k1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (i,k,k1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
IC (Comput (i,k,k1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput (i,k,k1)) . (IC ) is set
i +* a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialize k is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
k +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
dom 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)
k is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
i is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
k1 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
k1 +* k 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 K274(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 K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started 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
k1 +* k 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 K274(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 K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
a is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k is V65() Element of the carrier of SCM+FSA
i is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Exec (a,i) 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 . a 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 . a) . i is set
(Exec (a,i)) . k is ext-real V14() V15() integer set
i . k is ext-real V14() V15() integer set
InsCode a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
InsCode a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k1 is V65() Element of the carrier of SCM+FSA
k is V65() Element of the carrier of SCM+FSA
k1 := k 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
InsCode a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k1 is V65() Element of the carrier of SCM+FSA
k is V65() Element of the carrier of SCM+FSA
AddTo (k1,k) 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
InsCode a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k1 is V65() Element of the carrier of SCM+FSA
k is V65() Element of the carrier of SCM+FSA
SubFrom (k1,k) 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
InsCode a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k1 is V65() Element of the carrier of SCM+FSA
k is V65() Element of the carrier of SCM+FSA
MultBy (k1,k) 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
InsCode a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k1 is V65() Element of the carrier of SCM+FSA
k is V65() Element of the carrier of SCM+FSA
Divide (k1,k) 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
InsCode a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
goto k1 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(k1) is Element of the InstructionsF of K568()
InsCode a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
k is V65() Element of the carrier of SCM+FSA
k =0_goto k1 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
InsCode a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
k is V65() Element of the carrier of SCM+FSA
k >0_goto k1 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
InsCode a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k is V65() Element of the carrier of SCM+FSA
k1 is V65() Element of the carrier of SCM+FSA
l is FinSeq-Location
k := (l,k1) is 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
<*k,l,k1*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*k*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k] is set
{1,k} is non empty V29() set
{{1,k},{1}} is non empty V29() V33() V66() V67() set
{[1,k]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*l*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,l] is set
{1,l} is non empty V29() set
{{1,l},{1}} is non empty V29() V33() V66() V67() set
{[1,l]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*k*> ^ <*l*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*k1*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k1] is set
{1,k1} is non empty V29() set
{{1,k1},{1}} is non empty V29() V33() V66() V67() set
{[1,k1]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*k*> ^ <*l*>) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(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
K68(9,{},<*k,l,k1*>) is set
InsCode a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k is V65() Element of the carrier of SCM+FSA
k1 is V65() Element of the carrier of SCM+FSA
l is FinSeq-Location
(l,k1) := k is 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
<*k,l,k1*> is non empty Relation-like NAT -defined Function-like V29() 3 -element FinSequence-like FinSubsequence-like set
<*k*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k] is set
{1,k} is non empty V29() set
{{1,k},{1}} is non empty V29() V33() V66() V67() set
{[1,k]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*l*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,l] is set
{1,l} is non empty V29() set
{{1,l},{1}} is non empty V29() V33() V66() V67() set
{[1,l]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*k*> ^ <*l*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
<*k1*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k1] is set
{1,k1} is non empty V29() set
{{1,k1},{1}} is non empty V29() V33() V66() V67() set
{[1,k1]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
(<*k*> ^ <*l*>) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V29() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(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
K68(10,{},<*k,l,k1*>) is set
InsCode a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k1 is V65() Element of the carrier of SCM+FSA
k is FinSeq-Location
k1 :=len k is 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
<*k1,k*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
<*k1*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k1] is set
{1,k1} is non empty V29() set
{{1,k1},{1}} is non empty V29() V33() V66() V67() set
{[1,k1]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*k*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k] is set
{1,k} is non empty V29() set
{{1,k},{1}} is non empty V29() V33() V66() V67() set
{[1,k]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*k1*> ^ <*k*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
K68(11,{},<*k1,k*>) is set
InsCode a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
k1 is V65() Element of the carrier of SCM+FSA
k is FinSeq-Location
k :=<0,...,0> k1 is 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
<*k1,k*> is non empty Relation-like NAT -defined Function-like V29() 2 -element FinSequence-like FinSubsequence-like set
<*k1*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k1] is set
{1,k1} is non empty V29() set
{{1,k1},{1}} is non empty V29() V33() V66() V67() set
{[1,k1]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*k*> is non empty V5() Relation-like NAT -defined Function-like constant V29() 1 -element FinSequence-like FinSubsequence-like set
[1,k] is set
{1,k} is non empty V29() set
{{1,k},{1}} is non empty V29() V33() V66() V67() set
{[1,k]} is non empty V5() Relation-like Function-like constant V29() 1 -element set
<*k1*> ^ <*k*> is non empty Relation-like NAT -defined Function-like V29() 1 + 1 -element FinSequence-like FinSubsequence-like set
K68(12,{},<*k1,k*>) is set
InsCode a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
Initialize a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
a +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
k is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
i is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
k +* i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
k1 is V65() Element of the carrier of SCM+FSA
a . k1 is ext-real V14() V15() integer set
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput ((k +* i),(Initialize a),k) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
(Comput ((k +* i),(Initialize a),k)) . k1 is ext-real V14() V15() integer set
IC (Comput ((k +* i),(Initialize a),k)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
(Comput ((k +* i),(Initialize a),k)) . (IC ) is set
dom i 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)
(k +* i) . (IC (Comput ((k +* i),(Initialize a),k))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i . (IC (Comput ((k +* i),(Initialize a),k))) is set
rng i is non empty V29() set
dom (k +* i) is non empty V118() set
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
Comput ((k +* i),(Initialize a),(k + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
(Comput ((k +* i),(Initialize a),(k + 1))) . k1 is ext-real V14() V15() integer set
Following ((k +* i),(Comput ((k +* i),(Initialize a),k))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
CurInstr ((k +* i),(Comput ((k +* i),(Initialize a),k))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(k +* i) /. (IC (Comput ((k +* i),(Initialize a),k))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr ((k +* i),(Comput ((k +* i),(Initialize a),k)))),(Comput ((k +* i),(Initialize a),k))) 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 +* i),(Comput ((k +* i),(Initialize a),k)))) 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 +* i),(Comput ((k +* i),(Initialize a),k))))) . (Comput ((k +* i),(Initialize a),k)) is set
(Following ((k +* i),(Comput ((k +* i),(Initialize a),k)))) . k1 is ext-real V14() V15() integer set
Exec (((k +* i) . (IC (Comput ((k +* i),(Initialize a),k)))),(Comput ((k +* i),(Initialize a),k))) 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 . ((k +* i) . (IC (Comput ((k +* i),(Initialize a),k)))) 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 . ((k +* i) . (IC (Comput ((k +* i),(Initialize a),k))))) . (Comput ((k +* i),(Initialize a),k)) is set
(Exec (((k +* i) . (IC (Comput ((k +* i),(Initialize a),k)))),(Comput ((k +* i),(Initialize a),k)))) . k1 is ext-real V14() V15() integer set
Comput ((k +* i),(a +* (Start-At (0,SCM+FSA))),k) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
(Comput ((k +* i),(a +* (Start-At (0,SCM+FSA))),k)) . k1 is ext-real V14() V15() integer set
dom (Start-At (0,SCM+FSA)) is non empty V29() set
Comput ((k +* i),(Initialize a),0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
(Comput ((k +* i),(Initialize a),0)) . k1 is ext-real V14() V15() integer set
(Initialize a) . k1 is ext-real V14() V15() integer 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
dom (Stop 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() Element of K19(NAT)
dom (Start-At (0,SCM+FSA)) is non empty V29() set
a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started 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
Comput (k,a,0) 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,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
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
k /. (IC (Comput (k,a,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (k,a) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
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 /. (IC a) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k . (IC a) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
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
k . (IC (Start-At (0,SCM+FSA))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
k . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Stop SCM+FSA) . 0 is set
rng (Stop SCM+FSA) 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
a is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
k is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
k . (intloc 0) is ext-real V14() V15() integer set
Initialize k is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set
k +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set
i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
k1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
Comput (i,k,k1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set
(Comput (i,k,k1)) . (intloc 0) is ext-real V14() V15() integer set
i +* a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a is V65() Element of the carrier of SCM+FSA
a := (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
AddTo (a,(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
SubFrom (a,(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
{(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} is V29() set
k is ext-real V14() V15() integer set
aSeq (a,k) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
rng (aSeq (a,k)) is V29() set
i is set
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 := (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 .--> (a := (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} --> (a := (intloc 0)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41({0},{(a := (intloc 0))}) Element of K19(K20({0},{(a := (intloc 0))}))
{(a := (intloc 0))} is non empty V5() V29() 1 -element set
K20({0},{(a := (intloc 0))}) is Relation-like V29() set
K19(K20({0},{(a := (intloc 0))})) is V29() V33() set
<%(a := (intloc 0))%> ^ {} is non empty T-Sequence-like Relation-like NAT -defined Function-like V29() initial set
k1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
k1 + 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
k1 --> (AddTo (a,(intloc 0))) is T-Sequence-like Relation-like k1 -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41(k1, the InstructionsF of SCM+FSA) initial Element of K19(K20(k1, the InstructionsF of SCM+FSA))
K20(k1, the InstructionsF of SCM+FSA) is Relation-like set
K19(K20(k1, the InstructionsF of SCM+FSA)) is set
{(AddTo (a,(intloc 0)))} is non empty V5() V29() 1 -element set
K20(k1,{(AddTo (a,(intloc 0)))}) is Relation-like V29() set
<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
{(a := (intloc 0))} 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
<%(a := (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 .--> (a := (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} --> (a := (intloc 0)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41({0},{(a := (intloc 0))}) Element of K19(K20({0},{(a := (intloc 0))}))
{(a := (intloc 0))} is non empty V5() V29() 1 -element set
K20({0},{(a := (intloc 0))}) is Relation-like V29() set
K19(K20({0},{(a := (intloc 0))})) is V29() V33() set
k1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
k1 + 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
k1 --> (AddTo (a,(intloc 0))) is T-Sequence-like Relation-like k1 -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41(k1, the InstructionsF of SCM+FSA) initial Element of K19(K20(k1, the InstructionsF of SCM+FSA))
K20(k1, the InstructionsF of SCM+FSA) is Relation-like set
K19(K20(k1, the InstructionsF of SCM+FSA)) is set
{(AddTo (a,(intloc 0)))} is non empty V5() V29() 1 -element set
K20(k1,{(AddTo (a,(intloc 0)))}) is Relation-like V29() set
<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
rng <%(a := (intloc 0))%> is non empty V5() V29() 1 -element set
rng (k1 --> (AddTo (a,(intloc 0)))) is V5() V29() set
(rng <%(a := (intloc 0))%>) \/ (rng (k1 --> (AddTo (a,(intloc 0))))) is non empty V29() set
{(a := (intloc 0))} 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
{(a := (intloc 0))} \/ (rng (k1 --> (AddTo (a,(intloc 0))))) is non empty V29() set
{(AddTo (a,(intloc 0)))} is non empty V5() Relation-like V29() 1 -element Element of K19( the InstructionsF of SCM+FSA)
{(a := (intloc 0))} \/ {(AddTo (a,(intloc 0)))} is non empty Relation-like V29() Element of K19( the InstructionsF of SCM+FSA)
<%(a := (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 .--> (a := (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} --> (a := (intloc 0)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41({0},{(a := (intloc 0))}) Element of K19(K20({0},{(a := (intloc 0))}))
{(a := (intloc 0))} is non empty V5() V29() 1 -element set
K20({0},{(a := (intloc 0))}) is Relation-like V29() set
K19(K20({0},{(a := (intloc 0))})) is V29() V33() set
k1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() V29() cardinal integer V118() Element of NAT
k1 + k is ext-real V14() V15() integer set
k1 --> (SubFrom (a,(intloc 0))) is T-Sequence-like Relation-like k1 -defined the InstructionsF of SCM+FSA -valued Function-like constant V29() total V41(k1, the InstructionsF of SCM+FSA) initial Element of K19(K20(k1, the InstructionsF of SCM+FSA))
K20(k1, the InstructionsF of SCM+FSA) is Relation-like set
K19(K20(k1, the InstructionsF of SCM+FSA)) is set
{(SubFrom (a,(intloc 0)))} is non empty V5() V29() 1 -element set
K20(k1,{(SubFrom (a,(intloc 0)))}) is Relation-like V29() set
<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
rng <%(a := (intloc 0))%> is non empty V5() V29() 1 -element set
rng (k1 --> (SubFrom (a,(intloc 0)))) is V5() V29() set
(rng <%(a := (intloc 0))%>) \/ (rng (k1 --> (SubFrom (a,(intloc 0))))) is non empty V29() set
{(a := (intloc 0))} 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
{(a := (intloc 0))} \/ (rng (k1 --> (SubFrom (a,(intloc 0))))) is non empty V29() set
{(SubFrom (a,(intloc 0)))} is non empty V5() Relation-like V29() 1 -element Element of K19( the InstructionsF of SCM+FSA)
{(a := (intloc 0))} \/ {(SubFrom (a,(intloc 0)))} is non empty Relation-like V29() Element of K19( the InstructionsF of SCM+FSA)
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 is V65() Element of the carrier of SCM+FSA
a := (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
AddTo (a,(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
SubFrom (a,(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
{(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} is V29() set
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 paraclosed parahalting set
rng (a := k) is non empty V29() set
aSeq (a,k) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial set
rng (aSeq (a,k)) is V29() set
{(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} is V29() 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
rng ((aSeq (a,k)) ^ <%(halt SCM+FSA)%>) is non empty V29() set
rng <%(halt SCM+FSA)%> is non empty V5() V29() 1 -element set
(rng (aSeq (a,k))) \/ (rng <%(halt SCM+FSA)%>) is non empty V29() 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 (aSeq (a,k))) \/ {(halt SCM+FSA)} is non empty V29() set
i is set
a is V65() non read-only 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 paraclosed parahalting set
rng (a := k) is non empty V29() set
a := (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
AddTo (a,(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
SubFrom (a,(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
{(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} is V29() set
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
a is V65() non read-only 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 keeping_0 paraclosed parahalting () set