:: SF_MASTR semantic presentation

REAL is non empty non trivial V51() V52() V53() V57() non finite V69() V70() V72() V103() set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal V51() V52() V53() V54() V55() V56() V57() non finite V67() V69() cardinal limit_cardinal countable denumerable V103() Element of bool REAL

bool REAL is non empty non trivial cup-closed diff-closed preBoolean non finite V103() set

SCM+FSA is non empty V121(3) IC-Ins-separated strict V129(3) with_explicit_jumps IC-relocable V140(3) AMI-Struct over 3

3 is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V67() V68() V69() V70() V71() cardinal countable V102() Element of NAT

K515() is set

K579(NAT,K515()) is Element of K515()

K508() is non empty set

K518() is Relation-like K515() -defined 3 -valued Function-like total V18(K515(),3) Element of bool [:K515(),3:]

[:K515(),3:] is set

bool [:K515(),3:] is cup-closed diff-closed preBoolean set

K519() is Relation-like 3 -defined Function-like non empty total set

K526() is Relation-like K508() -defined K78((product (K518() (#) K519())),(product (K518() (#) K519()))) -valued Function-like non empty total V18(K508(),K78((product (K518() (#) K519())),(product (K518() (#) K519())))) Element of bool [:K508(),K78((product (K518() (#) K519())),(product (K518() (#) K519()))):]

K518() (#) K519() is Relation-like Function-like set

product (K518() (#) K519()) is functional with_common_domain product-like set

K78((product (K518() (#) K519())),(product (K518() (#) K519()))) is functional non empty set

[:K508(),K78((product (K518() (#) K519())),(product (K518() (#) K519()))):] is set

bool [:K508(),K78((product (K518() (#) K519())),(product (K518() (#) K519()))):] is cup-closed diff-closed preBoolean set

AMI-Struct(# K515(),K579(NAT,K515()),K508(),K518(),K519(),K526() #) is strict AMI-Struct over 3

the carrier of SCM+FSA is set

{} is Function-like functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() V34() integer ext-real V51() V52() V53() V54() V55() V56() V57() finite V62() V69() V70() V71() V72() cardinal {} -element FinSequence-membered countable set

the Function-like functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() V34() integer ext-real V51() V52() V53() V54() V55() V56() V57() finite V62() V69() V70() V71() V72() cardinal {} -element FinSequence-membered countable set is Function-like functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() V34() integer ext-real V51() V52() V53() V54() V55() V56() V57() finite V62() V69() V70() V71() V72() cardinal {} -element FinSequence-membered countable set

COMPLEX is non empty non trivial V51() V57() non finite V103() set

RAT is non empty non trivial V51() V52() V53() V54() V57() non finite V103() set

INT is non empty non trivial V51() V52() V53() V54() V55() V57() non finite V103() set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal V51() V52() V53() V54() V55() V56() V57() non finite V67() V69() cardinal limit_cardinal countable denumerable V103() set

bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite V103() set

bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite V103() set

[:COMPLEX,COMPLEX:] is non empty non trivial non finite V103() set

bool [:COMPLEX,COMPLEX:] is non empty non trivial cup-closed diff-closed preBoolean non finite V103() set

[:COMPLEX,REAL:] is non empty non trivial non finite V103() set

bool [:COMPLEX,REAL:] is non empty non trivial cup-closed diff-closed preBoolean non finite V103() set

9 is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V67() V68() V69() V70() V71() cardinal countable V102() Element of NAT

Segm 9 is V51() V52() V53() V54() V55() V56() V69() countable Element of bool NAT

Int-Locations is non empty set

SCM-Memory is non empty set

bool SCM-Memory is cup-closed diff-closed preBoolean set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V67() V68() V69() V70() V71() cardinal countable V102() Element of NAT

[:SCM-Memory,2:] is set

bool [:SCM-Memory,2:] is cup-closed diff-closed preBoolean set

SCM-OK is Relation-like SCM-Memory -defined 2 -valued Function-like non empty total V18( SCM-Memory ,2) Element of bool [:SCM-Memory,2:]

SCM-VAL is Relation-like 2 -defined Function-like non empty total set

SCM-OK (#) SCM-VAL is Relation-like non-empty Function-like set

product (SCM-OK (#) SCM-VAL) is functional non empty with_common_domain product-like set

K329() is Relation-like non empty standard-ins V111() J/A-independent V114() set

K78((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL))) is functional non empty set

[:K329(),K78((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL))):] is set

bool [:K329(),K78((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL))):] is cup-closed diff-closed preBoolean set

SCM is non empty V121(2) IC-Ins-separated strict strict V129(2) AMI-Struct over 2

K579(NAT,SCM-Memory) is Element of SCM-Memory

SCM-Exec is Relation-like K329() -defined K78((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL))) -valued Function-like non empty total V18(K329(),K78((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL)))) Element of bool [:K329(),K78((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL))):]

AMI-Struct(# SCM-Memory,K579(NAT,SCM-Memory),K329(),SCM-OK,SCM-VAL,SCM-Exec #) is strict AMI-Struct over 2

the InstructionsF of SCM is Relation-like non empty standard-ins V111() J/A-independent V114() set

the carrier of SCM is set

K423(2,SCM) is Relation-like non-empty the carrier of SCM -defined Function-like total set

the Object-Kind of SCM is Relation-like the carrier of SCM -defined 2 -valued Function-like total V18( the carrier of SCM,2) Element of bool [: the carrier of SCM,2:]

[: the carrier of SCM,2:] is set

bool [: the carrier of SCM,2:] is cup-closed diff-closed preBoolean set

the U7 of SCM is Relation-like 2 -defined Function-like non empty total set

the Object-Kind of SCM (#) the U7 of SCM is Relation-like Function-like set

bool the carrier of SCM+FSA is cup-closed diff-closed preBoolean set

the InstructionsF of SCM+FSA is Relation-like non empty standard-ins V111() J/A-independent V114() set

K507() is set

bool K515() is cup-closed diff-closed preBoolean set

K423(3,SCM+FSA) is Relation-like non-empty 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 total V18( the carrier of SCM+FSA,3) Element of bool [: the carrier of SCM+FSA,3:]

[: the carrier of SCM+FSA,3:] is set

bool [: the carrier of SCM+FSA,3:] is cup-closed diff-closed preBoolean set

the U7 of SCM+FSA is Relation-like 3 -defined Function-like non empty total set

the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA is Relation-like Function-like set

Int-Locations is non empty Element of bool the carrier of SCM+FSA

bool Int-Locations is cup-closed diff-closed preBoolean set

[:NAT,(bool NAT):] is non empty non trivial non finite V103() set

bool [:NAT,(bool NAT):] is non empty non trivial cup-closed diff-closed preBoolean non finite V103() set

FinPartSt SCM+FSA is functional non empty Element of bool (sproduct K423(3,SCM+FSA))

sproduct K423(3,SCM+FSA) is functional non empty set

bool (sproduct K423(3,SCM+FSA)) is cup-closed diff-closed preBoolean set

{ b

[:(FinPartSt SCM+FSA),(FinPartSt SCM+FSA):] is set

bool [:(FinPartSt SCM+FSA),(FinPartSt SCM+FSA):] is cup-closed diff-closed preBoolean set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V67() V68() V69() V70() V71() cardinal countable V102() Element of NAT

0 is Function-like functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() V57() finite V62() V69() V70() V71() V72() cardinal {} -element FinSequence-membered countable Element of NAT

12 is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V67() V68() V69() V70() V71() cardinal countable V102() Element of NAT

4 is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V67() V68() V69() V70() V71() cardinal countable V102() Element of NAT

5 is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V67() V68() V69() V70() V71() cardinal countable V102() Element of NAT

6 is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V67() V68() V69() V70() V71() cardinal countable V102() Element of NAT

7 is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V67() V68() V69() V70() V71() cardinal countable V102() Element of NAT

8 is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V67() V68() V69() V70() V71() cardinal countable V102() Element of NAT

10 is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V67() V68() V69() V70() V71() cardinal countable V102() Element of NAT

11 is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V67() V68() V69() V70() V71() cardinal countable V102() Element of NAT

K517() is Element of bool K515()

IC is Element of the carrier of SCM+FSA

halt SCM+FSA is ins-loc-free V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

halt the InstructionsF of SCM+FSA is ins-loc-free with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

K50(0,{},{}) is set

SCM-Data-Loc is non empty Element of bool SCM-Memory

intloc 0 is Int-like read-only Element of the carrier of SCM+FSA

dl. 0 is Int-like Element of the carrier of SCM

[1,0] is non empty non natural set

FinSeq-Locations is non empty non trivial non finite V103() Element of bool the carrier of SCM+FSA

bool FinSeq-Locations is non empty non trivial cup-closed diff-closed preBoolean non finite V103() set

I is Int-like Element of the carrier of SCM+FSA

n is Int-like Element of the carrier of SCM+FSA

I := n is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

s is Int-like Element of the carrier of SCM+FSA

t is Int-like Element of the carrier of SCM+FSA

s := t is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

P is Int-like Element of the carrier of SCM

Q is Int-like Element of the carrier of SCM

P := Q is Element of the InstructionsF of SCM

<*P,Q*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(1,{},<*P,Q*>) is set

m is Int-like Element of the carrier of SCM

p is Int-like Element of the carrier of SCM

m := p is Element of the InstructionsF of SCM

<*m,p*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(1,{},<*m,p*>) is set

<*m,p*> . 1 is set

<*m,p*> . 2 is set

<*P,Q*> . 1 is set

<*P,Q*> . 2 is set

I is Int-like Element of the carrier of SCM+FSA

n is Int-like Element of the carrier of SCM+FSA

AddTo (I,n) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

s is Int-like Element of the carrier of SCM+FSA

t is Int-like Element of the carrier of SCM+FSA

AddTo (s,t) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

P is Int-like Element of the carrier of SCM

Q is Int-like Element of the carrier of SCM

AddTo (P,Q) is Element of the InstructionsF of SCM

<*P,Q*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(2,{},<*P,Q*>) is set

m is Int-like Element of the carrier of SCM

p is Int-like Element of the carrier of SCM

AddTo (m,p) is Element of the InstructionsF of SCM

<*m,p*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(2,{},<*m,p*>) is set

<*m,p*> . 1 is set

<*m,p*> . 2 is set

<*P,Q*> . 1 is set

<*P,Q*> . 2 is set

I is Int-like Element of the carrier of SCM+FSA

n is Int-like Element of the carrier of SCM+FSA

SubFrom (I,n) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

s is Int-like Element of the carrier of SCM+FSA

t is Int-like Element of the carrier of SCM+FSA

SubFrom (s,t) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

P is Int-like Element of the carrier of SCM

Q is Int-like Element of the carrier of SCM

SubFrom (P,Q) is Element of the InstructionsF of SCM

<*P,Q*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(3,{},<*P,Q*>) is set

m is Int-like Element of the carrier of SCM

p is Int-like Element of the carrier of SCM

SubFrom (m,p) is Element of the InstructionsF of SCM

<*m,p*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(3,{},<*m,p*>) is set

<*m,p*> . 1 is set

<*m,p*> . 2 is set

<*P,Q*> . 1 is set

<*P,Q*> . 2 is set

I is Int-like Element of the carrier of SCM+FSA

n is Int-like Element of the carrier of SCM+FSA

MultBy (I,n) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

s is Int-like Element of the carrier of SCM+FSA

t is Int-like Element of the carrier of SCM+FSA

MultBy (s,t) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

P is Int-like Element of the carrier of SCM

Q is Int-like Element of the carrier of SCM

MultBy (P,Q) is Element of the InstructionsF of SCM

<*P,Q*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(4,{},<*P,Q*>) is set

m is Int-like Element of the carrier of SCM

p is Int-like Element of the carrier of SCM

MultBy (m,p) is Element of the InstructionsF of SCM

<*m,p*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(4,{},<*m,p*>) is set

<*m,p*> . 1 is set

<*m,p*> . 2 is set

<*P,Q*> . 1 is set

<*P,Q*> . 2 is set

I is Int-like Element of the carrier of SCM+FSA

n is Int-like Element of the carrier of SCM+FSA

Divide (I,n) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

s is Int-like Element of the carrier of SCM+FSA

t is Int-like Element of the carrier of SCM+FSA

Divide (s,t) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

P is Int-like Element of the carrier of SCM

Q is Int-like Element of the carrier of SCM

Divide (P,Q) is Element of the InstructionsF of SCM

<*P,Q*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(5,{},<*P,Q*>) is set

m is Int-like Element of the carrier of SCM

p is Int-like Element of the carrier of SCM

Divide (m,p) is Element of the InstructionsF of SCM

<*m,p*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(5,{},<*m,p*>) is set

<*m,p*> . 1 is set

<*m,p*> . 2 is set

<*P,Q*> . 1 is set

<*P,Q*> . 2 is set

I is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

goto I is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SCM-goto I is Element of the InstructionsF of SCM

<*I*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

K50(6,<*I*>,{}) is set

n is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

goto n is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SCM-goto n is Element of the InstructionsF of SCM

<*n*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

K50(6,<*n*>,{}) is set

<*I*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT

<*I*> . 1 is set

<*n*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT

<*n*> . 1 is set

I is Int-like Element of the carrier of SCM+FSA

n is Int-like Element of the carrier of SCM+FSA

s is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

I =0_goto s is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

t is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

n =0_goto t is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

P is Int-like Element of the carrier of SCM

P =0_goto s is Element of the InstructionsF of SCM

<*s*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

<*P*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

K50(7,<*s*>,<*P*>) is set

Q is Int-like Element of the carrier of SCM

Q =0_goto t is Element of the InstructionsF of SCM

<*t*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

<*Q*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

K50(7,<*t*>,<*Q*>) is set

<*t*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT

<*t*> . 1 is set

<*Q*> . 1 is set

<*s*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT

<*s*> . 1 is set

<*P*> . 1 is set

I is Int-like Element of the carrier of SCM+FSA

n is Int-like Element of the carrier of SCM+FSA

s is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

I >0_goto s is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

t is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

n >0_goto t is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

P is Int-like Element of the carrier of SCM

P >0_goto s is Element of the InstructionsF of SCM

<*s*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

<*P*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

K50(8,<*s*>,<*P*>) is set

Q is Int-like Element of the carrier of SCM

Q >0_goto t is Element of the InstructionsF of SCM

<*t*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

<*Q*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

K50(8,<*t*>,<*Q*>) is set

<*t*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT

<*t*> . 1 is set

<*Q*> . 1 is set

<*s*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT

<*s*> . 1 is set

<*P*> . 1 is set

I is Int-like Element of the carrier of SCM+FSA

n is Int-like Element of the carrier of SCM+FSA

s is Int-like Element of the carrier of SCM+FSA

t is Int-like Element of the carrier of SCM+FSA

P is FinSeq-Location

I := (P,n) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*I,P,n*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set

K50(9,{},<*I,P,n*>) is set

Q is FinSeq-Location

s := (Q,t) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*s,Q,t*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set

K50(9,{},<*s,Q,t*>) is set

<*I,P,n*> . 1 is set

<*I,P,n*> . 2 is set

<*I,P,n*> . 3 is set

<*s,Q,t*> . 1 is set

<*s,Q,t*> . 2 is set

<*s,Q,t*> . 3 is set

I is Int-like Element of the carrier of SCM+FSA

n is Int-like Element of the carrier of SCM+FSA

s is Int-like Element of the carrier of SCM+FSA

t is Int-like Element of the carrier of SCM+FSA

P is FinSeq-Location

(P,I) := n is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*n,P,I*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set

K50(10,{},<*n,P,I*>) is set

Q is FinSeq-Location

(Q,s) := t is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*t,Q,s*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set

K50(10,{},<*t,Q,s*>) is set

<*n,P,I*> . 1 is set

<*n,P,I*> . 2 is set

<*n,P,I*> . 3 is set

<*t,Q,s*> . 1 is set

<*t,Q,s*> . 2 is set

<*t,Q,s*> . 3 is set

I is Int-like Element of the carrier of SCM+FSA

n is Int-like Element of the carrier of SCM+FSA

s is FinSeq-Location

I :=len s is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*I,s*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(11,{},<*I,s*>) is set

t is FinSeq-Location

n :=len t is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*n,t*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(11,{},<*n,t*>) is set

<*I,s*> . 1 is set

<*I,s*> . 2 is set

<*n,t*> . 1 is set

<*n,t*> . 2 is set

I is Int-like Element of the carrier of SCM+FSA

n is Int-like Element of the carrier of SCM+FSA

s is FinSeq-Location

s :=<0,...,0> I is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*I,s*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(12,{},<*I,s*>) is set

t is FinSeq-Location

t :=<0,...,0> n is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*n,t*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(12,{},<*n,t*>) is set

<*I,s*> . 1 is set

<*I,s*> . 2 is set

<*n,t*> . 1 is set

<*n,t*> . 2 is set

I is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

InsCode I is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K58( the InstructionsF of SCM+FSA) is set

{1,2,3,4,5} is finite countable V102() set

Fin Int-Locations is non empty cup-closed diff-closed preBoolean set

n is Int-like Element of the carrier of SCM+FSA

s is Int-like Element of the carrier of SCM+FSA

n := s is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

AddTo (n,s) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SubFrom (n,s) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

MultBy (n,s) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

Divide (n,s) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

t is Element of Int-Locations

P is Element of Int-Locations

{.t,P.} is non empty finite countable Element of Fin Int-Locations

Q is finite countable Element of Fin Int-Locations

p is Int-like Element of the carrier of SCM+FSA

p is Int-like Element of the carrier of SCM+FSA

p := p is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

AddTo (p,p) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SubFrom (p,p) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

MultBy (p,p) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

Divide (p,p) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

m is finite countable Element of Fin Int-Locations

{p,p} is non empty finite countable Element of bool Int-Locations

n is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

s is Int-like Element of the carrier of SCM+FSA

s =0_goto n is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

s >0_goto n is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

t is Element of Int-Locations

{.t.} is non empty trivial finite 1 -element countable Element of Fin Int-Locations

P is finite countable Element of Fin Int-Locations

p is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

m is Int-like Element of the carrier of SCM+FSA

m =0_goto p is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

m >0_goto p is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

Q is finite countable Element of Fin Int-Locations

{m} is non empty trivial finite 1 -element countable Element of bool Int-Locations

s is Int-like Element of the carrier of SCM+FSA

n is Int-like Element of the carrier of SCM+FSA

t is FinSeq-Location

s := (t,n) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*s,t,n*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set

K50(9,{},<*s,t,n*>) is set

(t,n) := s is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K50(10,{},<*s,t,n*>) is set

P is Element of Int-Locations

Q is Element of Int-Locations

{.P,Q.} is non empty finite countable Element of Fin Int-Locations

m is finite countable Element of Fin Int-Locations

i is Int-like Element of the carrier of SCM+FSA

p is Int-like Element of the carrier of SCM+FSA

p1 is FinSeq-Location

i := (p1,p) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*i,p1,p*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set

K50(9,{},<*i,p1,p*>) is set

(p1,p) := i is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K50(10,{},<*i,p1,p*>) is set

p is finite countable Element of Fin Int-Locations

{p,i} is non empty finite countable Element of bool Int-Locations

n is Int-like Element of the carrier of SCM+FSA

s is FinSeq-Location

n :=len s is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*n,s*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(11,{},<*n,s*>) is set

s :=<0,...,0> n is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K50(12,{},<*n,s*>) is set

t is Element of Int-Locations

{.t.} is non empty trivial finite 1 -element countable Element of Fin Int-Locations

P is finite countable Element of Fin Int-Locations

m is Int-like Element of the carrier of SCM+FSA

p is FinSeq-Location

m :=len p is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*m,p*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(11,{},<*m,p*>) is set

p :=<0,...,0> m is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K50(12,{},<*m,p*>) is set

Q is finite countable Element of Fin Int-Locations

{m} is non empty trivial finite 1 -element countable Element of bool Int-Locations

n is finite countable Element of Fin Int-Locations

s is finite countable Element of Fin Int-Locations

t is Int-like Element of the carrier of SCM+FSA

P is Int-like Element of the carrier of SCM+FSA

t := P is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

AddTo (t,P) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SubFrom (t,P) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

MultBy (t,P) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

Divide (t,P) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

{t,P} is non empty finite countable Element of bool Int-Locations

Q is Int-like Element of the carrier of SCM+FSA

m is Int-like Element of the carrier of SCM+FSA

Q := m is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

AddTo (Q,m) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SubFrom (Q,m) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

MultBy (Q,m) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

Divide (Q,m) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

{Q,m} is non empty finite countable Element of bool Int-Locations

P is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

t is Int-like Element of the carrier of SCM+FSA

t =0_goto P is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

t >0_goto P is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

{t} is non empty trivial finite 1 -element countable Element of bool Int-Locations

m is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

Q is Int-like Element of the carrier of SCM+FSA

Q =0_goto m is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

Q >0_goto m is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

{Q} is non empty trivial finite 1 -element countable Element of bool Int-Locations

P is Int-like Element of the carrier of SCM+FSA

t is Int-like Element of the carrier of SCM+FSA

Q is FinSeq-Location

P := (Q,t) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*P,Q,t*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set

K50(9,{},<*P,Q,t*>) is set

(Q,t) := P is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K50(10,{},<*P,Q,t*>) is set

{t,P} is non empty finite countable Element of bool Int-Locations

p is Int-like Element of the carrier of SCM+FSA

m is Int-like Element of the carrier of SCM+FSA

p is FinSeq-Location

p := (p,m) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*p,p,m*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set

K50(9,{},<*p,p,m*>) is set

(p,m) := p is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K50(10,{},<*p,p,m*>) is set

{m,p} is non empty finite countable Element of bool Int-Locations

t is Int-like Element of the carrier of SCM+FSA

P is FinSeq-Location

t :=len P is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*t,P*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(11,{},<*t,P*>) is set

P :=<0,...,0> t is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K50(12,{},<*t,P*>) is set

{t} is non empty trivial finite 1 -element countable Element of bool Int-Locations

Q is Int-like Element of the carrier of SCM+FSA

m is FinSeq-Location

Q :=len m is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*Q,m*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(11,{},<*Q,m*>) is set

m :=<0,...,0> Q is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K50(12,{},<*Q,m*>) is set

{Q} is non empty trivial finite 1 -element countable Element of bool Int-Locations

s is Int-like Element of the carrier of SCM+FSA

t is Int-like Element of the carrier of SCM+FSA

s := t is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

AddTo (s,t) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SubFrom (s,t) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

MultBy (s,t) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

Divide (s,t) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

n is finite countable Element of Fin Int-Locations

{s,t} is non empty finite countable Element of bool Int-Locations

Q is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

P is Int-like Element of the carrier of SCM+FSA

P =0_goto Q is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

P >0_goto Q is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

{P} is non empty trivial finite 1 -element countable Element of bool Int-Locations

p is Int-like Element of the carrier of SCM+FSA

p is Int-like Element of the carrier of SCM+FSA

p := p is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

AddTo (p,p) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SubFrom (p,p) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

MultBy (p,p) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

Divide (p,p) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

m is finite countable Element of Fin Int-Locations

{p,p} is non empty finite countable Element of bool Int-Locations

p1 is Int-like Element of the carrier of SCM+FSA

i is Int-like Element of the carrier of SCM+FSA

f is FinSeq-Location

p1 := (f,i) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*p1,f,i*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set

K50(9,{},<*p1,f,i*>) is set

(f,i) := p1 is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K50(10,{},<*p1,f,i*>) is set

{i,p1} is non empty finite countable Element of bool Int-Locations

c

c

c

AddTo (c

SubFrom (c

MultBy (c

Divide (c

x9 is finite countable Element of Fin Int-Locations

{c

c

c

c

<*c

K50(11,{},<*c

c

K50(12,{},<*c

{c

c

c

c

c

c

{c

c

c

c

c

<*c

K50(9,{},<*c

(c

K50(10,{},<*c

{c

c

c

c

c

c

{c

c

c

c

<*c

K50(11,{},<*c

c

K50(12,{},<*c

{c

c

c

c

c

<*c

K50(9,{},<*c

(c

K50(10,{},<*c

c

{c

c

c

c

<*c

K50(11,{},<*c

c

K50(12,{},<*c

{c

((halt SCM+FSA)) is finite countable Element of Fin Int-Locations

InsCode (halt SCM+FSA) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable V138(3, SCM+FSA ) Element of InsCodes the InstructionsF of SCM+FSA

I is Int-like Element of the carrier of SCM+FSA

n is Int-like Element of the carrier of SCM+FSA

I := n is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

AddTo (I,n) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SubFrom (I,n) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

MultBy (I,n) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

Divide (I,n) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

{I,n} is non empty finite countable Element of bool Int-Locations

s is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(s) is finite countable Element of Fin Int-Locations

InsCode s is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable Element of InsCodes the InstructionsF of SCM+FSA

t is finite countable Element of Fin Int-Locations

I is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

goto I is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SCM-goto I is Element of the InstructionsF of SCM

<*I*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

K50(6,<*I*>,{}) is set

((goto I)) is finite countable Element of Fin Int-Locations

InsCode (goto I) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable V138(3, SCM+FSA ) Element of InsCodes the InstructionsF of SCM+FSA

I is Int-like Element of the carrier of SCM+FSA

{I} is non empty trivial finite 1 -element countable Element of bool Int-Locations

n is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

I =0_goto n is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

I >0_goto n is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

s is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(s) is finite countable Element of Fin Int-Locations

InsCode s is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable Element of InsCodes the InstructionsF of SCM+FSA

t is finite countable Element of Fin Int-Locations

I is Int-like Element of the carrier of SCM+FSA

n is Int-like Element of the carrier of SCM+FSA

{n,I} is non empty finite countable Element of bool Int-Locations

s is FinSeq-Location

I := (s,n) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*I,s,n*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set

K50(9,{},<*I,s,n*>) is set

(s,n) := I is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K50(10,{},<*I,s,n*>) is set

t is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(t) is finite countable Element of Fin Int-Locations

InsCode t is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable Element of InsCodes the InstructionsF of SCM+FSA

P is finite countable Element of Fin Int-Locations

I is Int-like Element of the carrier of SCM+FSA

{I} is non empty trivial finite 1 -element countable Element of bool Int-Locations

n is FinSeq-Location

I :=len n is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*I,n*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

K50(11,{},<*I,n*>) is set

n :=<0,...,0> I is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K50(12,{},<*I,n*>) is set

s is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(s) is finite countable Element of Fin Int-Locations

InsCode s is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable Element of InsCodes the InstructionsF of SCM+FSA

t is finite countable Element of Fin Int-Locations

[: the InstructionsF of SCM+FSA,(Fin Int-Locations):] is set

bool [: the InstructionsF of SCM+FSA,(Fin Int-Locations):] is cup-closed diff-closed preBoolean set

I is Relation-like Function-like set

n is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

s is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(s) is finite countable Element of Fin Int-Locations

t is finite countable Element of Fin Int-Locations

n is Relation-like the InstructionsF of SCM+FSA -defined Fin Int-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin Int-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin Int-Locations):]

I (#) n is Relation-like Function-like set

Union (I (#) n) is set

dom I is set

rng (I (#) n) is set

rng n is Element of bool (Fin Int-Locations)

bool (Fin Int-Locations) is cup-closed diff-closed preBoolean set

union (rng (I (#) n)) is set

union (bool Int-Locations) is set

Q is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

n . Q is finite countable Element of Fin Int-Locations

(Q) is finite countable Element of Fin Int-Locations

m is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(m) is finite countable Element of Fin Int-Locations

n is Element of bool Int-Locations

s is Element of bool Int-Locations

t is Relation-like the InstructionsF of SCM+FSA -defined Fin Int-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin Int-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin Int-Locations):]

I (#) t is Relation-like Function-like set

Union (I (#) t) is set

P is Relation-like the InstructionsF of SCM+FSA -defined Fin Int-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin Int-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin Int-Locations):]

I (#) P is Relation-like Function-like set

Union (I (#) P) is set

Q is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

t . Q is finite countable Element of Fin Int-Locations

P . Q is finite countable Element of Fin Int-Locations

m is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(m) is finite countable Element of Fin Int-Locations

I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set

(I) is Element of bool Int-Locations

dom I is V51() V52() V53() V54() V55() V56() finite V69() V70() V71() countable Element of bool NAT

s is Relation-like the InstructionsF of SCM+FSA -defined Fin Int-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin Int-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin Int-Locations):]

I (#) s is Relation-like Function-like finite countable set

Union (I (#) s) is set

rng I is finite countable Element of bool the InstructionsF of SCM+FSA

bool the InstructionsF of SCM+FSA is cup-closed diff-closed preBoolean set

n is finite countable set

[:n, the InstructionsF of SCM+FSA:] is set

bool [:n, the InstructionsF of SCM+FSA:] is cup-closed diff-closed preBoolean set

[:n,(Fin Int-Locations):] is set

bool [:n,(Fin Int-Locations):] is cup-closed diff-closed preBoolean set

t is Relation-like n -defined the InstructionsF of SCM+FSA -valued Function-like total V18(n, the InstructionsF of SCM+FSA) finite countable Element of bool [:n, the InstructionsF of SCM+FSA:]

s * t is Relation-like n -defined Fin Int-Locations -valued Function-like total V18(n, Fin Int-Locations) finite countable Element of bool [:n,(Fin Int-Locations):]

P is Relation-like n -defined Fin Int-Locations -valued Function-like total V18(n, Fin Int-Locations) finite countable Element of bool [:n,(Fin Int-Locations):]

Union P is finite countable set

I is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(I) is finite countable Element of Fin Int-Locations

n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set

rng n is finite countable Element of bool the InstructionsF of SCM+FSA

bool the InstructionsF of SCM+FSA is cup-closed diff-closed preBoolean set

(n) is finite countable Element of bool Int-Locations

dom n is V51() V52() V53() V54() V55() V56() finite V69() V70() V71() countable Element of bool NAT

s is set

n . s is set

t is Relation-like the InstructionsF of SCM+FSA -defined Fin Int-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin Int-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin Int-Locations):]

n (#) t is Relation-like Function-like finite countable set

Union (n (#) t) is set

rng (n (#) t) is finite countable set

union (rng (n (#) t)) is set

dom t is Element of bool the InstructionsF of SCM+FSA

dom (n (#) t) is finite countable set

(n (#) t) . s is set

t . I is finite countable Element of Fin Int-Locations

I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set

(I) is finite countable Element of bool Int-Locations

n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set

I +* n is Relation-like Function-like finite countable set

((I +* n)) is Element of bool Int-Locations

(n) is finite countable Element of bool Int-Locations

(I) \/ (n) is finite countable Element of bool Int-Locations

s is Relation-like the InstructionsF of SCM+FSA -defined Fin Int-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin Int-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin Int-Locations):]

(I +* n) (#) s is Relation-like Function-like finite countable set

Union ((I +* n) (#) s) is set

t is Relation-like the InstructionsF of SCM+FSA -defined Fin Int-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin Int-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin Int-Locations):]

I (#) t is Relation-like Function-like finite countable set

Union (I (#) t) is set

P is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

s . P is finite countable Element of Fin Int-Locations

t . P is finite countable Element of Fin Int-Locations

Q is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(Q) is finite countable Element of Fin Int-Locations

P is Relation-like the InstructionsF of SCM+FSA -defined Fin Int-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin Int-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin Int-Locations):]

n (#) P is Relation-like Function-like finite countable set

Union (n (#) P) is set

Q is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

s . Q is finite countable Element of Fin Int-Locations

P . Q is finite countable Element of Fin Int-Locations

m is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(m) is finite countable Element of Fin Int-Locations

dom s is Element of bool the InstructionsF of SCM+FSA

bool the InstructionsF of SCM+FSA is cup-closed diff-closed preBoolean set

rng n is finite countable Element of bool the InstructionsF of SCM+FSA

I (#) s is Relation-like Function-like finite countable set

n (#) s is Relation-like Function-like finite countable set

(I (#) s) +* (n (#) s) is Relation-like Function-like finite countable set

Union (n (#) s) is set

rng (n (#) s) is finite countable set

union (rng (n (#) s)) is set

rng ((I +* n) (#) s) is finite countable set

union (rng ((I +* n) (#) s)) is set

rng (I (#) s) is finite countable set

(rng (I (#) s)) \/ (rng (n (#) s)) is finite countable set

union ((rng (I (#) s)) \/ (rng (n (#) s))) is set

Union (I (#) s) is set

union (rng (I (#) s)) is set

I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set

dom I is V51() V52() V53() V54() V55() V56() finite V69() V70() V71() countable Element of bool NAT

(I) is finite countable Element of bool Int-Locations

n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set

dom n is V51() V52() V53() V54() V55() V56() finite V69() V70() V71() countable Element of bool NAT

I +* n is Relation-like Function-like finite countable set

((I +* n)) is Element of bool Int-Locations

(n) is finite countable Element of bool Int-Locations

(I) \/ (n) is finite countable Element of bool Int-Locations

s is Relation-like the InstructionsF of SCM+FSA -defined Fin Int-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin Int-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin Int-Locations):]

(I +* n) (#) s is Relation-like Function-like finite countable set

Union ((I +* n) (#) s) is set

I (#) s is Relation-like Function-like finite countable set

dom (I (#) s) is finite countable set

n (#) s is Relation-like Function-like finite countable set

dom (n (#) s) is finite countable set

(I (#) s) +* (n (#) s) is Relation-like Function-like finite countable set

(I (#) s) \/ (n (#) s) is finite countable set

dom s is Element of bool the InstructionsF of SCM+FSA

bool the InstructionsF of SCM+FSA is cup-closed diff-closed preBoolean set

rng n is finite countable Element of bool the InstructionsF of SCM+FSA

Union (n (#) s) is set

rng (n (#) s) is finite countable set

union (rng (n (#) s)) is set

rng ((I +* n) (#) s) is finite countable set

union (rng ((I +* n) (#) s)) is set

rng (I (#) s) is finite countable set

(rng (I (#) s)) \/ (rng (n (#) s)) is finite countable set

union ((rng (I (#) s)) \/ (rng (n (#) s))) is set

t is Relation-like the InstructionsF of SCM+FSA -defined Fin Int-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin Int-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin Int-Locations):]

I (#) t is Relation-like Function-like finite countable set

Union (I (#) t) is set

P is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

s . P is finite countable Element of Fin Int-Locations

t . P is finite countable Element of Fin Int-Locations

Q is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(Q) is finite countable Element of Fin Int-Locations

P is Relation-like the InstructionsF of SCM+FSA -defined Fin Int-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin Int-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin Int-Locations):]

n (#) P is Relation-like Function-like finite countable set

Union (n (#) P) is set

Q is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

s . Q is finite countable Element of Fin Int-Locations

P . Q is finite countable Element of Fin Int-Locations

m is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(m) is finite countable Element of Fin Int-Locations

Union (I (#) s) is set

union (rng (I (#) s)) is set

I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set

(I) is finite countable Element of bool Int-Locations

n is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

Shift (I,n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set

((Shift (I,n))) is finite countable Element of bool Int-Locations

t is Relation-like the InstructionsF of SCM+FSA -defined Fin Int-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin Int-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin Int-Locations):]

I (#) t is Relation-like Function-like finite countable set

Union (I (#) t) is set

P is Relation-like the InstructionsF of SCM+FSA -defined Fin Int-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin Int-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin Int-Locations):]

(Shift (I,n)) (#) P is Relation-like Function-like finite countable set

Union ((Shift (I,n)) (#) P) is set

Q is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

t . Q is finite countable Element of Fin Int-Locations

P . Q is finite countable Element of Fin Int-Locations

m is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(m) is finite countable Element of Fin Int-Locations

dom (Shift (I,n)) is V51() V52() V53() V54() V55() V56() finite V69() V70() V71() countable Element of bool NAT

dom I is V51() V52() V53() V54() V55() V56() finite V69() V70() V71() countable Element of bool NAT

{ (b

Q is set

rng (Shift (I,n)) is finite countable Element of bool the InstructionsF of SCM+FSA

bool the InstructionsF of SCM+FSA is cup-closed diff-closed preBoolean set

m is set

(Shift (I,n)) . m is set

p is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

p + n is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

I . p is set

rng I is finite countable Element of bool the InstructionsF of SCM+FSA

m is set

I . m is set

p is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

p is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

p + n is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

(Shift (I,n)) . (p + n) is set

I . p is set

(Shift (I,n)) (#) t is Relation-like Function-like finite countable set

Union ((Shift (I,n)) (#) t) is set

rng ((Shift (I,n)) (#) t) is finite countable set

union (rng ((Shift (I,n)) (#) t)) is set

t .: (rng (Shift (I,n))) is finite countable Element of bool (Fin Int-Locations)

bool (Fin Int-Locations) is cup-closed diff-closed preBoolean set

rng (I (#) t) is finite countable set

I is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(I) is finite countable Element of Fin Int-Locations

n is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

IncAddr (I,n) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

((IncAddr (I,n))) is finite countable Element of Fin Int-Locations

InsCode I is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable Element of InsCodes the InstructionsF of SCM+FSA

s is Int-like Element of the carrier of SCM+FSA

t is Int-like Element of the carrier of SCM+FSA

s := t is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

s is Int-like Element of the carrier of SCM+FSA

t is Int-like Element of the carrier of SCM+FSA

AddTo (s,t) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

s is Int-like Element of the carrier of SCM+FSA

t is Int-like Element of the carrier of SCM+FSA

SubFrom (s,t) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

s is Int-like Element of the carrier of SCM+FSA

t is Int-like Element of the carrier of SCM+FSA

MultBy (s,t) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

s is Int-like Element of the carrier of SCM+FSA

t is Int-like Element of the carrier of SCM+FSA

Divide (s,t) is ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

s is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

goto s is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SCM-goto s is Element of the InstructionsF of SCM

<*s*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

K50(6,<*s*>,{}) is set

s + n is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable Element of NAT

goto (s + n) is non ins-loc-free V115( the InstructionsF of SCM+FSA) V128(3, SCM+FSA ) with_explicit_jumps IC-relocable V139(3, SCM+FSA ) V141(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SCM-goto (s + n) is Element of the InstructionsF of SCM

<*(s + n)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

K50(6,<*(s + n)*>,{}) is set

s is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real V50() V51() V52() V53() V54() V55() V56() finite V69() V70() V71() cardinal countable