:: SCMFSA_2 semantic presentation

REAL is set

SCM-Data-Loc is non empty set

K86(NAT,1) is finite countable V63() Element of bool NAT

INT is set
K276(NAT,INT) is set

SCM-Halt is Element of Segm 9

{} is set
is V13() V14() set
is non natural V13() set

is non natural V13() set

{ [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT : b1 = 6 } is set
\/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT : b1 = 6 } is set

K87(NAT,7,8) is finite countable V63() Element of bool NAT
{ [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT , b3 is Element of SCM-Data-Loc : b1 in K87(NAT,7,8) } is set
( \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT , b3 is Element of SCM-Data-Loc : b1 in K87(NAT,7,8) } is set

K90(NAT,1,2,3,4,5) is finite countable V63() Element of bool NAT
{ [b1,{},K149(SCM-Data-Loc,b2,b3)] where b1 is Element of Segm 9, b2, b3 is Element of SCM-Data-Loc : b1 in K90(NAT,1,2,3,4,5) } is set
(( \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT , b3 is Element of SCM-Data-Loc : b1 in K87(NAT,7,8) } ) \/ { [b1,{},K149(SCM-Data-Loc,b2,b3)] where b1 is Element of Segm 9, b2, b3 is Element of SCM-Data-Loc : b1 in K90(NAT,1,2,3,4,5) } is set
K165((),()) is set
[:SCM-Instr,K165((),()):] is Relation-like set
bool [:SCM-Instr,K165((),()):] is set

In (NAT,SCM-Memory) is Element of SCM-Memory
SCM-Exec is Relation-like SCM-Instr -defined K165((),()) -valued Function-like V38( SCM-Instr ,K165((),())) Element of bool [:SCM-Instr,K165((),()):]
AMI-Struct(# SCM-Memory,(),SCM-Instr,SCM-OK,SCM-VAL,SCM-Exec #) is strict AMI-Struct over 2
the InstructionsF of SCM is Relation-like non empty standard-ins V72() V73() V75() set
the carrier of SCM is non empty set

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

SCM+FSA-Data*-Loc is non empty set

SCM+FSA-Memory is non empty set

K277(NAT,INT,()) is set

{9,10} is finite countable V63() set
{ [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set
SCM-Instr \/ { [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set

{11,12} is finite countable V63() set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 13, b2 is Element of SCM-Data-Loc , b3 is Element of SCM+FSA-Data*-Loc : b1 in {11,12} } is set
(SCM-Instr \/ { [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 13, b2 is Element of SCM-Data-Loc , b3 is Element of SCM+FSA-Data*-Loc : b1 in {11,12} } is set
K165((),()) is set

bool is set

RAT is set

IC is V49( SCM ) Element of the carrier of SCM
the ZeroF of SCM is Element of the carrier of SCM
halt SCM is halting Element of the InstructionsF of SCM
halt the InstructionsF of SCM is V74( the InstructionsF of SCM) Element of the InstructionsF of SCM
[0,{},{}] is V13() V14() set
is non natural V13() set

is non natural V13() set
SCM-Data-Loc is non empty Element of bool SCM-Memory

is non natural V13() set

() \ is Element of bool ()
bool () is set

() is strict AMI-Struct over 3
the carrier of () is set

the Object-Kind of () is Relation-like the carrier of () -defined 3 -valued Function-like V38( the carrier of (),3) Element of bool [: the carrier of (),3:]
[: the carrier of (),3:] is Relation-like set
bool [: the carrier of (),3:] is set

the Object-Kind of () * the ValuesF of () is Relation-like the carrier of () -defined Function-like set

[6,,{}] is V13() V14() set
[6,] is non natural V13() set

{{6,},{6}} is finite V30() countable set
[[6,],{}] is non natural V13() set

the InstructionsF of () is Relation-like non empty standard-ins V72() V73() V75() set
IC is V49(()) Element of the carrier of ()
the carrier of () is non empty set
the ZeroF of () is Element of the carrier of ()
bool the carrier of () is set
() is Element of bool the carrier of ()

fa is Element of the carrier of ()

a is Element of the carrier of ()

dl. fa is Int-like Element of the carrier of SCM
[1,fa] is non natural V13() set
{1,fa} is finite countable set

{{1,fa},{1}} is finite V30() countable set
() is non empty Element of bool the carrier of ()

- (fa + 1) is V24() V25() integer ext-real non positive set
- 0 is V24() V25() integer ext-real non positive set

- (a + 1) is V24() V25() integer ext-real non positive set

(fa) is ()

- (fa + 1) is V24() V25() integer ext-real non positive set
(a) is ()

- (a + 1) is V24() V25() integer ext-real non positive set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of SCM

dl. c is Int-like Element of the carrier of SCM
[1,c] is non natural V13() set
{1,c} is finite countable set
{{1,c},{1}} is finite V30() countable set
(c) is Int-like Element of the carrier of ()
fa is ()

- a is V24() V25() integer ext-real non positive set

(s) is ()

- (s + 1) is V24() V25() integer ext-real non positive set
[:NAT, the carrier of ():] is Relation-like set
bool [:NAT, the carrier of ():] is set
fa is Relation-like NAT -defined the carrier of () -valued Function-like V38( NAT , the carrier of ()) Element of bool [:NAT, the carrier of ():]
proj1 fa is set
proj2 fa is set
a is set
c is set
fa . a is set
fa . c is set

(s) is ()

- (s + 1) is V24() V25() integer ext-real non positive set
fa . s is Element of the carrier of ()

(a3) is ()

- (a3 + 1) is V24() V25() integer ext-real non positive set

rng fa is Element of bool the carrier of ()
a is set
c is set
fa . c is set

(s) is ()

- (s + 1) is V24() V25() integer ext-real non positive set
a is set

(c) is ()

- (c + 1) is V24() V25() integer ext-real non positive set
fa . c is Element of the carrier of ()
fa is Int-like Element of the carrier of ()
fa is Int-like Element of the carrier of ()
Values fa is non empty set

the Object-Kind of () is Relation-like the carrier of () -defined 3 -valued Function-like V38( the carrier of (),3) Element of bool [: the carrier of (),3:]
[: the carrier of (),3:] is Relation-like set
bool [: the carrier of (),3:] is set

the Object-Kind of () * the ValuesF of () is Relation-like the carrier of () -defined Function-like set
() . fa is set
fa is ()
Values fa is non empty set

the Object-Kind of () is Relation-like the carrier of () -defined 3 -valued Function-like V38( the carrier of (),3) Element of bool [: the carrier of (),3:]
[: the carrier of (),3:] is Relation-like set
bool [: the carrier of (),3:] is set

the Object-Kind of () * the ValuesF of () is Relation-like the carrier of () -defined Function-like set
() . fa is set
the InstructionsF of () is Relation-like non empty standard-ins V72() V73() V75() set
fa is Element of the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 13, b2 is Element of SCM+FSA-Data-Loc , b3 is Element of SCM+FSA-Data*-Loc : b1 in {11,12} } is set
a is Element of Segm 13

<*c,s*> is set
[a,{},<*c,s*>] is V13() V14() set
[a,{}] is non natural V13() set

{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,s*>] is non natural V13() set
{[a,{}],<*c,s*>} is finite countable set

{{[a,{}],<*c,s*>},{[a,{}]}} is finite V30() countable set

{ [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM+FSA-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set
SCM-Instr \/ { [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM+FSA-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set
a is Element of Segm 13

a3 is Element of SCM+FSA-Data*-Loc

<*c,a3,s*> is set
[a,{},<*c,a3,s*>] is V13() V14() set
[a,{}] is non natural V13() set

{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,a3,s*>] is non natural V13() set
{[a,{}],<*c,a3,s*>} is finite countable set

{{[a,{}],<*c,a3,s*>},{[a,{}]}} is finite V30() countable set
fa is Element of the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
{ [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM+FSA-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set
SCM-Instr \/ { [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM+FSA-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 13, b2 is Element of SCM+FSA-Data-Loc , b3 is Element of SCM+FSA-Data*-Loc : b1 in {11,12} } is set
a is Element of the InstructionsF of SCM

InsCodes the InstructionsF of SCM is non empty set
K39( the InstructionsF of SCM) is set
proj1 the InstructionsF of SCM is non empty set
proj1 () is set
K29(a) is set
K29(K29(a)) is set
a is Element of Segm 13

a3 is Element of SCM+FSA-Data*-Loc

<*c,a3,s*> is set
[a,{},<*c,a3,s*>] is V13() V14() set
[a,{}] is non natural V13() set

{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,a3,s*>] is non natural V13() set
{[a,{}],<*c,a3,s*>} is finite countable set

{{[a,{}],<*c,a3,s*>},{[a,{}]}} is finite V30() countable set

a is Element of Segm 13

<*c,s*> is set
[a,{},<*c,s*>] is V13() V14() set
[a,{}] is non natural V13() set

{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,s*>] is non natural V13() set
{[a,{}],<*c,s*>} is finite countable set

{{[a,{}],<*c,s*>},{[a,{}]}} is finite V30() countable set

fa is Element of the InstructionsF of SCM
{ [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM+FSA-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set
SCM-Instr \/ { [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM+FSA-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
c := s is Element of the InstructionsF of SCM
<*c,s*> is set
[1,{},<*c,s*>] is V13() V14() set
[1,{}] is non natural V13() set

{{1,{}},{1}} is finite V30() countable set
[[1,{}],<*c,s*>] is non natural V13() set
{[1,{}],<*c,s*>} is finite countable set

{{[1,{}],<*c,s*>},{[1,{}]}} is finite V30() countable set
a3 is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
t is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
a3 := t is Element of the InstructionsF of SCM
<*a3,t*> is set
[1,{},<*a3,t*>] is V13() V14() set
[1,{}] is non natural V13() set

{{1,{}},{1}} is finite V30() countable set
[[1,{}],<*a3,t*>] is non natural V13() set
{[1,{}],<*a3,t*>} is finite countable set

{{[1,{}],<*a3,t*>},{[1,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
w is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
t := w is Element of the InstructionsF of SCM
<*t,w*> is set
[1,{},<*t,w*>] is V13() V14() set
[[1,{}],<*t,w*>] is non natural V13() set
{[1,{}],<*t,w*>} is finite countable set
{{[1,{}],<*t,w*>},{[1,{}]}} is finite V30() countable set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
AddTo (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[2,{},<*c,s*>] is V13() V14() set
[2,{}] is non natural V13() set

{{2,{}},{2}} is finite V30() countable set
[[2,{}],<*c,s*>] is non natural V13() set
{[2,{}],<*c,s*>} is finite countable set

{{[2,{}],<*c,s*>},{[2,{}]}} is finite V30() countable set
a3 is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
t is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
AddTo (a3,t) is Element of the InstructionsF of SCM
<*a3,t*> is set
[2,{},<*a3,t*>] is V13() V14() set
[2,{}] is non natural V13() set

{{2,{}},{2}} is finite V30() countable set
[[2,{}],<*a3,t*>] is non natural V13() set
{[2,{}],<*a3,t*>} is finite countable set

{{[2,{}],<*a3,t*>},{[2,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
w is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
AddTo (t,w) is Element of the InstructionsF of SCM
<*t,w*> is set
[2,{},<*t,w*>] is V13() V14() set
[[2,{}],<*t,w*>] is non natural V13() set
{[2,{}],<*t,w*>} is finite countable set
{{[2,{}],<*t,w*>},{[2,{}]}} is finite V30() countable set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
SubFrom (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[3,{},<*c,s*>] is V13() V14() set
[3,{}] is non natural V13() set

{{3,{}},{3}} is finite V30() countable set
[[3,{}],<*c,s*>] is non natural V13() set
{[3,{}],<*c,s*>} is finite countable set

{{[3,{}],<*c,s*>},{[3,{}]}} is finite V30() countable set
a3 is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
t is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
SubFrom (a3,t) is Element of the InstructionsF of SCM
<*a3,t*> is set
[3,{},<*a3,t*>] is V13() V14() set
[3,{}] is non natural V13() set

{{3,{}},{3}} is finite V30() countable set
[[3,{}],<*a3,t*>] is non natural V13() set
{[3,{}],<*a3,t*>} is finite countable set

{{[3,{}],<*a3,t*>},{[3,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
w is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
SubFrom (t,w) is Element of the InstructionsF of SCM
<*t,w*> is set
[3,{},<*t,w*>] is V13() V14() set
[[3,{}],<*t,w*>] is non natural V13() set
{[3,{}],<*t,w*>} is finite countable set
{{[3,{}],<*t,w*>},{[3,{}]}} is finite V30() countable set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
MultBy (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[4,{},<*c,s*>] is V13() V14() set
[4,{}] is non natural V13() set

{{4,{}},{4}} is finite V30() countable set
[[4,{}],<*c,s*>] is non natural V13() set
{[4,{}],<*c,s*>} is finite countable set

{{[4,{}],<*c,s*>},{[4,{}]}} is finite V30() countable set
a3 is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
t is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
MultBy (a3,t) is Element of the InstructionsF of SCM
<*a3,t*> is set
[4,{},<*a3,t*>] is V13() V14() set
[4,{}] is non natural V13() set

{{4,{}},{4}} is finite V30() countable set
[[4,{}],<*a3,t*>] is non natural V13() set
{[4,{}],<*a3,t*>} is finite countable set

{{[4,{}],<*a3,t*>},{[4,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
w is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
MultBy (t,w) is Element of the InstructionsF of SCM
<*t,w*> is set
[4,{},<*t,w*>] is V13() V14() set
[[4,{}],<*t,w*>] is non natural V13() set
{[4,{}],<*t,w*>} is finite countable set
{{[4,{}],<*t,w*>},{[4,{}]}} is finite V30() countable set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
Divide (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[5,{},<*c,s*>] is V13() V14() set
[5,{}] is non natural V13() set

{{5,{}},{5}} is finite V30() countable set
[[5,{}],<*c,s*>] is non natural V13() set
{[5,{}],<*c,s*>} is finite countable set

{{[5,{}],<*c,s*>},{[5,{}]}} is finite V30() countable set
a3 is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
t is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
Divide (a3,t) is Element of the InstructionsF of SCM
<*a3,t*> is set
[5,{},<*a3,t*>] is V13() V14() set
[5,{}] is non natural V13() set

{{5,{}},{5}} is finite V30() countable set
[[5,{}],<*a3,t*>] is non natural V13() set
{[5,{}],<*a3,t*>} is finite countable set

{{[5,{}],<*a3,t*>},{[5,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
w is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
Divide (t,w) is Element of the InstructionsF of SCM
<*t,w*> is set
[5,{},<*t,w*>] is V13() V14() set
[[5,{}],<*t,w*>] is non natural V13() set
{[5,{}],<*t,w*>} is finite countable set
{{[5,{}],<*t,w*>},{[5,{}]}} is finite V30() countable set

SCM-goto fa is Element of the InstructionsF of SCM

[6,<*fa*>,{}] is V13() V14() set
[6,<*fa*>] is non natural V13() set
{6,<*fa*>} is finite countable set

{{6,<*fa*>},{6}} is finite V30() countable set
[[6,<*fa*>],{}] is non natural V13() set
{[6,<*fa*>],{}} is finite countable set

{{[6,<*fa*>],{}},{[6,<*fa*>]}} is finite V30() countable set
a is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of SCM
c =0_goto fa is Element of the InstructionsF of SCM

[7,<*fa*>,<*c*>] is V13() V14() set
[7,<*fa*>] is non natural V13() set
{7,<*fa*>} is finite countable set

{{7,<*fa*>},{7}} is finite V30() countable set
[[7,<*fa*>],<*c*>] is non natural V13() set
{[7,<*fa*>],<*c*>} is finite countable set

{{[7,<*fa*>],<*c*>},{[7,<*fa*>]}} is finite V30() countable set
s is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
a3 =0_goto fa is Element of the InstructionsF of SCM

[7,<*fa*>,<*a3*>] is V13() V14() set
[7,<*fa*>] is non natural V13() set
{7,<*fa*>} is finite countable set

{{7,<*fa*>},{7}} is finite V30() countable set
[[7,<*fa*>],<*a3*>] is non natural V13() set
{[7,<*fa*>],<*a3*>} is finite countable set

{{[7,<*fa*>],<*a3*>},{[7,<*fa*>]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
t =0_goto fa is Element of the InstructionsF of SCM

[7,<*fa*>,<*t*>] is V13() V14() set
[[7,<*fa*>],<*t*>] is non natural V13() set
{[7,<*fa*>],<*t*>} is finite countable set
{{[7,<*fa*>],<*t*>},{[7,<*fa*>]}} is finite V30() countable set
c is Int-like Element of the carrier of SCM
c >0_goto fa is Element of the InstructionsF of SCM

[8,<*fa*>,<*c*>] is V13() V14() set
[8,<*fa*>] is non natural V13() set
{8,<*fa*>} is finite countable set

{{8,<*fa*>},{8}} is finite V30() countable set
[[8,<*fa*>],<*c*>] is non natural V13() set
{[8,<*fa*>],<*c*>} is finite countable set

{{[8,<*fa*>],<*c*>},{[8,<*fa*>]}} is finite V30() countable set
s is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
a3 >0_goto fa is Element of the InstructionsF of SCM

[8,<*fa*>,<*a3*>] is V13() V14() set
[8,<*fa*>] is non natural V13() set
{8,<*fa*>} is finite countable set

{{8,<*fa*>},{8}} is finite V30() countable set
[[8,<*fa*>],<*a3*>] is non natural V13() set
{[8,<*fa*>],<*a3*>} is finite countable set

{{[8,<*fa*>],<*a3*>},{[8,<*fa*>]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
t >0_goto fa is Element of the InstructionsF of SCM

[8,<*fa*>,<*t*>] is V13() V14() set
[[8,<*fa*>],<*t*>] is non natural V13() set
{[8,<*fa*>],<*t*>} is finite countable set
{{[8,<*fa*>],<*t*>},{[8,<*fa*>]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
c is ()
a is Int-like Element of the carrier of ()
<*fa,c,a*> is set
[9,{},<*fa,c,a*>] is V13() V14() set
[9,{}] is non natural V13() set

{{9,{}},{9}} is finite V30() countable set
[[9,{}],<*fa,c,a*>] is non natural V13() set
{[9,{}],<*fa,c,a*>} is finite countable set

{{[9,{}],<*fa,c,a*>},{[9,{}]}} is finite V30() countable set
a3 is Element of SCM-Data-Loc

t is Element of SCM-Data-Loc
<*a3,s,t*> is set
[9,{},<*a3,s,t*>] is V13() V14() set
[[9,{}],<*a3,s,t*>] is non natural V13() set
{[9,{}],<*a3,s,t*>} is finite countable set
{{[9,{}],<*a3,s,t*>},{[9,{}]}} is finite V30() countable set
[10,{},<*fa,c,a*>] is V13() V14() set
[10,{}] is non natural V13() set

{10} is finite countable V63() set
{{10,{}},{10}} is finite V30() countable set
[[10,{}],<*fa,c,a*>] is non natural V13() set
{[10,{}],<*fa,c,a*>} is finite countable set

{{[10,{}],<*fa,c,a*>},{[10,{}]}} is finite V30() countable set
a3 is Element of SCM-Data-Loc

t is Element of SCM-Data-Loc
<*a3,s,t*> is set
[10,{},<*a3,s,t*>] is V13() V14() set
[[10,{}],<*a3,s,t*>] is non natural V13() set
{[10,{}],<*a3,s,t*>} is finite countable set
{{[10,{}],<*a3,s,t*>},{[10,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is ()
<*fa,a*> is set
[11,{},<*fa,a*>] is V13() V14() set
[11,{}] is non natural V13() set

{11} is finite countable V63() set
{{11,{}},{11}} is finite V30() countable set
[[11,{}],<*fa,a*>] is non natural V13() set
{[11,{}],<*fa,a*>} is finite countable set

{{[11,{}],<*fa,a*>},{[11,{}]}} is finite V30() countable set
s is Element of SCM-Data-Loc

<*s,c*> is set
[11,{},<*s,c*>] is V13() V14() set
[[11,{}],<*s,c*>] is non natural V13() set
{[11,{}],<*s,c*>} is finite countable set
{{[11,{}],<*s,c*>},{[11,{}]}} is finite V30() countable set
[12,{},<*fa,a*>] is V13() V14() set
[12,{}] is non natural V13() set

{12} is finite countable V63() set
{{12,{}},{12}} is finite V30() countable set
[[12,{}],<*fa,a*>] is non natural V13() set
{[12,{}],<*fa,a*>} is finite countable set

{{[12,{}],<*fa,a*>},{[12,{}]}} is finite V30() countable set
s is Element of SCM-Data-Loc

<*s,c*> is set
[12,{},<*s,c*>] is V13() V14() set
[[12,{}],<*s,c*>] is non natural V13() set
{[12,{}],<*s,c*>} is finite countable set
{{[12,{}],<*s,c*>},{[12,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
c := s is Element of the InstructionsF of SCM
<*c,s*> is set
[1,{},<*c,s*>] is V13() V14() set
[1,{}] is non natural V13() set

{{1,{}},{1}} is finite V30() countable set
[[1,{}],<*c,s*>] is non natural V13() set
{[1,{}],<*c,s*>} is finite countable set

{{[1,{}],<*c,s*>},{[1,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
AddTo (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[2,{},<*c,s*>] is V13() V14() set
[2,{}] is non natural V13() set

{{2,{}},{2}} is finite V30() countable set
[[2,{}],<*c,s*>] is non natural V13() set
{[2,{}],<*c,s*>} is finite countable set

{{[2,{}],<*c,s*>},{[2,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
SubFrom (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[3,{},<*c,s*>] is V13() V14() set
[3,{}] is non natural V13() set

{{3,{}},{3}} is finite V30() countable set
[[3,{}],<*c,s*>] is non natural V13() set
{[3,{}],<*c,s*>} is finite countable set

{{[3,{}],<*c,s*>},{[3,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
MultBy (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[4,{},<*c,s*>] is V13() V14() set
[4,{}] is non natural V13() set

{{4,{}},{4}} is finite V30() countable set
[[4,{}],<*c,s*>] is non natural V13() set
{[4,{}],<*c,s*>} is finite countable set

{{[4,{}],<*c,s*>},{[4,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
Divide (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[5,{},<*c,s*>] is V13() V14() set
[5,{}] is non natural V13() set

{{5,{}},{5}} is finite V30() countable set
[[5,{}],<*c,s*>] is non natural V13() set
{[5,{}],<*c,s*>} is finite countable set

{{[5,{}],<*c,s*>},{[5,{}]}} is finite V30() countable set

(fa) is Element of the InstructionsF of ()
SCM-goto fa is Element of the InstructionsF of SCM

[6,<*fa*>,{}] is V13() V14() set
[6,<*fa*>] is non natural V13() set
{6,<*fa*>} is finite countable set
{{6,<*fa*>},{6}} is finite V30() countable set
[[6,<*fa*>],{}] is non natural V13() set

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa)) is set
K29(K29((fa))) is set

a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
c =0_goto fa is Element of the InstructionsF of SCM

[7,<*fa*>,<*c*>] is V13() V14() set
[7,<*fa*>] is non natural V13() set
{7,<*fa*>} is finite countable set

{{7,<*fa*>},{7}} is finite V30() countable set
[[7,<*fa*>],<*c*>] is non natural V13() set
{[7,<*fa*>],<*c*>} is finite countable set

{{[7,<*fa*>],<*c*>},{[7,<*fa*>]}} is finite V30() countable set

a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
c >0_goto fa is Element of the InstructionsF of SCM

[8,<*fa*>,<*c*>] is V13() V14() set
[8,<*fa*>] is non natural V13() set
{8,<*fa*>} is finite countable set

{{8,<*fa*>},{8}} is finite V30() countable set
[[8,<*fa*>],<*c*>] is non natural V13() set
{[8,<*fa*>],<*c*>} is finite countable set

{{[8,<*fa*>],<*c*>},{[8,<*fa*>]}} is finite V30() countable set
a is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of ()
fa is ()
(a,c,fa) is Element of the InstructionsF of ()
<*a,fa,c*> is set
[9,{},<*a,fa,c*>] is V13() V14() set
[[9,{}],<*a,fa,c*>] is non natural V13() set
{[9,{}],<*a,fa,c*>} is finite countable set
{{[9,{}],<*a,fa,c*>},{[9,{}]}} is finite V30() countable set

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((a,c,fa)) is set
K29(K29((a,c,fa))) is set
c is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
fa is ()
(c,a,fa) is Element of the InstructionsF of ()
<*c,fa,a*> is set
[10,{},<*c,fa,a*>] is V13() V14() set
[[10,{}],<*c,fa,a*>] is non natural V13() set
{[10,{}],<*c,fa,a*>} is finite countable set
{{[10,{}],<*c,fa,a*>},{[10,{}]}} is finite V30() countable set

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((c,a,fa)) is set
K29(K29((c,a,fa))) is set
a is Int-like Element of the carrier of ()
fa is ()
(a,fa) is Element of the InstructionsF of ()
<*a,fa*> is set
[11,{},<*a,fa*>] is V13() V14() set
[[11,{}],<*a,fa*>] is non natural V13() set
{[11,{}],<*a,fa*>} is finite countable set
{{[11,{}],<*a,fa*>},{[11,{}]}} is finite V30() countable set

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((a,fa)) is set
K29(K29((a,fa))) is set
a is Int-like Element of the carrier of ()
fa is ()
(a,fa) is Element of the InstructionsF of ()
<*a,fa*> is set
[12,{},<*a,fa*>] is V13() V14() set
[[12,{}],<*a,fa*>] is non natural V13() set
{[12,{}],<*a,fa*>} is finite countable set
{{[12,{}],<*a,fa*>},{[12,{}]}} is finite V30() countable set

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((a,fa)) is set
K29(K29((a,fa))) is set
fa is Element of the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
a is Element of the InstructionsF of SCM
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
c := s is Element of the InstructionsF of SCM
<*c,s*> is set
[1,{},<*c,s*>] is V13() V14() set
[1,{}] is non natural V13() set

{{1,{}},{1}} is finite V30() countable set
[[1,{}],<*c,s*>] is non natural V13() set
{[1,{}],<*c,s*>} is finite countable set

{{[1,{}],<*c,s*>},{[1,{}]}} is finite V30() countable set
() is non empty Element of bool the carrier of ()
a3 is Int-like Element of the carrier of ()
t is Int-like Element of the carrier of ()
(a3,t) is Element of the InstructionsF of ()
fa is Element of the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
a is Element of the InstructionsF of SCM
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
AddTo (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[2,{},<*c,s*>] is V13() V14() set
[2,{}] is non natural V13() set

{{2,{}},{2}} is finite V30() countable set
[[2,{}],<*c,s*>] is non natural V13() set
{[2,{}],<*c,s*>} is finite countable set

{{[2,{}],<*c,s*>},{[2,{}]}} is finite V30() countable set
() is non empty Element of bool the carrier of ()
a3 is Int-like Element of the carrier of ()
t is Int-like Element of the carrier of ()
(a3,t) is Element of the InstructionsF of ()
fa is Element of the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
a is Element of the InstructionsF of SCM
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
SubFrom (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[3,{},<*c,s*>] is V13() V14() set
[3,{}] is non natural V13() set

{{3,{}