:: 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

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