:: SF_MASTR semantic presentation

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

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

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()))):]

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

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

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
is non empty non trivial non finite V103() set

is non empty non trivial 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

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

K78((),()) is functional non empty set
[:K329(),K78((),()):] is set

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

SCM-Exec is Relation-like K329() -defined K78((),()) -valued Function-like non empty total V18(K329(),K78((),())) Element of bool [:K329(),K78((),()):]
AMI-Struct(# SCM-Memory,K579(NAT,SCM-Memory),K329(),SCM-OK,SCM-VAL,SCM-Exec #) is strict AMI-Struct over 2

the carrier of SCM is 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

K507() is 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

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

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

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

{ b1 where b1 is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible Element of sproduct K423(3,SCM+FSA) : b1 is finite } is 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

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

K50(0,{},{}) is set
SCM-Data-Loc is non empty Element of bool SCM-Memory

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

<*I*> . 1 is set

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(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

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

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

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

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

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

K50(12,{},<*I,s*>) is 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

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

n is Int-like Element of the carrier of SCM+FSA
s is Int-like Element of the carrier 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

p is Int-like Element of the carrier of SCM+FSA
p is Int-like Element of the carrier 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

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

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

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

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

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

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

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

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,i} is non empty finite countable Element of bool Int-Locations
n is Int-like Element of the carrier of SCM+FSA

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

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

K50(12,{},<*n,s*>) is set
t is Element of Int-Locations

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

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

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

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

t is Int-like Element of the carrier of SCM+FSA
P is Int-like Element of the carrier 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 Int-like Element of the carrier of SCM+FSA
p is Int-like Element of the carrier 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

{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

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

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
c14 is Int-like Element of the carrier of SCM+FSA
c15 is Int-like Element of the carrier of SCM+FSA
c14 := c15 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 (c14,c15) 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 (c14,c15) 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 (c14,c15) 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 (c14,c15) 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

{c14,c15} is non empty finite countable Element of bool Int-Locations
c16 is Int-like Element of the carrier of SCM+FSA
c17 is FinSeq-Location
c16 :=len c17 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(11,{},<*c16,c17*>) is set
c17 :=<0,...,0> c16 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,{},<*c16,c17*>) is set

c19 is Int-like Element of the carrier of SCM+FSA
c19 =0_goto c20 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
c19 >0_goto c20 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

c22 is Int-like Element of the carrier of SCM+FSA
c21 is Int-like Element of the carrier of SCM+FSA
c23 is FinSeq-Location
c22 := (c23,c21) 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(9,{},<*c22,c23,c21*>) is set
(c23,c21) := c22 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,{},<*c22,c23,c21*>) is set
{c21,c22} is non empty finite countable Element of bool Int-Locations

c25 is Int-like Element of the carrier of SCM+FSA
c25 =0_goto c26 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
c25 >0_goto c26 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

c27 is Int-like Element of the carrier of SCM+FSA
c28 is FinSeq-Location
c27 :=len c28 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(11,{},<*c27,c28*>) is set
c28 :=<0,...,0> c27 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,{},<*c27,c28*>) is set

c31 is Int-like Element of the carrier of SCM+FSA
c30 is Int-like Element of the carrier of SCM+FSA
c32 is FinSeq-Location
c31 := (c32,c30) 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(9,{},<*c31,c32,c30*>) is set
(c32,c30) := c31 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,{},<*c31,c32,c30*>) is set

{c30,c31} is non empty finite countable Element of bool Int-Locations
c33 is Int-like Element of the carrier of SCM+FSA
c34 is FinSeq-Location
c33 :=len c34 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(11,{},<*c33,c34*>) is set
c34 :=<0,...,0> c33 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,{},<*c33,c34*>) 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
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

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

K50(6,<*I*>,{}) is set
((goto I)) is finite countable Element of Fin Int-Locations

I is Int-like Element of the carrier 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
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 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

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

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

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

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

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

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

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

Union (I (#) n) is set
dom I is set
rng (I (#) n) is set
rng n is Element of bool

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

Union (I (#) t) is set

Union (I (#) P) is 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

Union (I (#) s) is set

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

[:n,:] is set

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

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

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

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

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

Union (I (#) t) is set

Union (n (#) P) is set

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

(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

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

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

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

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

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

dom (I (#) s) is 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

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 (#) t) is set

Union (n (#) P) is set

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

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

Union (I (#) t) is set

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

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
{ (b1 + n) where b1 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 : b1 in dom I } is set
Q is set
rng (Shift (I,n)) is finite countable Element of bool the InstructionsF of SCM+FSA

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

I . p is set

m is set
I . m is set

(Shift (I,n)) . (p + n) is set
I . p is 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

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

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

s is Int-like Element of the carrier of SCM+FSA
t 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
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

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

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

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

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