:: 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 Element of NAT
t is Int-like Element of the carrier of SCM+FSA
t =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
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
t =0_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
{t} is non empty trivial finite 1 -element countable Element of bool Int-Locations
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
t is Int-like Element of the carrier of SCM+FSA
t >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
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
t >0_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
{t} is non empty trivial finite 1 -element countable Element of bool Int-Locations
t is Int-like Element of the carrier of SCM+FSA
s is Int-like Element of the carrier of SCM+FSA
P is FinSeq-Location
t := (P,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
<*t,P,s*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set
K50(9,{},<*t,P,s*>) is set
t is Int-like Element of the carrier of SCM+FSA
s is Int-like Element of the carrier of SCM+FSA
P is FinSeq-Location
(P,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,P,s*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set
K50(10,{},<*t,P,s*>) is set
s is Int-like Element of the carrier of SCM+FSA
t is FinSeq-Location
s :=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
<*s,t*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set
K50(11,{},<*s,t*>) is set
s is Int-like Element of the carrier of SCM+FSA
t is FinSeq-Location
t :=<0,...,0> 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
<*s,t*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set
K50(12,{},<*s,t*>) 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
IncAddr (I,n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
((IncAddr (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
(IncAddr (I,n)) (#) t is Relation-like Function-like finite countable set
m 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):]
(IncAddr (I,n)) (#) m is Relation-like Function-like finite countable set
Union ((IncAddr (I,n)) (#) m) is set
p is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
t . p is finite countable Element of Fin Int-Locations
m . p is finite countable Element of Fin Int-Locations
p is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(p) is finite countable Element of Fin Int-Locations
dom t is Element of bool the InstructionsF of SCM+FSA
bool the InstructionsF of SCM+FSA is cup-closed diff-closed preBoolean set
rng I is finite countable Element of bool the InstructionsF of SCM+FSA
rng (IncAddr (I,n)) is finite countable Element of bool the InstructionsF of SCM+FSA
dom ((IncAddr (I,n)) (#) t) is finite countable set
dom (IncAddr (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
dom (I (#) t) is finite countable set
p is set
I . p 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
(IncAddr (I,n)) . p is set
p1 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 /. p1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((I /. p1),n) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
p is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr (p,n) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((IncAddr (I,n)) (#) t) . p is set
f is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
t . f is finite countable Element of Fin Int-Locations
(f) is finite countable Element of Fin Int-Locations
(p) is finite countable Element of Fin Int-Locations
t . p is finite countable Element of Fin Int-Locations
(I (#) t) . p is set
I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() 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
Reloc (I,n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
IncAddr (I,n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Shift ((IncAddr (I,n)),n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable set
((Reloc (I,n))) is finite countable Element of bool Int-Locations
Shift (I,n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable set
IncAddr ((Shift (I,n)),n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable set
((Shift (I,n))) is finite countable Element of bool Int-Locations
I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
(I) is finite countable Element of bool Int-Locations
Directed I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
card I 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
Directed (I,(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
goto (card 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 (card I) is Element of the InstructionsF of SCM
<*(card I)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set
K50(6,<*(card I)*>,{}) is set
I +~ ((halt SCM+FSA),(goto (card I))) is set
((Directed I)) is finite countable Element of bool 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 finite countable set
Union (I (#) n) is set
dom n is Element of bool the InstructionsF of SCM+FSA
bool the InstructionsF of SCM+FSA is cup-closed diff-closed preBoolean set
n . (halt SCM+FSA) is finite countable Element of Fin 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):]
(Directed I) (#) s is Relation-like Function-like finite countable set
Union ((Directed I) (#) s) is set
t is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
n . t is finite countable Element of Fin Int-Locations
s . t is finite countable Element of Fin Int-Locations
P is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(P) is finite countable Element of Fin Int-Locations
n . (goto (card I)) is finite countable Element of Fin Int-Locations
((goto (card I))) is finite countable Element of Fin Int-Locations
rng I is finite countable Element of bool the InstructionsF of SCM+FSA
(Directed I) (#) n is Relation-like Function-like finite countable set
id the InstructionsF of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one non empty total V18( the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA) Element of bool [: the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA:]
[: the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA:] is set
bool [: the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA:] is cup-closed diff-closed preBoolean set
(id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card I))) is Relation-like the InstructionsF of SCM+FSA -defined the InstructionsF of SCM+FSA -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA) Element of bool [: the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA:]
I (#) ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card I)))) is Relation-like Function-like finite countable set
(I (#) ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card I))))) (#) n is Relation-like Function-like finite countable set
n * ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card I)))) 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 * ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card I))))) is Relation-like Function-like finite countable set
I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
(I) is finite countable Element of bool Int-Locations
n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
I ";" n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
stop I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant non empty trivial finite 1 -element countable V109() non halt-free V118( SCM+FSA ) V119( SCM+FSA ) V142(3, SCM+FSA ) set
K391((halt SCM+FSA)) is set
K381(I,(Stop SCM+FSA)) is Relation-like Function-like T-Sequence-like set
CutLastLoc (stop I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
Directed (CutLastLoc (stop I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
card (CutLastLoc (stop 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
Directed ((CutLastLoc (stop I)),(card (CutLastLoc (stop I)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
goto (card (CutLastLoc (stop 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 (card (CutLastLoc (stop I))) is Element of the InstructionsF of SCM
<*(card (CutLastLoc (stop I)))*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set
K50(6,<*(card (CutLastLoc (stop I)))*>,{}) is set
(CutLastLoc (stop I)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop I))))) is set
card I 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
Reloc (n,(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
IncAddr (n,(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Shift ((IncAddr (n,(card I))),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable set
(Directed (CutLastLoc (stop I))) +* (Reloc (n,(card I))) is Relation-like Function-like finite countable set
((I ";" n)) is finite countable Element of bool Int-Locations
(n) is finite countable Element of bool Int-Locations
(I) \/ (n) is finite countable Element of bool Int-Locations
dom I is V51() V52() V53() V54() V55() V56() finite V69() V70() V71() countable Element of bool NAT
Directed I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
Directed (I,(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
goto (card 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 (card I) is Element of the InstructionsF of SCM
<*(card I)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set
K50(6,<*(card I)*>,{}) is set
I +~ ((halt SCM+FSA),(goto (card I))) is set
dom (Directed I) is V51() V52() V53() V54() V55() V56() finite V69() V70() V71() countable Element of bool NAT
dom (Reloc (n,(card I))) is V51() V52() V53() V54() V55() V56() finite V69() V70() V71() countable Element of bool NAT
((Directed I)) is finite countable Element of bool Int-Locations
((Reloc (n,(card I)))) is finite countable Element of bool Int-Locations
((Directed I)) \/ ((Reloc (n,(card I)))) is finite countable Element of bool Int-Locations
(I) \/ ((Reloc (n,(card I)))) is finite countable Element of bool Int-Locations
I is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Macro I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
K419(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
stop K419(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
((Macro I)) is finite countable Element of bool Int-Locations
(I) 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):]
(Macro I) (#) n is Relation-like Function-like finite countable set
Union ((Macro I) (#) n) is set
rng (Macro 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
{I,(halt SCM+FSA)} is non empty finite countable set
dom n is Element of bool the InstructionsF of SCM+FSA
rng ((Macro I) (#) n) is finite countable set
union (rng ((Macro I) (#) n)) is set
n .: (rng (Macro I)) is finite countable Element of bool (Fin Int-Locations)
bool (Fin Int-Locations) is cup-closed diff-closed preBoolean set
union (n .: (rng (Macro I))) is set
n . I is finite countable Element of Fin Int-Locations
n . (halt SCM+FSA) is finite countable Element of Fin Int-Locations
{(n . I),(n . (halt SCM+FSA))} is non empty finite V62() countable set
union {(n . I),(n . (halt SCM+FSA))} is finite countable set
(n . I) \/ (n . (halt SCM+FSA)) is finite countable Element of Fin Int-Locations
(I) \/ (n . (halt SCM+FSA)) is finite countable Element of Fin Int-Locations
(I) \/ ((halt SCM+FSA)) is finite countable Element of Fin Int-Locations
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 non empty finite countable V109() set
I ";" n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Macro I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
K419(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
stop K419(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
(Macro I) ";" n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
stop (Macro I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant non empty trivial finite 1 -element countable V109() non halt-free V118( SCM+FSA ) V119( SCM+FSA ) V142(3, SCM+FSA ) set
K391((halt SCM+FSA)) is set
K381((Macro I),(Stop SCM+FSA)) is Relation-like Function-like T-Sequence-like set
CutLastLoc (stop (Macro I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
Directed (CutLastLoc (stop (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
card (CutLastLoc (stop (Macro 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
Directed ((CutLastLoc (stop (Macro I))),(card (CutLastLoc (stop (Macro I))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
goto (card (CutLastLoc (stop (Macro 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 (card (CutLastLoc (stop (Macro I)))) is Element of the InstructionsF of SCM
<*(card (CutLastLoc (stop (Macro I))))*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set
K50(6,<*(card (CutLastLoc (stop (Macro I))))*>,{}) is set
(CutLastLoc (stop (Macro I))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro I)))))) is set
card (Macro I) 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
Reloc (n,(card (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
IncAddr (n,(card (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Shift ((IncAddr (n,(card (Macro I)))),(card (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable set
(Directed (CutLastLoc (stop (Macro I)))) +* (Reloc (n,(card (Macro I)))) is Relation-like Function-like finite countable set
((I ";" n)) is finite countable Element of bool Int-Locations
(n) is finite countable Element of bool Int-Locations
(I) \/ (n) is finite countable set
((Macro I)) is finite countable Element of bool Int-Locations
((Macro I)) \/ (n) is finite countable Element of bool Int-Locations
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 non empty finite countable V109() set
n ";" I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Macro I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
K419(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
stop K419(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
n ";" (Macro I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
stop n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant non empty trivial finite 1 -element countable V109() non halt-free V118( SCM+FSA ) V119( SCM+FSA ) V142(3, SCM+FSA ) set
K391((halt SCM+FSA)) is set
K381(n,(Stop SCM+FSA)) is Relation-like Function-like T-Sequence-like set
CutLastLoc (stop n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
Directed (CutLastLoc (stop n)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
card (CutLastLoc (stop 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
Directed ((CutLastLoc (stop n)),(card (CutLastLoc (stop n)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
goto (card (CutLastLoc (stop 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 (card (CutLastLoc (stop n))) is Element of the InstructionsF of SCM
<*(card (CutLastLoc (stop n)))*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set
K50(6,<*(card (CutLastLoc (stop n)))*>,{}) is set
(CutLastLoc (stop n)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop n))))) is set
card n 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
Reloc ((Macro I),(card n)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
IncAddr ((Macro I),(card n)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Shift ((IncAddr ((Macro I),(card n))),(card n)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable set
(Directed (CutLastLoc (stop n))) +* (Reloc ((Macro I),(card n))) is Relation-like Function-like finite countable set
((n ";" I)) is finite countable Element of bool Int-Locations
(n) is finite countable Element of bool Int-Locations
(n) \/ (I) is finite countable set
((Macro I)) is finite countable Element of bool Int-Locations
(n) \/ ((Macro I)) is finite countable Element of bool Int-Locations
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 with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
I ";" n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Macro I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
K419(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
stop K419(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
Macro n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
K419(SCM+FSA,n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
stop K419(SCM+FSA,n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
(Macro I) ";" (Macro n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
stop (Macro I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant non empty trivial finite 1 -element countable V109() non halt-free V118( SCM+FSA ) V119( SCM+FSA ) V142(3, SCM+FSA ) set
K391((halt SCM+FSA)) is set
K381((Macro I),(Stop SCM+FSA)) is Relation-like Function-like T-Sequence-like set
CutLastLoc (stop (Macro I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
Directed (CutLastLoc (stop (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
card (CutLastLoc (stop (Macro 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
Directed ((CutLastLoc (stop (Macro I))),(card (CutLastLoc (stop (Macro I))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
goto (card (CutLastLoc (stop (Macro 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 (card (CutLastLoc (stop (Macro I)))) is Element of the InstructionsF of SCM
<*(card (CutLastLoc (stop (Macro I))))*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set
K50(6,<*(card (CutLastLoc (stop (Macro I))))*>,{}) is set
(CutLastLoc (stop (Macro I))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro I)))))) is set
card (Macro I) 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
Reloc ((Macro n),(card (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
IncAddr ((Macro n),(card (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Shift ((IncAddr ((Macro n),(card (Macro I)))),(card (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable set
(Directed (CutLastLoc (stop (Macro I)))) +* (Reloc ((Macro n),(card (Macro I)))) is Relation-like Function-like finite countable set
((I ";" n)) is finite countable Element of bool Int-Locations
(n) is finite countable Element of Fin Int-Locations
(I) \/ (n) is finite countable Element of Fin Int-Locations
((Macro I)) is finite countable Element of bool Int-Locations
((Macro n)) is finite countable Element of bool Int-Locations
((Macro I)) \/ ((Macro n)) is finite countable Element of bool Int-Locations
((Macro I)) \/ (n) is finite countable 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
Fin FinSeq-Locations is non empty cup-closed diff-closed preBoolean set
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 FinSeq-Locations
{.P.} is non empty trivial finite 1 -element countable Element of Fin FinSeq-Locations
Q is finite countable Element of Fin FinSeq-Locations
p is Int-like Element of the carrier of SCM+FSA
p is Int-like Element of the carrier of SCM+FSA
i is FinSeq-Location
p := (i,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
<*p,i,p*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set
K50(9,{},<*p,i,p*>) is set
(i,p) := 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,i,p*>) is set
m is finite countable Element of Fin FinSeq-Locations
{i} is non empty trivial finite 1 -element countable set
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 FinSeq-Locations
{.t.} is non empty trivial finite 1 -element countable Element of Fin FinSeq-Locations
P is finite countable Element of Fin FinSeq-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 FinSeq-Locations
{p} is non empty trivial finite 1 -element countable set
n is finite countable Element of Fin FinSeq-Locations
s is finite countable Element of Fin FinSeq-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
{Q} is non empty trivial finite 1 -element countable set
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
{p} is non empty trivial finite 1 -element countable set
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
{P} is non empty trivial finite 1 -element countable set
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
{m} is non empty trivial finite 1 -element countable set
t is Int-like Element of the carrier of SCM+FSA
s is Int-like Element of the carrier of SCM+FSA
P is FinSeq-Location
t := (P,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
<*t,P,s*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set
K50(9,{},<*t,P,s*>) is set
(P,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,P,s*>) is set
n is finite countable Element of Fin FinSeq-Locations
{P} is non empty trivial finite 1 -element countable set
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
{m} is non empty trivial finite 1 -element countable 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
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
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
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
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 with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(t) is finite countable Element of Fin FinSeq-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
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 := (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
{s} is non empty trivial finite 1 -element countable set
t is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(t) is finite countable Element of Fin FinSeq-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 FinSeq-Locations
I is Int-like Element of the carrier of SCM+FSA
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
{n} is non empty trivial finite 1 -element countable set
s is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(s) is finite countable Element of Fin FinSeq-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 FinSeq-Locations
[: the InstructionsF of SCM+FSA,(Fin FinSeq-Locations):] is set
bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-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 FinSeq-Locations
t is finite countable Element of Fin FinSeq-Locations
n is Relation-like the InstructionsF of SCM+FSA -defined Fin FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-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 FinSeq-Locations)
bool (Fin FinSeq-Locations) is cup-closed diff-closed preBoolean set
union (rng (I (#) n)) is set
union (bool FinSeq-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 FinSeq-Locations
(Q) is finite countable Element of Fin FinSeq-Locations
m is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(m) is finite countable Element of Fin FinSeq-Locations
n is Element of bool FinSeq-Locations
s is Element of bool FinSeq-Locations
t is Relation-like the InstructionsF of SCM+FSA -defined Fin FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-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 FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-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 FinSeq-Locations
P . Q is finite countable Element of Fin FinSeq-Locations
m is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(m) is finite countable Element of Fin FinSeq-Locations
I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
(I) is Element of bool FinSeq-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 FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-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 FinSeq-Locations):] is set
bool [:n,(Fin FinSeq-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 FinSeq-Locations -valued Function-like total V18(n, Fin FinSeq-Locations) finite countable Element of bool [:n,(Fin FinSeq-Locations):]
P is Relation-like n -defined Fin FinSeq-Locations -valued Function-like total V18(n, Fin FinSeq-Locations) finite countable Element of bool [:n,(Fin FinSeq-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 FinSeq-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 FinSeq-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 FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-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 FinSeq-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 FinSeq-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 FinSeq-Locations
(n) is finite countable Element of bool FinSeq-Locations
(I) \/ (n) is finite countable Element of bool FinSeq-Locations
s is Relation-like the InstructionsF of SCM+FSA -defined Fin FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-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 FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-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 FinSeq-Locations
t . P is finite countable Element of Fin FinSeq-Locations
Q is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Q) is finite countable Element of Fin FinSeq-Locations
P is Relation-like the InstructionsF of SCM+FSA -defined Fin FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-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 FinSeq-Locations
P . Q is finite countable Element of Fin FinSeq-Locations
m is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(m) is finite countable Element of Fin FinSeq-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 FinSeq-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 FinSeq-Locations
(n) is finite countable Element of bool FinSeq-Locations
(I) \/ (n) is finite countable Element of bool FinSeq-Locations
s is Relation-like the InstructionsF of SCM+FSA -defined Fin FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-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 FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-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 FinSeq-Locations
t . P is finite countable Element of Fin FinSeq-Locations
Q is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Q) is finite countable Element of Fin FinSeq-Locations
P is Relation-like the InstructionsF of SCM+FSA -defined Fin FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-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 FinSeq-Locations
P . Q is finite countable Element of Fin FinSeq-Locations
m is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(m) is finite countable Element of Fin FinSeq-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 FinSeq-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 FinSeq-Locations
t is Relation-like the InstructionsF of SCM+FSA -defined Fin FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-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 FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-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 FinSeq-Locations
P . Q is finite countable Element of Fin FinSeq-Locations
m is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(m) is finite countable Element of Fin FinSeq-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 FinSeq-Locations)
bool (Fin FinSeq-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 FinSeq-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 FinSeq-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 Element of NAT
t is Int-like Element of the carrier of SCM+FSA
t =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
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
t =0_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
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
t is Int-like Element of the carrier of SCM+FSA
t >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
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
t >0_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
t is Int-like Element of the carrier of SCM+FSA
s is Int-like Element of the carrier of SCM+FSA
P is FinSeq-Location
t := (P,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
<*t,P,s*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set
K50(9,{},<*t,P,s*>) is set
t is Int-like Element of the carrier of SCM+FSA
s is Int-like Element of the carrier of SCM+FSA
P is FinSeq-Location
(P,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,P,s*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set
K50(10,{},<*t,P,s*>) is set
s is Int-like Element of the carrier of SCM+FSA
t is FinSeq-Location
s :=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
<*s,t*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set
K50(11,{},<*s,t*>) is set
s is Int-like Element of the carrier of SCM+FSA
t is FinSeq-Location
t :=<0,...,0> 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
<*s,t*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set
K50(12,{},<*s,t*>) 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 FinSeq-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 Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
((IncAddr (I,n))) is finite countable Element of bool FinSeq-Locations
t is Relation-like the InstructionsF of SCM+FSA -defined Fin FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-Locations):]
I (#) t is Relation-like Function-like finite countable set
Union (I (#) t) is set
(IncAddr (I,n)) (#) t is Relation-like Function-like finite countable set
m is Relation-like the InstructionsF of SCM+FSA -defined Fin FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-Locations):]
(IncAddr (I,n)) (#) m is Relation-like Function-like finite countable set
Union ((IncAddr (I,n)) (#) m) is set
p is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
t . p is finite countable Element of Fin FinSeq-Locations
m . p is finite countable Element of Fin FinSeq-Locations
p is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(p) is finite countable Element of Fin FinSeq-Locations
dom t is Element of bool the InstructionsF of SCM+FSA
bool the InstructionsF of SCM+FSA is cup-closed diff-closed preBoolean set
rng I is finite countable Element of bool the InstructionsF of SCM+FSA
rng (IncAddr (I,n)) is finite countable Element of bool the InstructionsF of SCM+FSA
dom ((IncAddr (I,n)) (#) t) is finite countable set
dom (IncAddr (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
dom (I (#) t) is finite countable set
p is set
I . p 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
(IncAddr (I,n)) . p is set
p1 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 /. p1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((I /. p1),n) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
p is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr (p,n) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((IncAddr (I,n)) (#) t) . p is set
f is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
t . f is finite countable Element of Fin FinSeq-Locations
(f) is finite countable Element of Fin FinSeq-Locations
(p) is finite countable Element of Fin FinSeq-Locations
t . p is finite countable Element of Fin FinSeq-Locations
(I (#) t) . p is set
I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
(I) is finite countable Element of bool FinSeq-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
Reloc (I,n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
IncAddr (I,n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Shift ((IncAddr (I,n)),n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable set
((Reloc (I,n))) is finite countable Element of bool FinSeq-Locations
Shift (I,n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable set
IncAddr ((Shift (I,n)),n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable set
((Shift (I,n))) is finite countable Element of bool FinSeq-Locations
I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
(I) is finite countable Element of bool FinSeq-Locations
Directed I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
card I 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
Directed (I,(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
goto (card 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 (card I) is Element of the InstructionsF of SCM
<*(card I)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set
K50(6,<*(card I)*>,{}) is set
I +~ ((halt SCM+FSA),(goto (card I))) is set
((Directed I)) is finite countable Element of bool FinSeq-Locations
n is Relation-like the InstructionsF of SCM+FSA -defined Fin FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-Locations):]
I (#) n is Relation-like Function-like finite countable set
Union (I (#) n) is set
n . (halt SCM+FSA) is finite countable Element of Fin FinSeq-Locations
((halt SCM+FSA)) is finite countable Element of Fin FinSeq-Locations
s is Relation-like the InstructionsF of SCM+FSA -defined Fin FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-Locations):]
(Directed I) (#) s is Relation-like Function-like finite countable set
Union ((Directed I) (#) s) is set
t is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
n . t is finite countable Element of Fin FinSeq-Locations
s . t is finite countable Element of Fin FinSeq-Locations
P is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(P) is finite countable Element of Fin FinSeq-Locations
n . (goto (card I)) is finite countable Element of Fin FinSeq-Locations
((goto (card I))) is finite countable Element of Fin FinSeq-Locations
dom n is Element of bool the InstructionsF of SCM+FSA
bool the InstructionsF of SCM+FSA is cup-closed diff-closed preBoolean set
rng I is finite countable Element of bool the InstructionsF of SCM+FSA
(Directed I) (#) n is Relation-like Function-like finite countable set
id the InstructionsF of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one non empty total V18( the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA) Element of bool [: the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA:]
[: the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA:] is set
bool [: the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA:] is cup-closed diff-closed preBoolean set
(id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card I))) is Relation-like the InstructionsF of SCM+FSA -defined the InstructionsF of SCM+FSA -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA) Element of bool [: the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA:]
I (#) ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card I)))) is Relation-like Function-like finite countable set
(I (#) ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card I))))) (#) n is Relation-like Function-like finite countable set
n * ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card I)))) is Relation-like the InstructionsF of SCM+FSA -defined Fin FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-Locations):]
I (#) (n * ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card I))))) is Relation-like Function-like finite countable set
I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
(I) is finite countable Element of bool FinSeq-Locations
n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
I ";" n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
stop I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant non empty trivial finite 1 -element countable V109() non halt-free V118( SCM+FSA ) V119( SCM+FSA ) V142(3, SCM+FSA ) set
K391((halt SCM+FSA)) is set
K381(I,(Stop SCM+FSA)) is Relation-like Function-like T-Sequence-like set
CutLastLoc (stop I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
Directed (CutLastLoc (stop I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
card (CutLastLoc (stop 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
Directed ((CutLastLoc (stop I)),(card (CutLastLoc (stop I)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
goto (card (CutLastLoc (stop 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 (card (CutLastLoc (stop I))) is Element of the InstructionsF of SCM
<*(card (CutLastLoc (stop I)))*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set
K50(6,<*(card (CutLastLoc (stop I)))*>,{}) is set
(CutLastLoc (stop I)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop I))))) is set
card I 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
Reloc (n,(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
IncAddr (n,(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Shift ((IncAddr (n,(card I))),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable set
(Directed (CutLastLoc (stop I))) +* (Reloc (n,(card I))) is Relation-like Function-like finite countable set
((I ";" n)) is finite countable Element of bool FinSeq-Locations
(n) is finite countable Element of bool FinSeq-Locations
(I) \/ (n) is finite countable Element of bool FinSeq-Locations
dom I is V51() V52() V53() V54() V55() V56() finite V69() V70() V71() countable Element of bool NAT
Directed I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
Directed (I,(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
goto (card 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 (card I) is Element of the InstructionsF of SCM
<*(card I)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set
K50(6,<*(card I)*>,{}) is set
I +~ ((halt SCM+FSA),(goto (card I))) is set
dom (Directed I) is V51() V52() V53() V54() V55() V56() finite V69() V70() V71() countable Element of bool NAT
dom (Reloc (n,(card I))) is V51() V52() V53() V54() V55() V56() finite V69() V70() V71() countable Element of bool NAT
((Directed I)) is finite countable Element of bool FinSeq-Locations
((Reloc (n,(card I)))) is finite countable Element of bool FinSeq-Locations
((Directed I)) \/ ((Reloc (n,(card I)))) is finite countable Element of bool FinSeq-Locations
(I) \/ ((Reloc (n,(card I)))) is finite countable Element of bool FinSeq-Locations
I is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Macro I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
K419(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
stop K419(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
((Macro I)) is finite countable Element of bool FinSeq-Locations
(I) is finite countable Element of Fin FinSeq-Locations
n is Relation-like the InstructionsF of SCM+FSA -defined Fin FinSeq-Locations -valued Function-like non empty total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of bool [: the InstructionsF of SCM+FSA,(Fin FinSeq-Locations):]
(Macro I) (#) n is Relation-like Function-like finite countable set
Union ((Macro I) (#) n) is set
rng (Macro 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
{I,(halt SCM+FSA)} is non empty finite countable set
dom n is Element of bool the InstructionsF of SCM+FSA
rng ((Macro I) (#) n) is finite countable set
union (rng ((Macro I) (#) n)) is set
n .: (rng (Macro I)) is finite countable Element of bool (Fin FinSeq-Locations)
bool (Fin FinSeq-Locations) is cup-closed diff-closed preBoolean set
union (n .: (rng (Macro I))) is set
n . I is finite countable Element of Fin FinSeq-Locations
n . (halt SCM+FSA) is finite countable Element of Fin FinSeq-Locations
{(n . I),(n . (halt SCM+FSA))} is non empty finite V62() countable set
union {(n . I),(n . (halt SCM+FSA))} is finite countable set
(n . I) \/ (n . (halt SCM+FSA)) is finite countable Element of Fin FinSeq-Locations
(I) \/ (n . (halt SCM+FSA)) is finite countable Element of Fin FinSeq-Locations
((halt SCM+FSA)) is finite countable Element of Fin FinSeq-Locations
(I) \/ ((halt SCM+FSA)) is finite countable Element of Fin FinSeq-Locations
(I) \/ {} 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 FinSeq-Locations
n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
I ";" n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Macro I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
K419(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
stop K419(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
(Macro I) ";" n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
stop (Macro I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant non empty trivial finite 1 -element countable V109() non halt-free V118( SCM+FSA ) V119( SCM+FSA ) V142(3, SCM+FSA ) set
K391((halt SCM+FSA)) is set
K381((Macro I),(Stop SCM+FSA)) is Relation-like Function-like T-Sequence-like set
CutLastLoc (stop (Macro I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
Directed (CutLastLoc (stop (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
card (CutLastLoc (stop (Macro 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
Directed ((CutLastLoc (stop (Macro I))),(card (CutLastLoc (stop (Macro I))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
goto (card (CutLastLoc (stop (Macro 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 (card (CutLastLoc (stop (Macro I)))) is Element of the InstructionsF of SCM
<*(card (CutLastLoc (stop (Macro I))))*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set
K50(6,<*(card (CutLastLoc (stop (Macro I))))*>,{}) is set
(CutLastLoc (stop (Macro I))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro I)))))) is set
card (Macro I) 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
Reloc (n,(card (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
IncAddr (n,(card (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Shift ((IncAddr (n,(card (Macro I)))),(card (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable set
(Directed (CutLastLoc (stop (Macro I)))) +* (Reloc (n,(card (Macro I)))) is Relation-like Function-like finite countable set
((I ";" n)) is finite countable Element of bool FinSeq-Locations
(n) is finite countable Element of bool FinSeq-Locations
(I) \/ (n) is finite countable set
((Macro I)) is finite countable Element of bool FinSeq-Locations
((Macro I)) \/ (n) is finite countable Element of bool FinSeq-Locations
I is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(I) is finite countable Element of Fin FinSeq-Locations
n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
n ";" I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Macro I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
K419(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
stop K419(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
n ";" (Macro I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
stop n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant non empty trivial finite 1 -element countable V109() non halt-free V118( SCM+FSA ) V119( SCM+FSA ) V142(3, SCM+FSA ) set
K391((halt SCM+FSA)) is set
K381(n,(Stop SCM+FSA)) is Relation-like Function-like T-Sequence-like set
CutLastLoc (stop n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
Directed (CutLastLoc (stop n)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
card (CutLastLoc (stop 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
Directed ((CutLastLoc (stop n)),(card (CutLastLoc (stop n)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
goto (card (CutLastLoc (stop 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 (card (CutLastLoc (stop n))) is Element of the InstructionsF of SCM
<*(card (CutLastLoc (stop n)))*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set
K50(6,<*(card (CutLastLoc (stop n)))*>,{}) is set
(CutLastLoc (stop n)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop n))))) is set
card n 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
Reloc ((Macro I),(card n)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
IncAddr ((Macro I),(card n)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Shift ((IncAddr ((Macro I),(card n))),(card n)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable set
(Directed (CutLastLoc (stop n))) +* (Reloc ((Macro I),(card n))) is Relation-like Function-like finite countable set
((n ";" I)) is finite countable Element of bool FinSeq-Locations
(n) is finite countable Element of bool FinSeq-Locations
(n) \/ (I) is finite countable set
((Macro I)) is finite countable Element of bool FinSeq-Locations
(n) \/ ((Macro I)) is finite countable Element of bool FinSeq-Locations
I is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(I) is finite countable Element of Fin FinSeq-Locations
n is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
I ";" n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Macro I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
K419(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
stop K419(SCM+FSA,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
Macro n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
K419(SCM+FSA,n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
stop K419(SCM+FSA,n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
(Macro I) ";" (Macro n) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
stop (Macro I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant non empty trivial finite 1 -element countable V109() non halt-free V118( SCM+FSA ) V119( SCM+FSA ) V142(3, SCM+FSA ) set
K391((halt SCM+FSA)) is set
K381((Macro I),(Stop SCM+FSA)) is Relation-like Function-like T-Sequence-like set
CutLastLoc (stop (Macro I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
Directed (CutLastLoc (stop (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
card (CutLastLoc (stop (Macro 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
Directed ((CutLastLoc (stop (Macro I))),(card (CutLastLoc (stop (Macro I))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
goto (card (CutLastLoc (stop (Macro 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 (card (CutLastLoc (stop (Macro I)))) is Element of the InstructionsF of SCM
<*(card (CutLastLoc (stop (Macro I))))*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set
K50(6,<*(card (CutLastLoc (stop (Macro I))))*>,{}) is set
(CutLastLoc (stop (Macro I))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro I)))))) is set
card (Macro I) 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
Reloc ((Macro n),(card (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
IncAddr ((Macro n),(card (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
Shift ((IncAddr ((Macro n),(card (Macro I)))),(card (Macro I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable set
(Directed (CutLastLoc (stop (Macro I)))) +* (Reloc ((Macro n),(card (Macro I)))) is Relation-like Function-like finite countable set
((I ";" n)) is finite countable Element of bool FinSeq-Locations
(n) is finite countable Element of Fin FinSeq-Locations
(I) \/ (n) is finite countable Element of Fin FinSeq-Locations
((Macro I)) is finite countable Element of bool FinSeq-Locations
((Macro n)) is finite countable Element of bool FinSeq-Locations
((Macro I)) \/ ((Macro n)) is finite countable Element of bool FinSeq-Locations
((Macro I)) \/ (n) is finite countable set
I is finite countable Element of bool Int-Locations
FirstNotIn I is Int-like Element of the carrier of SCM+FSA
s is finite countable Element of bool Int-Locations
FirstNotIn s is Int-like Element of the carrier of SCM+FSA
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
intloc I is Int-like Element of the carrier of SCM+FSA
dl. I is Int-like Element of the carrier of SCM
[1,I] is non empty non natural 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
intloc n is Int-like Element of the carrier of SCM+FSA
dl. n is Int-like Element of the carrier of SCM
[1,n] is non empty non natural 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
{(intloc 0)} is non empty trivial finite 1 -element countable Element of bool Int-Locations
(I) \/ {(intloc 0)} is non empty finite countable 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 finite countable Element of bool Int-Locations
FirstNotIn s is Int-like Element of the carrier of SCM+FSA
t is finite countable Element of bool Int-Locations
n is Int-like Element of the carrier of SCM+FSA
FirstNotIn t is Int-like Element of the carrier of SCM+FSA
P is finite countable Element of bool Int-Locations
s is Int-like Element of the carrier of SCM+FSA
FirstNotIn P is Int-like Element of the carrier of SCM+FSA
I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
(I) is Int-like Element of the carrier of SCM+FSA
(I) is finite countable Element of bool Int-Locations
(I) \/ {(intloc 0)} is non empty finite countable Element of bool Int-Locations
n is finite countable Element of bool Int-Locations
FirstNotIn n is Int-like Element of the carrier of SCM+FSA
I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
(I) is Int-like non read-only Element of the carrier of SCM+FSA
(I) is finite countable Element of bool Int-Locations
(I) \/ {(intloc 0)} is non empty finite countable Element of bool Int-Locations
n is finite countable Element of bool Int-Locations
FirstNotIn n is Int-like Element of 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
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
s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
rng s is finite countable Element of bool the InstructionsF of SCM+FSA
bool the InstructionsF of SCM+FSA is cup-closed diff-closed preBoolean set
(s) is Int-like non read-only Element of the carrier of SCM+FSA
t is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(t) is finite countable Element of Fin Int-Locations
{I,n} is non empty finite countable Element of bool Int-Locations
(s) is finite countable Element of bool Int-Locations
I is Int-like Element of the carrier of SCM+FSA
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 Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
rng s is finite countable Element of bool the InstructionsF of SCM+FSA
bool the InstructionsF of SCM+FSA is cup-closed diff-closed preBoolean set
(s) is Int-like non read-only Element of the carrier of SCM+FSA
t is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(t) is finite countable Element of Fin Int-Locations
{I} is non empty trivial finite 1 -element countable Element of bool Int-Locations
(s) is finite countable Element of bool Int-Locations
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 := (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 Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
rng t is finite countable Element of bool the InstructionsF of SCM+FSA
bool the InstructionsF of SCM+FSA is cup-closed diff-closed preBoolean set
(t) is Int-like non read-only Element of the carrier of SCM+FSA
P is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(P) is finite countable Element of Fin Int-Locations
{n,I} is non empty finite countable Element of bool Int-Locations
(t) is finite countable Element of bool Int-Locations
I is Int-like Element of the carrier of SCM+FSA
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 Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
rng s is finite countable Element of bool the InstructionsF of SCM+FSA
bool the InstructionsF of SCM+FSA is cup-closed diff-closed preBoolean set
(s) is Int-like non read-only Element of the carrier of SCM+FSA
t is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(t) is finite countable Element of Fin Int-Locations
{I} is non empty trivial finite 1 -element countable Element of bool Int-Locations
(s) is finite countable Element of bool Int-Locations
I is finite countable Element of bool FinSeq-Locations
First*NotIn I is FinSeq-Location
s is finite countable Element of bool FinSeq-Locations
First*NotIn s is FinSeq-Location
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
fsloc I is FinSeq-Location
I + 1 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 + 1) is V33() V34() integer ext-real 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
fsloc n is FinSeq-Location
n + 1 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 + 1) is V33() V34() integer ext-real 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 FinSeq-Locations
First*NotIn (I) is FinSeq-Location
t is finite countable Element of bool FinSeq-Locations
n is FinSeq-Location
First*NotIn t is FinSeq-Location
P is finite countable Element of bool FinSeq-Locations
s is FinSeq-Location
First*NotIn P is FinSeq-Location
I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
(I) is FinSeq-Location
(I) is finite countable Element of bool FinSeq-Locations
n is finite countable Element of bool FinSeq-Locations
First*NotIn n is FinSeq-Location
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 := (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 Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
rng t is finite countable Element of bool the InstructionsF of SCM+FSA
bool the InstructionsF of SCM+FSA is cup-closed diff-closed preBoolean set
(t) is FinSeq-Location
P is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(P) is finite countable Element of Fin FinSeq-Locations
{s} is non empty trivial finite 1 -element countable set
(t) is finite countable Element of bool FinSeq-Locations
I is Int-like Element of the carrier of SCM+FSA
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 Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite countable set
rng s is finite countable Element of bool the InstructionsF of SCM+FSA
bool the InstructionsF of SCM+FSA is cup-closed diff-closed preBoolean set
(s) is FinSeq-Location
t is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(t) is finite countable Element of Fin FinSeq-Locations
{n} is non empty trivial finite 1 -element countable set
(s) is finite countable Element of bool FinSeq-Locations
I is Int-like Element of the carrier of SCM+FSA
n is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(n) is finite countable Element of Fin Int-Locations
s is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
Exec (n,s) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA) is functional with_common_domain product-like set
K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) is functional non empty set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) -valued Function-like non empty total V18( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) Element of bool [: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):]
[: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):] is set
bool [: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):] is cup-closed diff-closed preBoolean set
the Execution of SCM+FSA . n is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
( the Execution of SCM+FSA . n) . s is set
(Exec (n,s)) . I is V33() V34() integer ext-real set
s . I is V33() V34() integer ext-real set
InsCode n 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 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
{t,P} is non empty finite countable Element of bool Int-Locations
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
{t,P} is non empty finite countable Element of bool Int-Locations
t is Int-like Element of the carrier of SCM+FSA
P is Int-like Element of the carrier 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
{t,P} is non empty finite countable Element of bool Int-Locations
t is Int-like Element of the carrier of SCM+FSA
P is Int-like Element of the carrier 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
{t,P} is non empty finite countable Element of bool Int-Locations
t is Int-like Element of the carrier of SCM+FSA
P is Int-like Element of the carrier 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
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
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
SCM-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
K50(6,<*t*>,{}) is set
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
P is Int-like Element of the carrier of SCM+FSA
P =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
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
P is Int-like Element of the carrier of SCM+FSA
P >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+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
{t,P} is non empty finite 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
(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
<*P,Q,t*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set
K50(10,{},<*P,Q,t*>) is set
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
{t} is non empty trivial finite 1 -element countable Element of bool Int-Locations
t is Int-like Element of the carrier of SCM+FSA
P is FinSeq-Location
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
<*t,P*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set
K50(12,{},<*t,P*>) is set
I is Int-like Element of the carrier of SCM+FSA
n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
dom n is V51() V52() V53() V54() V55() V56() finite V69() V70() V71() countable Element of bool NAT
(n) is finite countable Element of bool Int-Locations
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
t is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
t . I is V33() V34() integer ext-real set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set
Comput (P,t,s) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
(Comput (P,t,s)) . I is V33() V34() integer ext-real set
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
Comput (P,t,Q) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
(Comput (P,t,Q)) . I is V33() V34() integer ext-real set
Q + 1 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
Comput (P,t,(Q + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
(Comput (P,t,(Q + 1))) . I is V33() V34() integer ext-real set
IC (Comput (P,t,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
(Comput (P,t,Q)) . (IC ) is set
n . (IC (Comput (P,t,Q))) is 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
dom P is V51() V52() V53() V54() V55() V56() V69() countable Element of bool NAT
P /. (IC (Comput (P,t,Q))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P . (IC (Comput (P,t,Q))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((P . (IC (Comput (P,t,Q))))) is finite countable Element of Fin Int-Locations
Following (P,(Comput (P,t,Q))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
CurInstr (P,(Comput (P,t,Q))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P,(Comput (P,t,Q)))),(Comput (P,t,Q))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA) is functional with_common_domain product-like set
K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) is functional non empty set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) -valued Function-like non empty total V18( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) Element of bool [: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):]
[: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):] is set
bool [: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):] is cup-closed diff-closed preBoolean set
the Execution of SCM+FSA . (CurInstr (P,(Comput (P,t,Q)))) is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (CurInstr (P,(Comput (P,t,Q))))) . (Comput (P,t,Q)) is set
(Following (P,(Comput (P,t,Q)))) . I is V33() V34() integer ext-real set
Comput (P,t,0) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
(Comput (P,t,0)) . I is V33() V34() integer ext-real set
I is FinSeq-Location
n is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(n) is finite countable Element of Fin FinSeq-Locations
s is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
Exec (n,s) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA) is functional with_common_domain product-like set
K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) is functional non empty set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) -valued Function-like non empty total V18( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) Element of bool [: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):]
[: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):] is set
bool [: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):] is cup-closed diff-closed preBoolean set
the Execution of SCM+FSA . n is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
( the Execution of SCM+FSA . n) . s is set
(Exec (n,s)) . I is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
s . I is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
InsCode n 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 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
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
t is Int-like Element of the carrier of SCM+FSA
P is Int-like Element of the carrier 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
t is Int-like Element of the carrier of SCM+FSA
P is Int-like Element of the carrier 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
t is Int-like Element of the carrier of SCM+FSA
P is Int-like Element of the carrier 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 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 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
SCM-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
K50(6,<*t*>,{}) is set
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
P is Int-like Element of the carrier of SCM+FSA
P =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
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
P is Int-like Element of the carrier of SCM+FSA
P >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+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
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
(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
<*P,Q,t*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set
K50(10,{},<*P,Q,t*>) is set
{Q} is non empty trivial finite 1 -element countable set
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
t is Int-like Element of the carrier of SCM+FSA
P is FinSeq-Location
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
<*t,P*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set
K50(12,{},<*t,P*>) is set
{P} is non empty trivial finite 1 -element countable set
I is FinSeq-Location
n is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
dom n is V51() V52() V53() V54() V55() V56() finite V69() V70() V71() countable Element of bool NAT
(n) is finite countable Element of bool FinSeq-Locations
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
t is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
t . I is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set
Comput (P,t,s) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
(Comput (P,t,s)) . I is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
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
Comput (P,t,Q) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
(Comput (P,t,Q)) . I is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
Q + 1 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
Comput (P,t,(Q + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
(Comput (P,t,(Q + 1))) . I is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
IC (Comput (P,t,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
(Comput (P,t,Q)) . (IC ) is set
n . (IC (Comput (P,t,Q))) is 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
dom P is V51() V52() V53() V54() V55() V56() V69() countable Element of bool NAT
P /. (IC (Comput (P,t,Q))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P . (IC (Comput (P,t,Q))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((P . (IC (Comput (P,t,Q))))) is finite countable Element of Fin FinSeq-Locations
Following (P,(Comput (P,t,Q))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
CurInstr (P,(Comput (P,t,Q))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P,(Comput (P,t,Q)))),(Comput (P,t,Q))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA) is functional with_common_domain product-like set
K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) is functional non empty set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) -valued Function-like non empty total V18( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) Element of bool [: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):]
[: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):] is set
bool [: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):] is cup-closed diff-closed preBoolean set
the Execution of SCM+FSA . (CurInstr (P,(Comput (P,t,Q)))) is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (CurInstr (P,(Comput (P,t,Q))))) . (Comput (P,t,Q)) is set
(Following (P,(Comput (P,t,Q)))) . I is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
Comput (P,t,0) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
(Comput (P,t,0)) . I is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
I is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(I) is finite countable Element of Fin Int-Locations
(I) is finite countable Element of Fin FinSeq-Locations
n is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
n | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
n | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
IC 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
n . (IC ) is set
Exec (I,n) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA) is functional with_common_domain product-like set
K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) is functional non empty set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) -valued Function-like non empty total V18( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) Element of bool [: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):]
[: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):] is set
bool [: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):] is cup-closed diff-closed preBoolean set
the Execution of SCM+FSA . I is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
( the Execution of SCM+FSA . I) . n is set
IC (Exec (I,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
(Exec (I,n)) . (IC ) is set
(Exec (I,n)) | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
(Exec (I,n)) | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
s is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
s | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
s | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
IC 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
s . (IC ) is set
Exec (I,s) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
( the Execution of SCM+FSA . I) . s is set
IC (Exec (I,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
(Exec (I,s)) . (IC ) is set
(Exec (I,s)) | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
(Exec (I,s)) | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
dom (Exec (I,n)) is Element of bool the carrier of SCM+FSA
dom (Exec (I,s)) is Element of bool the carrier 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
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
{p,p} is non empty finite countable Element of bool Int-Locations
n . p is V33() V34() integer ext-real set
(n | (I)) . p is set
s . p is V33() V34() integer ext-real set
succ (IC s) is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable V102() set
(Exec (I,n)) . p is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
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
succ (IC s) is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable V102() set
{p,p} is non empty finite countable Element of bool Int-Locations
n . p is V33() V34() integer ext-real set
(n | (I)) . p is set
s . p is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
n . p is V33() V34() integer ext-real set
(n . p) + (n . p) is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . p is V33() V34() integer ext-real set
(s . p) + (s . p) is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
n . p is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . p is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
n . p is V33() V34() integer ext-real set
(n . p) + (n . p) is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . p is V33() V34() integer ext-real set
(s . p) + (s . p) is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
n . p is V33() V34() integer ext-real set
(n . p) + (n . p) is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . p is V33() V34() integer ext-real set
(s . p) + (s . p) is V33() V34() integer ext-real set
(n | (I)) . p is set
(Exec (I,n)) . p is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
p is Int-like Element of the carrier of SCM+FSA
p is Int-like Element of the carrier 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
succ (IC s) is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable V102() set
{p,p} is non empty finite countable Element of bool Int-Locations
n . p is V33() V34() integer ext-real set
(n | (I)) . p is set
s . p is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
n . p is V33() V34() integer ext-real set
(n . p) - (n . p) is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . p is V33() V34() integer ext-real set
(s . p) - (s . p) is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
n . p is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . p is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
n . p is V33() V34() integer ext-real set
(n . p) - (n . p) is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . p is V33() V34() integer ext-real set
(s . p) - (s . p) is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
n . p is V33() V34() integer ext-real set
(n . p) - (n . p) is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . p is V33() V34() integer ext-real set
(s . p) - (s . p) is V33() V34() integer ext-real set
(n | (I)) . p is set
(Exec (I,n)) . p is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
p is Int-like Element of the carrier of SCM+FSA
p is Int-like Element of the carrier 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
succ (IC s) is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable V102() set
{p,p} is non empty finite countable Element of bool Int-Locations
n . p is V33() V34() integer ext-real set
(n | (I)) . p is set
s . p is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
n . p is V33() V34() integer ext-real set
(n . p) * (n . p) is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . p is V33() V34() integer ext-real set
(s . p) * (s . p) is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
n . p is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . p is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
n . p is V33() V34() integer ext-real set
(n . p) * (n . p) is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . p is V33() V34() integer ext-real set
(s . p) * (s . p) is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
n . p is V33() V34() integer ext-real set
(n . p) * (n . p) is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . p is V33() V34() integer ext-real set
(s . p) * (s . p) is V33() V34() integer ext-real set
(n | (I)) . p is set
(Exec (I,n)) . p is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
p is Int-like Element of the carrier of SCM+FSA
p is Int-like Element of the carrier 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
n . p is V33() V34() integer ext-real set
(n | (I)) . p is set
s . p is V33() V34() integer ext-real set
n . p is V33() V34() integer ext-real set
(n | (I)) . p is set
s . p is V33() V34() integer ext-real set
succ (IC s) is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable V102() set
(Exec (I,n)) . p is V33() V34() integer ext-real set
(n . p) mod (n . p) is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
(s . p) mod (s . p) is V33() V34() integer ext-real set
succ (IC s) is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable V102() set
(Exec (I,n)) . p is V33() V34() integer ext-real set
(n . p) mod (n . p) is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
(s . p) mod (s . p) is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
(n . p) div (n . p) is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
(s . p) div (s . p) is V33() V34() integer ext-real 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
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
SCM-goto p is Element of the InstructionsF of SCM
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set
K50(6,<*p*>,{}) 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 Int-like Element of the carrier of SCM+FSA
p =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
{p} is non empty trivial finite 1 -element countable Element of bool Int-Locations
n . p is V33() V34() integer ext-real set
(n | (I)) . p is set
s . p is V33() V34() integer ext-real set
succ (IC n) is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable V102() set
(Exec (I,n)) . p is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real 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 Int-like Element of the carrier of SCM+FSA
p >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
{p} is non empty trivial finite 1 -element countable Element of bool Int-Locations
n . p is V33() V34() integer ext-real set
(n | (I)) . p is set
s . p is V33() V34() integer ext-real set
succ (IC n) is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable V102() set
(Exec (I,n)) . p is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
p is Int-like Element of the carrier of SCM+FSA
p is Int-like Element of the carrier of SCM+FSA
i is FinSeq-Location
p := (i,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
<*p,i,p*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set
K50(9,{},<*p,i,p*>) is set
{p,p} is non empty finite countable Element of bool Int-Locations
n . p is V33() V34() integer ext-real set
(n | (I)) . p is set
s . p is V33() V34() integer ext-real set
succ (IC s) is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable V102() set
{i} is non empty trivial finite 1 -element countable set
n . i is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(n | (I)) . i is set
abs (n . 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
(Exec (I,n)) . p is V33() V34() integer ext-real set
abs (s . 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
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . i is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
p1 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 . i) /. p1 is V33() V34() integer ext-real V50() Element of INT
f 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 . i) /. f is V33() V34() integer ext-real V50() Element of INT
(Exec (I,n)) . p is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
p1 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 . i) /. p1 is V33() V34() integer ext-real V50() Element of INT
f 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 . i) /. f is V33() V34() integer ext-real V50() Element of INT
(Exec (I,n)) . i is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(Exec (I,s)) . i is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
p is Int-like Element of the carrier of SCM+FSA
p is Int-like Element of the carrier of SCM+FSA
i is FinSeq-Location
(i,p) := 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
<*p,i,p*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set
K50(10,{},<*p,i,p*>) is set
succ (IC s) is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable V102() set
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . p is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . p is V33() V34() integer ext-real set
{p,p} is non empty finite countable Element of bool Int-Locations
n . p is V33() V34() integer ext-real set
(n | (I)) . p is set
n . p is V33() V34() integer ext-real set
(n | (I)) . p is set
{i} is non empty trivial finite 1 -element countable set
n . i is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(n | (I)) . i is set
s . i is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(Exec (I,n)) . p is V33() V34() integer ext-real set
(Exec (I,n)) . p is V33() V34() integer ext-real set
abs (n . 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
(Exec (I,n)) . i is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
abs (s . 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
(Exec (I,s)) . i is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
p1 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 . i) +* (p1,(n . p)) is Relation-like Function-like set
f 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 . i) +* (f,(s . p)) is Relation-like Function-like set
p is Int-like Element of the carrier of SCM+FSA
p is FinSeq-Location
p :=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
<*p,p*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set
K50(11,{},<*p,p*>) is set
succ (IC s) is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable V102() set
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . p is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
len (s . 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 non empty trivial finite 1 -element countable Element of bool Int-Locations
(Exec (I,n)) . p is V33() V34() integer ext-real set
n . p is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
len (n . 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 non empty trivial finite 1 -element countable set
(n | (I)) . p is set
(Exec (I,n)) . p is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(Exec (I,s)) . p is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
p is Int-like Element of the carrier of SCM+FSA
p is FinSeq-Location
p :=<0,...,0> 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
<*p,p*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set
K50(12,{},<*p,p*>) is set
succ (IC s) is non empty epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable V102() set
{p} is non empty trivial finite 1 -element countable Element of bool Int-Locations
n . p is V33() V34() integer ext-real set
(n | (I)) . p is set
{p} is non empty trivial finite 1 -element countable set
abs (n . 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
(Exec (I,n)) . p is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(Exec (I,n)) . p is V33() V34() integer ext-real set
(Exec (I,s)) . p is V33() V34() integer ext-real set
s . p is V33() V34() integer ext-real set
abs (s . 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
(Exec (I,s)) . p is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
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
i |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of i -tuples_on NAT
i -tuples_on NAT is FinSequenceSet of NAT
p1 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
p1 |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of p1 -tuples_on NAT
p1 -tuples_on NAT is FinSequenceSet of NAT
Start-At (0,SCM+FSA) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible non empty finite countable 0 -started set
K456((IC ),0) is finite Cardinal-yielding countable set
{(IC )} is non empty trivial finite 1 -element countable set
K447({(IC )},0) is Relation-like {(IC )} -defined {0} -valued Function-like non empty total V18({(IC )},{0}) finite Cardinal-yielding countable Element of bool [:{(IC )},{0}:]
{0} is non empty trivial V51() V52() V53() V54() V55() V56() finite V62() V67() V68() V69() V70() V71() 1 -element countable set
[:{(IC )},{0}:] is finite countable set
bool [:{(IC )},{0}:] is cup-closed diff-closed preBoolean finite V62() countable set
I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty finite countable V109() set
(I) is finite countable Element of bool Int-Locations
(I) is finite countable Element of bool FinSeq-Locations
dom I is V51() V52() V53() V54() V55() V56() finite V69() V70() V71() countable Element of bool NAT
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 Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
s | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
s | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
t is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
t | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
t | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set
Q is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set
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
Comput (Q,t,m) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
IC (Comput (Q,t,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
(Comput (Q,t,m)) . (IC ) is set
Comput (P,s,m) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
IC (Comput (P,s,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
(Comput (P,s,m)) . (IC ) is set
m + 1 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
Comput (Q,t,(m + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
IC (Comput (Q,t,(m + 1))) 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
(Comput (Q,t,(m + 1))) . (IC ) is set
Comput (P,s,(m + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
IC (Comput (P,s,(m + 1))) 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
(Comput (P,s,(m + 1))) . (IC ) is set
P . (IC (Comput (P,s,m))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom P is V51() V52() V53() V54() V55() V56() V69() countable Element of bool NAT
P /. (IC (Comput (P,s,m))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Following (P,(Comput (P,s,m))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
CurInstr (P,(Comput (P,s,m))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P,(Comput (P,s,m)))),(Comput (P,s,m))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA) is functional with_common_domain product-like set
K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) is functional non empty set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) -valued Function-like non empty total V18( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) Element of bool [: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):]
[: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):] is set
bool [: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):] is cup-closed diff-closed preBoolean set
the Execution of SCM+FSA . (CurInstr (P,(Comput (P,s,m)))) is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (CurInstr (P,(Comput (P,s,m))))) . (Comput (P,s,m)) is set
Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . (P . (IC (Comput (P,s,m)))) is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (P . (IC (Comput (P,s,m))))) . (Comput (P,s,m)) is set
(Comput (P,s,m)) | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
dom ((Comput (P,s,m)) | (I)) is finite countable Element of bool the carrier of SCM+FSA
dom (Comput (P,s,m)) is Element of bool the carrier of SCM+FSA
(dom (Comput (P,s,m))) /\ (I) is finite countable Element of bool FinSeq-Locations
the carrier of SCM+FSA /\ (I) is finite countable Element of bool FinSeq-Locations
dom (Comput (Q,t,m)) is Element of bool the carrier of SCM+FSA
(dom (Comput (Q,t,m))) /\ (I) is finite countable Element of bool FinSeq-Locations
i is set
((Comput (P,s,m)) | (I)) . i is set
p1 is FinSeq-Location
(Comput (P,s,m)) . p1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(Comput (Q,t,m)) . i is set
(Comput (Q,t,m)) | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
I . (IC (Comput (P,s,m))) is set
Q . (IC (Comput (Q,t,m))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Comput (P,s,m)) | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
dom ((Comput (P,s,m)) | (I)) is finite countable Element of bool the carrier of SCM+FSA
(dom (Comput (P,s,m))) /\ (I) is finite countable Element of bool Int-Locations
the carrier of SCM+FSA /\ (I) is finite countable Element of bool Int-Locations
(dom (Comput (Q,t,m))) /\ (I) is finite countable Element of bool Int-Locations
i is set
((Comput (P,s,m)) | (I)) . i is set
p1 is Int-like Element of the carrier of SCM+FSA
(Comput (P,s,m)) . p1 is V33() V34() integer ext-real set
(Comput (Q,t,m)) . i is set
(Comput (Q,t,m)) | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
dom Q is V51() V52() V53() V54() V55() V56() V69() countable Element of bool NAT
Q /. (IC (Comput (Q,t,m))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Following (Q,(Comput (Q,t,m))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
CurInstr (Q,(Comput (Q,t,m))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (Q,(Comput (Q,t,m)))),(Comput (Q,t,m))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . (CurInstr (Q,(Comput (Q,t,m)))) is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (CurInstr (Q,(Comput (Q,t,m))))) . (Comput (Q,t,m)) is set
Exec ((Q . (IC (Comput (Q,t,m)))),(Comput (Q,t,m))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . (Q . (IC (Comput (Q,t,m)))) is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (Q . (IC (Comput (Q,t,m))))) . (Comput (Q,t,m)) 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
((P . (IC (Comput (P,s,m))))) is finite countable Element of Fin FinSeq-Locations
(Comput (P,s,m)) | ((P . (IC (Comput (P,s,m))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
((Comput (P,s,m)) | (I)) | ((P . (IC (Comput (P,s,m))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
(Comput (Q,t,m)) | ((P . (IC (Comput (P,s,m))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
((P . (IC (Comput (P,s,m))))) is finite countable Element of Fin Int-Locations
(Comput (P,s,m)) | ((P . (IC (Comput (P,s,m))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
((Comput (P,s,m)) | (I)) | ((P . (IC (Comput (P,s,m))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
(Comput (Q,t,m)) | ((P . (IC (Comput (P,s,m))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
(Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) | ((P . (IC (Comput (P,s,m))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
Exec ((P . (IC (Comput (P,s,m)))),(Comput (Q,t,m))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
( the Execution of SCM+FSA . (P . (IC (Comput (P,s,m))))) . (Comput (Q,t,m)) is set
(Exec ((P . (IC (Comput (P,s,m)))),(Comput (Q,t,m)))) | ((P . (IC (Comput (P,s,m))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
IC (Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,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
(Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) . (IC ) is set
IC (Exec ((P . (IC (Comput (P,s,m)))),(Comput (Q,t,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
(Exec ((P . (IC (Comput (P,s,m)))),(Comput (Q,t,m)))) . (IC ) is set
(Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) | ((P . (IC (Comput (P,s,m))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
(Exec ((P . (IC (Comput (P,s,m)))),(Comput (Q,t,m)))) | ((P . (IC (Comput (P,s,m))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
i is Int-like Element of the carrier of SCM+FSA
(Comput (P,s,(m + 1))) . i is V33() V34() integer ext-real set
((Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) | ((P . (IC (Comput (P,s,m)))))) . i is set
(Comput (Q,t,(m + 1))) . i is V33() V34() integer ext-real set
(Comput (P,s,(m + 1))) . i is V33() V34() integer ext-real set
(Comput (P,s,m)) . i is V33() V34() integer ext-real set
(Comput (Q,t,m)) . i is V33() V34() integer ext-real set
(Comput (Q,t,(m + 1))) . i is V33() V34() integer ext-real set
i is FinSeq-Location
(Comput (P,s,(m + 1))) . i is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(Comput (Q,t,(m + 1))) . i is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
((Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) | ((P . (IC (Comput (P,s,m)))))) . i is set
(Comput (P,s,m)) . i is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(Comput (Q,t,m)) . i is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
Comput (Q,t,0) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
IC (Comput (Q,t,0)) 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
(Comput (Q,t,0)) . (IC ) is set
Comput (P,s,0) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
IC (Comput (P,s,0)) 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
(Comput (P,s,0)) . (IC ) is set
IC 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
t . (IC ) is set
IC 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
s . (IC ) is set
m is Int-like Element of the carrier of SCM+FSA
(Comput (P,s,0)) . m is V33() V34() integer ext-real set
s . m is V33() V34() integer ext-real set
(s | (I)) . m is set
t . m is V33() V34() integer ext-real set
(Comput (Q,t,0)) . m is V33() V34() integer ext-real set
m is FinSeq-Location
(Comput (P,s,0)) . m is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(Comput (Q,t,0)) . m is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
s . m is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(s | (I)) . m is set
t . m is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
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
Comput (Q,t,m) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
IC (Comput (Q,t,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
(Comput (Q,t,m)) . (IC ) is set
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
Comput (P,s,m) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
IC (Comput (P,s,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
(Comput (P,s,m)) . (IC ) is set
Comput (Q,t,m) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
IC (Comput (Q,t,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
(Comput (Q,t,m)) . (IC ) is set
IC 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
t . (IC ) is set
IC 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
s . (IC ) is set
p is Int-like Element of the carrier of SCM+FSA
(Comput (P,s,m)) . p is V33() V34() integer ext-real set
s . p is V33() V34() integer ext-real set
(s | (I)) . p is set
t . p is V33() V34() integer ext-real set
(Comput (Q,t,m)) . p is V33() V34() integer ext-real set
p is FinSeq-Location
(Comput (P,s,m)) . p is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(Comput (Q,t,m)) . p is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
s . p is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(s | (I)) . p is set
t . p is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
p is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real finite cardinal countable set
p + 1 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 finite cardinal countable set
p + 1 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
Comput (P,s,p) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
IC (Comput (P,s,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
(Comput (P,s,p)) . (IC ) is set
(Comput (P,s,p)) | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
dom ((Comput (P,s,p)) | (I)) is finite countable Element of bool the carrier of SCM+FSA
dom (Comput (P,s,p)) is Element of bool the carrier of SCM+FSA
(dom (Comput (P,s,p))) /\ (I) is finite countable Element of bool FinSeq-Locations
the carrier of SCM+FSA /\ (I) is finite countable Element of bool FinSeq-Locations
Comput (Q,t,p) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
dom (Comput (Q,t,p)) is Element of bool the carrier of SCM+FSA
(dom (Comput (Q,t,p))) /\ (I) is finite countable Element of bool FinSeq-Locations
i is set
((Comput (P,s,p)) | (I)) . i is set
p1 is FinSeq-Location
(Comput (P,s,p)) . p1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(Comput (Q,t,p)) . i is set
(Comput (Q,t,p)) | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
P . (IC (Comput (P,s,p))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
p + 1 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
dom P is V51() V52() V53() V54() V55() V56() V69() countable Element of bool NAT
P /. (IC (Comput (P,s,p))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (P,s,(p + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
Following (P,(Comput (P,s,p))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
CurInstr (P,(Comput (P,s,p))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P,(Comput (P,s,p)))),(Comput (P,s,p))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA) is functional with_common_domain product-like set
K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) is functional non empty set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) -valued Function-like non empty total V18( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) Element of bool [: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):]
[: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):] is set
bool [: the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))):] is cup-closed diff-closed preBoolean set
the Execution of SCM+FSA . (CurInstr (P,(Comput (P,s,p)))) is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (CurInstr (P,(Comput (P,s,p))))) . (Comput (P,s,p)) is set
Exec ((P . (IC (Comput (P,s,p)))),(Comput (P,s,p))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . (P . (IC (Comput (P,s,p)))) is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (P . (IC (Comput (P,s,p))))) . (Comput (P,s,p)) is set
(Comput (P,s,p)) | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
dom ((Comput (P,s,p)) | (I)) is finite countable Element of bool the carrier of SCM+FSA
(dom (Comput (P,s,p))) /\ (I) is finite countable Element of bool Int-Locations
the carrier of SCM+FSA /\ (I) is finite countable Element of bool Int-Locations
(dom (Comput (Q,t,p))) /\ (I) is finite countable Element of bool Int-Locations
f is set
((Comput (P,s,p)) | (I)) . f is set
x9 is Int-like Element of the carrier of SCM+FSA
(Comput (P,s,p)) . x9 is V33() V34() integer ext-real set
(Comput (Q,t,p)) . f is set
(Comput (Q,t,p)) | (I) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
IC (Comput (Q,t,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
(Comput (Q,t,p)) . (IC ) is set
I . (IC (Comput (P,s,p))) is set
dom Q is V51() V52() V53() V54() V55() V56() V69() countable Element of bool NAT
Q /. (IC (Comput (Q,t,p))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Q . (IC (Comput (Q,t,p))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (Q,t,(p + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
Following (Q,(Comput (Q,t,p))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
CurInstr (Q,(Comput (Q,t,p))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (Q,(Comput (Q,t,p)))),(Comput (Q,t,p))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . (CurInstr (Q,(Comput (Q,t,p)))) is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (CurInstr (Q,(Comput (Q,t,p))))) . (Comput (Q,t,p)) is set
Exec ((Q . (IC (Comput (Q,t,p)))),(Comput (Q,t,p))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . (Q . (IC (Comput (Q,t,p)))) is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (Q . (IC (Comput (Q,t,p))))) . (Comput (Q,t,p)) 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
((P . (IC (Comput (P,s,p))))) is finite countable Element of Fin FinSeq-Locations
(Comput (P,s,p)) | ((P . (IC (Comput (P,s,p))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
((Comput (P,s,p)) | (I)) | ((P . (IC (Comput (P,s,p))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
(Comput (Q,t,p)) | ((P . (IC (Comput (P,s,p))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
((P . (IC (Comput (P,s,p))))) is finite countable Element of Fin Int-Locations
(Comput (P,s,p)) | ((P . (IC (Comput (P,s,p))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
((Comput (P,s,p)) | (I)) | ((P . (IC (Comput (P,s,p))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
(Comput (Q,t,p)) | ((P . (IC (Comput (P,s,p))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
(Exec ((P . (IC (Comput (P,s,p)))),(Comput (P,s,p)))) | ((P . (IC (Comput (P,s,p))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
Exec ((P . (IC (Comput (P,s,p)))),(Comput (Q,t,p))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible total set
( the Execution of SCM+FSA . (P . (IC (Comput (P,s,p))))) . (Comput (Q,t,p)) is set
(Exec ((P . (IC (Comput (P,s,p)))),(Comput (Q,t,p)))) | ((P . (IC (Comput (P,s,p))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
f is Int-like Element of the carrier of SCM+FSA
(Comput (P,s,m)) . f is V33() V34() integer ext-real set
((Exec ((P . (IC (Comput (P,s,p)))),(Comput (P,s,p)))) | ((P . (IC (Comput (P,s,p)))))) . f is set
(Comput (Q,t,m)) . f is V33() V34() integer ext-real set
(Comput (P,s,m)) . f is V33() V34() integer ext-real set
(Comput (P,s,p)) . f is V33() V34() integer ext-real set
(Comput (Q,t,p)) . f is V33() V34() integer ext-real set
(Comput (Q,t,m)) . f is V33() V34() integer ext-real set
(Exec ((P . (IC (Comput (P,s,p)))),(Comput (P,s,p)))) | ((P . (IC (Comput (P,s,p))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
(Exec ((P . (IC (Comput (P,s,p)))),(Comput (Q,t,p)))) | ((P . (IC (Comput (P,s,p))))) is Relation-like the carrier of SCM+FSA -defined Function-like K423(3,SCM+FSA) -compatible finite countable set
f is FinSeq-Location
(Comput (P,s,m)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
((Exec ((P . (IC (Comput (P,s,p)))),(Comput (P,s,p)))) | ((P . (IC (Comput (P,s,p)))))) . f is set
(Comput (Q,t,m)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(Comput (P,s,m)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(Comput (P,s,p)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(Comput (Q,t,p)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT
(Comput (Q,t,m)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of INT