:: 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₁ where b₁ is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible Element of sproduct K423(3,SCM+FSA) : b₁ is finite } is set
[:(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₁₄ is Int-like Element of the carrier of SCM+FSA
c₁₅ is Int-like Element of the carrier of SCM+FSA
c₁₄ := c₁₅ 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 (c₁₄,c₁₅) 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 (c₁₄,c₁₅) 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 (c₁₄,c₁₅) 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 (c₁₄,c₁₅) 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
x9 is finite countable Element of Fin Int-Locations
{c₁₄,c₁₅} is non empty finite countable Element of bool Int-Locations
c₁₆ is Int-like Element of the carrier of SCM+FSA
c₁₇ is FinSeq-Location
c₁₆ :=len c₁₇ 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
<*c₁₆,c₁₇*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set
K50(11,{},<*c₁₆,c₁₇*>) is set
c₁₇ :=<0,...,0> c₁₆ 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,{},<*c₁₆,c₁₇*>) is set
{c₁₆} is non empty trivial finite 1 -element countable Element of bool Int-Locations
c₂₀ 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
c₁₉ is Int-like Element of the carrier of SCM+FSA
c₁₉ =0_goto c₂₀ 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
c₁₉ >0_goto c₂₀ 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
c₁₈ is finite countable Element of Fin Int-Locations
{c₁₉} is non empty trivial finite 1 -element countable Element of bool Int-Locations
c₂₂ is Int-like Element of the carrier of SCM+FSA
c₂₁ is Int-like Element of the carrier of SCM+FSA
c₂₃ is FinSeq-Location
c₂₂ := (c₂₃,c₂₁) 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
<*c₂₂,c₂₃,c₂₁*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set
K50(9,{},<*c₂₂,c₂₃,c₂₁*>) is set
(c₂₃,c₂₁) := c₂₂ 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,{},<*c₂₂,c₂₃,c₂₁*>) is set
{c₂₁,c₂₂} is non empty finite countable Element of bool Int-Locations
c₂₆ 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
c₂₅ is Int-like Element of the carrier of SCM+FSA
c₂₅ =0_goto c₂₆ 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
c₂₅ >0_goto c₂₆ 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
c₂₄ is finite countable Element of Fin Int-Locations
{c₂₅} is non empty trivial finite 1 -element countable Element of bool Int-Locations
c₂₇ is Int-like Element of the carrier of SCM+FSA
c₂₈ is FinSeq-Location
c₂₇ :=len c₂₈ 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
<*c₂₇,c₂₈*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set
K50(11,{},<*c₂₇,c₂₈*>) is set
c₂₈ :=<0,...,0> c₂₇ 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,{},<*c₂₇,c₂₈*>) is set
{c₂₇} is non empty trivial finite 1 -element countable Element of bool Int-Locations
c₃₁ is Int-like Element of the carrier of SCM+FSA
c₃₀ is Int-like Element of the carrier of SCM+FSA
c₃₂ is FinSeq-Location
c₃₁ := (c₃₂,c₃₀) 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
<*c₃₁,c₃₂,c₃₀*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set
K50(9,{},<*c₃₁,c₃₂,c₃₀*>) is set
(c₃₂,c₃₀) := c₃₁ 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,{},<*c₃₁,c₃₂,c₃₀*>) is set
c₂₉ is finite countable Element of Fin Int-Locations
{c₃₀,c₃₁} is non empty finite countable Element of bool Int-Locations
c₃₃ is Int-like Element of the carrier of SCM+FSA
c₃₄ is FinSeq-Location
c₃₃ :=len c₃₄ 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
<*c₃₃,c₃₄*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set
K50(11,{},<*c₃₃,c₃₄*>) is set
c₃₄ :=<0,...,0> c₃₃ 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,{},<*c₃₃,c₃₄*>) is set
{c₃₃} is non empty trivial finite 1 -element countable Element of bool Int-Locations
((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₁ + n) where b₁ 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 : b₁ in dom I } is set
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