:: SCMFSA6C semantic presentation

REAL is non empty V5() V40() V52() set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K32(REAL)
K32(REAL) is set
SCM+FSA is non empty V90(3) IC-Ins-separated strict V98(3) V139(3) with_explicit_jumps IC-relocable AMI-Struct over 3
3 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() Element of NAT
K530() is set
In (NAT,K530()) is Element of K530()
K523() is non empty set
K533() is Relation-like K530() -defined 3 -valued Function-like V18(K530(),3) Element of K32(K33(K530(),3))
K33(K530(),3) is Relation-like set
K32(K33(K530(),3)) is set
K534() is non empty Relation-like 3 -defined Function-like total set
K541() is Relation-like K523() -defined K99(K290((K533() * K534())),K290((K533() * K534()))) -valued Function-like V18(K523(),K99(K290((K533() * K534())),K290((K533() * K534())))) Element of K32(K33(K523(),K99(K290((K533() * K534())),K290((K533() * K534())))))
K533() * K534() is Relation-like K530() -defined Function-like total set
K290((K533() * K534())) is set
K99(K290((K533() * K534())),K290((K533() * K534()))) is set
K33(K523(),K99(K290((K533() * K534())),K290((K533() * K534())))) is Relation-like set
K32(K33(K523(),K99(K290((K533() * K534())),K290((K533() * K534()))))) is set
AMI-Struct(# K530(),(In (NAT,K530())),K523(),K533(),K534(),K541() #) is strict AMI-Struct over 3
the carrier of SCM+FSA is non empty set
COMPLEX is non empty V5() V40() V52() set
NAT is non empty epsilon-transitive epsilon-connected ordinal set
K32(NAT) is set
K32(NAT) is set
9 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() Element of NAT
Segm 9 is Element of K32(NAT)
Int-Locations is non empty set
K327() is set
K32(K327()) is set
2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() Element of NAT
K33(K327(),2) is Relation-like set
K32(K33(K327(),2)) is set
K329() is Relation-like K327() -defined 2 -valued Function-like V18(K327(),2) Element of K32(K33(K327(),2))
K330() is non empty Relation-like 2 -defined Function-like total set
K329() * K330() is Relation-like K327() -defined Function-like total set
K290((K329() * K330())) is set
K321() is non empty set
K99(K290((K329() * K330())),K290((K329() * K330()))) is set
K33(K321(),K99(K290((K329() * K330())),K290((K329() * K330())))) is Relation-like set
K32(K33(K321(),K99(K290((K329() * K330())),K290((K329() * K330()))))) is set
K32( the carrier of SCM+FSA) is set
the InstructionsF of SCM+FSA is non empty Relation-like standard-ins V60() J/A-independent V63() set
INT is non empty V5() V40() V52() set
Int-Locations is non empty Element of K32( the carrier of SCM+FSA)
K113(Int-Locations) is V24() set
K32(Int-Locations) is set
FinSeq-Locations is non empty V5() V40() V52() Element of K32( the carrier of SCM+FSA)
K532() is Element of K32(K530())
K32(K530()) is set
K113(FinSeq-Locations) is V24() set
K32(FinSeq-Locations) is set
K301(3,SCM+FSA) is non empty Relation-like non-empty non empty-yielding the carrier of SCM+FSA -defined Function-like total set
the Object-Kind of SCM+FSA is Relation-like the carrier of SCM+FSA -defined 3 -valued Function-like V18( the carrier of SCM+FSA,3) Element of K32(K33( the carrier of SCM+FSA,3))
K33( the carrier of SCM+FSA,3) is Relation-like set
K32(K33( the carrier of SCM+FSA,3)) is set
the U7 of SCM+FSA is non empty Relation-like 3 -defined Function-like total set
the Object-Kind of SCM+FSA * the U7 of SCM+FSA is non empty Relation-like the carrier of SCM+FSA -defined Function-like total set
RAT is non empty V5() V40() V52() set
K522() is set
K33(NAT,K32(NAT)) is Relation-like set
K32(K33(NAT,K32(NAT))) is set
FinPartSt SCM+FSA is non empty Element of K32(K294(K301(3,SCM+FSA)))
K294(K301(3,SCM+FSA)) is set
K32(K294(K301(3,SCM+FSA))) is set
{ b₁ where b₁ is Element of K294(K301(3,SCM+FSA)) : b₁ is V40() } is set
K33((FinPartSt SCM+FSA),(FinPartSt SCM+FSA)) is Relation-like set
K32(K33((FinPartSt SCM+FSA),(FinPartSt SCM+FSA))) is set
1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() Element of NAT
{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() V37() integer V40() V41() V44() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V149() set
0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() V37() integer V40() V41() V44() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V149() Element of NAT
12 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() Element of NAT
4 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() Element of NAT
5 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() Element of NAT
6 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() Element of NAT
7 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() Element of NAT
8 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() Element of NAT
10 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() Element of NAT
11 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() Element of NAT
IC is V77( SCM+FSA ) Element of the carrier of SCM+FSA
halt SCM+FSA is ins-loc-free ins-loc-free V97(3, SCM+FSA ) jump-only V140(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
NonZero SCM+FSA is Element of K32( the carrier of SCM+FSA)
Int-Locations \/ FinSeq-Locations is non empty Element of K32( the carrier of SCM+FSA)
K83(NAT,0,6,7,8) is V40() Element of K32(NAT)
intloc 0 is V101() read-only Element of the carrier of SCM+FSA
K81(NAT,0,1) is non empty V40() Element of K32(NAT)
K328() is non empty Element of K32(K327())
Start-At (0,SCM+FSA) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible V40() 0 -started set
(IC ) .--> 0 is V5() Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued Function-like one-to-one constant V40() Function-yielding V149() set
{(IC )} is non empty V40() set
{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued {0} -valued Function-like constant total V18({(IC )},{0}) V40() Function-yielding V149() Element of K32(K33({(IC )},{0}))
{0} is non empty functional V40() V44() set
K33({(IC )},{0}) is Relation-like V40() set
K32(K33({(IC )},{0})) is V40() V44() set
a is V101() Element of the carrier of SCM+FSA
b is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
i0 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
i1 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() keeping_0 paraclosed parahalting set
IExec (i1,i0,b) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
i0 +* i1 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialized b is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total 0 -started set
(intloc 0) .--> 1 is V5() Relation-like the carrier of SCM+FSA -defined {(intloc 0)} -defined {(intloc 0)} -defined NAT -valued Function-like one-to-one constant K301(3,SCM+FSA) -compatible V40() data-only set
{(intloc 0)} is non empty V40() set
{(intloc 0)} --> 1 is non empty Relation-like non-empty non empty-yielding {(intloc 0)} -defined NAT -valued {1} -valued Function-like constant total V18({(intloc 0)},{1}) V40() Element of K32(K33({(intloc 0)},{1}))
{1} is non empty V40() V51() V52() set
K33({(intloc 0)},{1}) is Relation-like V40() set
K32(K33({(intloc 0)},{1})) is V40() V44() set
Initialize ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible V40() 0 -started 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 K301(3,SCM+FSA) -compatible K301(3,SCM+FSA) -compatible V40() 0 -started set
b +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible K301(3,SCM+FSA) -compatible total 0 -started set
Result ((i0 +* i1),(Initialized b)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
i2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() paraclosed parahalting set
i1 ";" i2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() paraclosed parahalting set
K277(SCM+FSA,i1) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() set
Stop SCM+FSA is non empty V5() Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant V40() V58() non halt-free halt-ending unique-halt really-closed paraclosed set
K248((halt SCM+FSA)) is set
K238(i1,(Stop SCM+FSA)) is Relation-like Function-like T-Sequence-like set
K451(K277(SCM+FSA,i1)) is Relation-like Function-like set
Directed K451(K277(SCM+FSA,i1)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
card i1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
K273(SCM+FSA,i2,(card i1)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
IncAddr (i2,(card i1)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() set
K449((IncAddr (i2,(card i1))),(card i1)) is Relation-like Function-like set
(Directed K451(K277(SCM+FSA,i1))) +* K273(SCM+FSA,i2,(card i1)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
IExec ((i1 ";" i2),i0,b) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
i0 +* (i1 ";" i2) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Result ((i0 +* (i1 ";" i2)),(Initialized b)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
(IExec ((i1 ";" i2),i0,b)) . a is ext-real V36() V37() integer set
IExec (i2,i0,(IExec (i1,i0,b))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
i0 +* i2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialized (IExec (i1,i0,b)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total 0 -started set
(IExec (i1,i0,b)) +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible K301(3,SCM+FSA) -compatible total 0 -started set
Result ((i0 +* i2),(Initialized (IExec (i1,i0,b)))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
(IExec (i2,i0,(IExec (i1,i0,b)))) . a is ext-real V36() V37() integer set
IC (IExec (i2,i0,(IExec (i1,i0,b)))) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(IExec (i2,i0,(IExec (i1,i0,b)))) . (IC ) is set
(IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
Start-At (((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1)),SCM+FSA) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible V40() (IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1) -started set
(IC ) .--> ((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1)) is V5() Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued Function-like one-to-one constant V40() set
{(IC )} --> ((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1)) is non empty Relation-like {(IC )} -defined NAT -valued {((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1))} -valued Function-like constant total V18({(IC )},{((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1))}) V40() Element of K32(K33({(IC )},{((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1))}))
{((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1))} is non empty V40() set
K33({(IC )},{((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1))}) is Relation-like V40() set
K32(K33({(IC )},{((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1))})) is V40() V44() set
dom (Start-At (((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1)),SCM+FSA)) is non empty V40() set
IncIC ((IExec (i2,i0,(IExec (i1,i0,b)))),(card i1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
(IExec (i2,i0,(IExec (i1,i0,b)))) +* (Start-At (((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1)),SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible K301(3,SCM+FSA) -compatible total (IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1) -started set
a is FinSeq-Location
b is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
i0 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
i1 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() keeping_0 paraclosed parahalting set
IExec (i1,i0,b) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
i0 +* i1 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialized b is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total 0 -started set
(intloc 0) .--> 1 is V5() Relation-like the carrier of SCM+FSA -defined {(intloc 0)} -defined {(intloc 0)} -defined NAT -valued Function-like one-to-one constant K301(3,SCM+FSA) -compatible V40() data-only set
{(intloc 0)} is non empty V40() set
{(intloc 0)} --> 1 is non empty Relation-like non-empty non empty-yielding {(intloc 0)} -defined NAT -valued {1} -valued Function-like constant total V18({(intloc 0)},{1}) V40() Element of K32(K33({(intloc 0)},{1}))
{1} is non empty V40() V51() V52() set
K33({(intloc 0)},{1}) is Relation-like V40() set
K32(K33({(intloc 0)},{1})) is V40() V44() set
Initialize ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible V40() 0 -started 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 K301(3,SCM+FSA) -compatible K301(3,SCM+FSA) -compatible V40() 0 -started set
b +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible K301(3,SCM+FSA) -compatible total 0 -started set
Result ((i0 +* i1),(Initialized b)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
i2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() paraclosed parahalting set
i1 ";" i2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() paraclosed parahalting set
K277(SCM+FSA,i1) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() set
Stop SCM+FSA is non empty V5() Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant V40() V58() non halt-free halt-ending unique-halt really-closed paraclosed set
K248((halt SCM+FSA)) is set
K238(i1,(Stop SCM+FSA)) is Relation-like Function-like T-Sequence-like set
K451(K277(SCM+FSA,i1)) is Relation-like Function-like set
Directed K451(K277(SCM+FSA,i1)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
card i1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
K273(SCM+FSA,i2,(card i1)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
IncAddr (i2,(card i1)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() set
K449((IncAddr (i2,(card i1))),(card i1)) is Relation-like Function-like set
(Directed K451(K277(SCM+FSA,i1))) +* K273(SCM+FSA,i2,(card i1)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
IExec ((i1 ";" i2),i0,b) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
i0 +* (i1 ";" i2) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Result ((i0 +* (i1 ";" i2)),(Initialized b)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
(IExec ((i1 ";" i2),i0,b)) . a is Relation-like NAT -defined INT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of INT
IExec (i2,i0,(IExec (i1,i0,b))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
i0 +* i2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialized (IExec (i1,i0,b)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total 0 -started set
(IExec (i1,i0,b)) +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible K301(3,SCM+FSA) -compatible total 0 -started set
Result ((i0 +* i2),(Initialized (IExec (i1,i0,b)))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
(IExec (i2,i0,(IExec (i1,i0,b)))) . a is Relation-like NAT -defined INT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of INT
IC (IExec (i2,i0,(IExec (i1,i0,b)))) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(IExec (i2,i0,(IExec (i1,i0,b)))) . (IC ) is set
(IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
Start-At (((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1)),SCM+FSA) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible V40() (IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1) -started set
(IC ) .--> ((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1)) is V5() Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued Function-like one-to-one constant V40() set
{(IC )} --> ((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1)) is non empty Relation-like {(IC )} -defined NAT -valued {((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1))} -valued Function-like constant total V18({(IC )},{((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1))}) V40() Element of K32(K33({(IC )},{((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1))}))
{((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1))} is non empty V40() set
K33({(IC )},{((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1))}) is Relation-like V40() set
K32(K33({(IC )},{((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1))})) is V40() V44() set
dom (Start-At (((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1)),SCM+FSA)) is non empty V40() set
IncIC ((IExec (i2,i0,(IExec (i1,i0,b)))),(card i1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
(IExec (i2,i0,(IExec (i1,i0,b)))) +* (Start-At (((IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1)),SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible K301(3,SCM+FSA) -compatible total (IC (IExec (i2,i0,(IExec (i1,i0,b))))) + (card i1) -started set
Macro (halt SCM+FSA) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() set
K276(SCM+FSA,(halt SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
K277(SCM+FSA,K276(SCM+FSA,(halt SCM+FSA))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
a is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total 0 -started set
i1 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
dom (Start-At (0,SCM+FSA)) is non empty V40() set
Comput (i1,a,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
IC (Comput (i1,a,0)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (i1,a,0)) . (IC ) is set
dom i1 is non empty set
CurInstr (i1,(Comput (i1,a,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i1 /. (IC (Comput (i1,a,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom (Macro (halt SCM+FSA)) is non empty V40() set
{0,1} is non empty V40() set
CurInstr (i1,a) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC a is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
a . (IC ) is set
i1 /. (IC a) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i1 . (IC a) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Start-At (0,SCM+FSA)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Start-At (0,SCM+FSA)) . (IC ) is set
i1 . (IC (Start-At (0,SCM+FSA))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i1 . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro (halt SCM+FSA)) . 0 is set
b is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total 0 -started set
b . (intloc 0) is ext-real V36() V37() integer set
i0 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
i1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
Comput (i0,b,i1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
(Comput (i0,b,i1)) . (intloc 0) is ext-real V36() V37() integer set
IC b is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
b . (IC ) is set
i0 /. (IC b) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i0 . (IC b) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom (Macro (halt SCM+FSA)) is non empty V40() set
Comput (i0,b,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
CurInstr (i0,(Comput (i0,b,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (i0,b,0)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (i0,b,0)) . (IC ) is set
i0 /. (IC (Comput (i0,b,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i0 . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro (halt SCM+FSA)) . 0 is set
a is with_explicit_jumps IC-relocable () Element of the InstructionsF of SCM+FSA
Macro a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() set
K276(SCM+FSA,a) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
K277(SCM+FSA,K276(SCM+FSA,a)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
a is with_explicit_jumps IC-relocable () Element of the InstructionsF of SCM+FSA
Macro a is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() set
K276(SCM+FSA,a) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
K277(SCM+FSA,K276(SCM+FSA,a)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
a is V101() Element of the carrier of SCM+FSA
b is V101() Element of the carrier of SCM+FSA
a := b is ins-loc-free V64( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) V140(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Macro (a := b) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() set
K276(SCM+FSA,(a := b)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
K277(SCM+FSA,K276(SCM+FSA,(a := b))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
i1 is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total 0 -started set
i2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Comput (i2,i1,1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
IC (Comput (i2,i1,1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (i2,i1,1)) . (IC ) is set
dom i2 is non empty set
CurInstr (i2,(Comput (i2,i1,1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i2 /. (IC (Comput (i2,i1,1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom (Start-At (0,SCM+FSA)) is non empty V40() set
IC i1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
i1 . (IC ) is set
(Start-At (0,SCM+FSA)) . (IC ) is set
Exec ((a := b),i1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like V18( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(a := b)) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(a := b)) . i1 is Relation-like Function-like set
IC (Exec ((a := b),i1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Exec ((a := b),i1)) . (IC ) is set
succ 0 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() set
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
dom (Macro (a := b)) is non empty V40() set
i2 . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro (a := b)) . 0 is set
i2 . 1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro (a := b)) . 1 is set
Comput (i2,i1,(0 + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
Comput (i2,i1,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
Following (i2,(Comput (i2,i1,0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
CurInstr (i2,(Comput (i2,i1,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (i2,i1,0)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (i2,i1,0)) . (IC ) is set
i2 /. (IC (Comput (i2,i1,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i2,(Comput (i2,i1,0)))),(Comput (i2,i1,0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,(Comput (i2,i1,0))))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,(Comput (i2,i1,0))))) . (Comput (i2,i1,0)) is Relation-like Function-like set
Following (i2,i1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
CurInstr (i2,i1) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i2 /. (IC i1) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i2,i1)),i1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,i1))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,i1))) . i1 is Relation-like Function-like set
AddTo (a,b) is ins-loc-free V64( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) V140(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Macro (AddTo (a,b)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() set
K276(SCM+FSA,(AddTo (a,b))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
K277(SCM+FSA,K276(SCM+FSA,(AddTo (a,b)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
i1 is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total 0 -started set
i2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Comput (i2,i1,1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
IC (Comput (i2,i1,1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (i2,i1,1)) . (IC ) is set
dom i2 is non empty set
CurInstr (i2,(Comput (i2,i1,1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i2 /. (IC (Comput (i2,i1,1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom (Start-At (0,SCM+FSA)) is non empty V40() set
IC i1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
i1 . (IC ) is set
(Start-At (0,SCM+FSA)) . (IC ) is set
Exec ((AddTo (a,b)),i1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like V18( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(AddTo (a,b))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(AddTo (a,b))) . i1 is Relation-like Function-like set
IC (Exec ((AddTo (a,b)),i1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Exec ((AddTo (a,b)),i1)) . (IC ) is set
succ 0 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() set
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
dom (Macro (AddTo (a,b))) is non empty V40() set
i2 . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro (AddTo (a,b))) . 0 is set
i2 . 1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro (AddTo (a,b))) . 1 is set
Comput (i2,i1,(0 + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
Comput (i2,i1,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
Following (i2,(Comput (i2,i1,0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
CurInstr (i2,(Comput (i2,i1,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (i2,i1,0)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (i2,i1,0)) . (IC ) is set
i2 /. (IC (Comput (i2,i1,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i2,(Comput (i2,i1,0)))),(Comput (i2,i1,0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,(Comput (i2,i1,0))))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,(Comput (i2,i1,0))))) . (Comput (i2,i1,0)) is Relation-like Function-like set
Following (i2,i1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
CurInstr (i2,i1) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i2 /. (IC i1) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i2,i1)),i1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,i1))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,i1))) . i1 is Relation-like Function-like set
SubFrom (a,b) is ins-loc-free V64( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) V140(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Macro (SubFrom (a,b)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() set
K276(SCM+FSA,(SubFrom (a,b))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
K277(SCM+FSA,K276(SCM+FSA,(SubFrom (a,b)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
i1 is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total 0 -started set
i2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Comput (i2,i1,1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
IC (Comput (i2,i1,1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (i2,i1,1)) . (IC ) is set
dom i2 is non empty set
CurInstr (i2,(Comput (i2,i1,1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i2 /. (IC (Comput (i2,i1,1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom (Start-At (0,SCM+FSA)) is non empty V40() set
IC i1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
i1 . (IC ) is set
(Start-At (0,SCM+FSA)) . (IC ) is set
Exec ((SubFrom (a,b)),i1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like V18( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(SubFrom (a,b))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(SubFrom (a,b))) . i1 is Relation-like Function-like set
IC (Exec ((SubFrom (a,b)),i1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Exec ((SubFrom (a,b)),i1)) . (IC ) is set
succ 0 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() set
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
dom (Macro (SubFrom (a,b))) is non empty V40() set
i2 . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro (SubFrom (a,b))) . 0 is set
i2 . 1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro (SubFrom (a,b))) . 1 is set
Comput (i2,i1,(0 + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
Comput (i2,i1,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
Following (i2,(Comput (i2,i1,0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
CurInstr (i2,(Comput (i2,i1,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (i2,i1,0)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (i2,i1,0)) . (IC ) is set
i2 /. (IC (Comput (i2,i1,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i2,(Comput (i2,i1,0)))),(Comput (i2,i1,0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,(Comput (i2,i1,0))))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,(Comput (i2,i1,0))))) . (Comput (i2,i1,0)) is Relation-like Function-like set
Following (i2,i1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
CurInstr (i2,i1) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i2 /. (IC i1) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i2,i1)),i1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,i1))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,i1))) . i1 is Relation-like Function-like set
MultBy (a,b) is ins-loc-free V64( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) V140(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Macro (MultBy (a,b)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() set
K276(SCM+FSA,(MultBy (a,b))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
K277(SCM+FSA,K276(SCM+FSA,(MultBy (a,b)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
i1 is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total 0 -started set
i2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Comput (i2,i1,1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
IC (Comput (i2,i1,1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (i2,i1,1)) . (IC ) is set
dom i2 is non empty set
CurInstr (i2,(Comput (i2,i1,1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i2 /. (IC (Comput (i2,i1,1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom (Start-At (0,SCM+FSA)) is non empty V40() set
IC i1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
i1 . (IC ) is set
(Start-At (0,SCM+FSA)) . (IC ) is set
Exec ((MultBy (a,b)),i1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like V18( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(MultBy (a,b))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(MultBy (a,b))) . i1 is Relation-like Function-like set
IC (Exec ((MultBy (a,b)),i1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Exec ((MultBy (a,b)),i1)) . (IC ) is set
succ 0 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() set
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
dom (Macro (MultBy (a,b))) is non empty V40() set
i2 . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro (MultBy (a,b))) . 0 is set
i2 . 1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro (MultBy (a,b))) . 1 is set
Comput (i2,i1,(0 + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
Comput (i2,i1,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
Following (i2,(Comput (i2,i1,0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
CurInstr (i2,(Comput (i2,i1,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (i2,i1,0)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (i2,i1,0)) . (IC ) is set
i2 /. (IC (Comput (i2,i1,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i2,(Comput (i2,i1,0)))),(Comput (i2,i1,0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,(Comput (i2,i1,0))))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,(Comput (i2,i1,0))))) . (Comput (i2,i1,0)) is Relation-like Function-like set
Following (i2,i1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
CurInstr (i2,i1) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i2 /. (IC i1) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i2,i1)),i1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,i1))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,i1))) . i1 is Relation-like Function-like set
Divide (a,b) is ins-loc-free V64( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) V140(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Macro (Divide (a,b)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() set
K276(SCM+FSA,(Divide (a,b))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
K277(SCM+FSA,K276(SCM+FSA,(Divide (a,b)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
i1 is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total 0 -started set
i2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Comput (i2,i1,1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
IC (Comput (i2,i1,1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (i2,i1,1)) . (IC ) is set
dom i2 is non empty set
CurInstr (i2,(Comput (i2,i1,1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i2 /. (IC (Comput (i2,i1,1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom (Start-At (0,SCM+FSA)) is non empty V40() set
IC i1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
i1 . (IC ) is set
(Start-At (0,SCM+FSA)) . (IC ) is set
Exec ((Divide (a,b)),i1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like V18( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(Divide (a,b))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(Divide (a,b))) . i1 is Relation-like Function-like set
IC (Exec ((Divide (a,b)),i1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Exec ((Divide (a,b)),i1)) . (IC ) is set
succ 0 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() set
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
dom (Macro (Divide (a,b))) is non empty V40() set
i2 . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro (Divide (a,b))) . 0 is set
i2 . 1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro (Divide (a,b))) . 1 is set
Comput (i2,i1,(0 + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
Comput (i2,i1,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
Following (i2,(Comput (i2,i1,0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
CurInstr (i2,(Comput (i2,i1,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (i2,i1,0)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (i2,i1,0)) . (IC ) is set
i2 /. (IC (Comput (i2,i1,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i2,(Comput (i2,i1,0)))),(Comput (i2,i1,0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,(Comput (i2,i1,0))))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,(Comput (i2,i1,0))))) . (Comput (i2,i1,0)) is Relation-like Function-like set
Following (i2,i1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
CurInstr (i2,i1) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i2 /. (IC i1) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i2,i1)),i1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,i1))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,i1))) . i1 is Relation-like Function-like set
i0 is FinSeq-Location
b := (i0,a) is ins-loc-free V64( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) non jump-only V140(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<*b,i0,a*> is non empty Relation-like NAT -defined Function-like V40() 3 -element FinSequence-like FinSubsequence-like set
K15(9,{},<*b,i0,a*>) is set
Macro (b := (i0,a)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() set
K276(SCM+FSA,(b := (i0,a))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
K277(SCM+FSA,K276(SCM+FSA,(b := (i0,a)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
i2 is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total 0 -started set
i1 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Comput (i1,i2,1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
IC (Comput (i1,i2,1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (i1,i2,1)) . (IC ) is set
dom i1 is non empty set
CurInstr (i1,(Comput (i1,i2,1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i1 /. (IC (Comput (i1,i2,1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom (Start-At (0,SCM+FSA)) is non empty V40() set
IC i2 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
i2 . (IC ) is set
(Start-At (0,SCM+FSA)) . (IC ) is set
Exec ((b := (i0,a)),i2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like V18( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(b := (i0,a))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(b := (i0,a))) . i2 is Relation-like Function-like set
IC (Exec ((b := (i0,a)),i2)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Exec ((b := (i0,a)),i2)) . (IC ) is set
succ 0 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() set
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
dom (Macro (b := (i0,a))) is non empty V40() set
i1 . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro (b := (i0,a))) . 0 is set
i1 . 1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro (b := (i0,a))) . 1 is set
Comput (i1,i2,(0 + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
Comput (i1,i2,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
Following (i1,(Comput (i1,i2,0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
CurInstr (i1,(Comput (i1,i2,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (i1,i2,0)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (i1,i2,0)) . (IC ) is set
i1 /. (IC (Comput (i1,i2,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i1,(Comput (i1,i2,0)))),(Comput (i1,i2,0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i1,(Comput (i1,i2,0))))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i1,(Comput (i1,i2,0))))) . (Comput (i1,i2,0)) is Relation-like Function-like set
Following (i1,i2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
CurInstr (i1,i2) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i1 /. (IC i2) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i1,i2)),i2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i1,i2))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i1,i2))) . i2 is Relation-like Function-like set
(i0,a) := b is ins-loc-free V64( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) non jump-only V140(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K15(10,{},<*b,i0,a*>) is set
Macro ((i0,a) := b) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() set
K276(SCM+FSA,((i0,a) := b)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
K277(SCM+FSA,K276(SCM+FSA,((i0,a) := b))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
i2 is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total 0 -started set
i1 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Comput (i1,i2,1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
IC (Comput (i1,i2,1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (i1,i2,1)) . (IC ) is set
dom i1 is non empty set
CurInstr (i1,(Comput (i1,i2,1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i1 /. (IC (Comput (i1,i2,1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom (Start-At (0,SCM+FSA)) is non empty V40() set
IC i2 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
i2 . (IC ) is set
(Start-At (0,SCM+FSA)) . (IC ) is set
Exec (((i0,a) := b),i2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like V18( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,((i0,a) := b)) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,((i0,a) := b)) . i2 is Relation-like Function-like set
IC (Exec (((i0,a) := b),i2)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Exec (((i0,a) := b),i2)) . (IC ) is set
succ 0 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V51() set
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
dom (Macro ((i0,a) := b)) is non empty V40() set
i1 . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro ((i0,a) := b)) . 0 is set
i1 . 1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro ((i0,a) := b)) . 1 is set
Comput (i1,i2,(0 + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
Comput (i1,i2,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
Following (i1,(Comput (i1,i2,0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
CurInstr (i1,(Comput (i1,i2,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (i1,i2,0)) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (i1,i2,0)) . (IC ) is set
i1 /. (IC (Comput (i1,i2,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i1,(Comput (i1,i2,0)))),(Comput (i1,i2,0))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i1,(Comput (i1,i2,0))))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i1,(Comput (i1,i2,0))))) . (Comput (i1,i2,0)) is Relation-like Function-like set
Following (i1,i2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
CurInstr (i1,i2) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i1 /. (IC i2) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i1,i2)),i2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total set
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i1,i2))) is Element of K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K101( the InstructionsF of SCM+FSA,K99(K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K290(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i1,i2))) . i2 is Relation-like Function-like set
Macro ((i0,a) := b) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() V58() set
K276(SCM+FSA,((i0,a) := b)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
K277(SCM+FSA,K276(SCM+FSA,((i0,a) := b))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V40() set
i2 is non empty Relation-like the carrier of SCM+FSA -defined Function-like K301(3,SCM+FSA) -compatible total 0 -started set
i2 . (intloc 0) is ext-real V36() V37() integer set
i1 is non empty Relation-like NAT -defined the InstructionsF of