:: SCMPDS_2 semantic presentation

REAL is V63() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V26() V59() V60() V63() Element of K32(REAL)

K32(REAL) is set

omega is non empty epsilon-transitive epsilon-connected ordinal V26() V59() V60() V63() set

K32(omega) is set

K32(NAT) is set

9 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V63() ext-real positive non negative Element of NAT

Segm 9 is V59() Element of K32(omega)

K208() is non empty set

SCM-Memory is non empty set

{NAT} is non empty V63() V64() set

{NAT} \/ K208() is non empty set

K32(SCM-Memory) is set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V63() ext-real positive non negative Element of NAT

K33(SCM-Memory,2) is Relation-like set

K32(K33(SCM-Memory,2)) is set

SCM-OK is non empty Relation-like SCM-Memory -defined 2 -valued Function-like V37( SCM-Memory ) V38( SCM-Memory ,2) Element of K32(K33(SCM-Memory,2))

SCM-VAL is non empty Relation-like 2 -defined Function-like V37(2) set

INT is set

K274(NAT,INT) is set

SCM-OK * SCM-VAL is non empty Relation-like non-empty non empty-yielding SCM-Memory -defined SCM-Memory -defined Function-like V37( SCM-Memory ) V37( SCM-Memory ) set

K191((SCM-OK * SCM-VAL)) is non empty functional V57() V58() set

K209() is non empty Relation-like standard-ins V72() V73() V75() set

K163(K191((SCM-OK * SCM-VAL)),K191((SCM-OK * SCM-VAL))) is non empty functional set

K33(K209(),K163(K191((SCM-OK * SCM-VAL)),K191((SCM-OK * SCM-VAL)))) is Relation-like set

K32(K33(K209(),K163(K191((SCM-OK * SCM-VAL)),K191((SCM-OK * SCM-VAL))))) is set

SCM is non empty with_non-empty_values IC-Ins-separated strict strict halting AMI-Struct over 2

the InstructionsF of SCM is non empty Relation-like standard-ins V72() V73() V75() set

the carrier of SCM is set

the_Values_of SCM is Relation-like the carrier of SCM -defined Function-like V37( the carrier of SCM) set

the Object-Kind of SCM is Relation-like the carrier of SCM -defined 2 -valued Function-like V37( the carrier of SCM) V38( the carrier of SCM,2) Element of K32(K33( the carrier of SCM,2))

K33( the carrier of SCM,2) is Relation-like set

K32(K33( the carrier of SCM,2)) is set

the ValuesF of SCM is non empty Relation-like 2 -defined Function-like V37(2) set

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

K208() \/ INT is non empty set

SCM-Data-Loc is non empty Element of K32(SCM-Memory)

SCM-Data-Loc \/ INT is non empty set

SCMPDS-Instr is non empty Relation-like standard-ins V72() V73() V75() set

0 is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() V56() integer Function-yielding V94() ext-real non positive non negative Element of NAT

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() V56() integer Function-yielding V94() ext-real non positive non negative set

[0,{},{}] is V1() V2() set

[0,{}] is V1() set

{0,{}} is non empty functional set

{0} is non empty functional V57() set

{{0,{}},{0}} is non empty V63() V64() set

[[0,{}],{}] is V1() set

{[0,{}],{}} is non empty set

{[0,{}]} is non empty Relation-like Function-like set

{{[0,{}],{}},{[0,{}]}} is non empty V63() V64() set

{[0,{},{}]} is non empty Relation-like standard-ins V72() V73() V75() set

14 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V63() ext-real positive non negative Element of NAT

{ [14,{},<*b

{[0,{},{}]} \/ { [14,{},<*b

1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V63() ext-real positive non negative Element of NAT

{ [1,{},<*b

({[0,{},{}]} \/ { [14,{},<*b

15 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V63() ext-real positive non negative Element of NAT

Segm 15 is V59() Element of K32(omega)

3 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V63() ext-real positive non negative Element of NAT

{2,3} is non empty V63() V64() set

{ [b

(({[0,{},{}]} \/ { [14,{},<*b

4 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V63() ext-real positive non negative Element of NAT

5 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V63() ext-real positive non negative Element of NAT

6 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V63() ext-real positive non negative Element of NAT

7 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V63() ext-real positive non negative Element of NAT

8 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V63() ext-real positive non negative Element of NAT

{4,5,6,7,8} is V63() set

{ [b

((({[0,{},{}]} \/ { [14,{},<*b

10 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V63() ext-real positive non negative Element of NAT

11 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V63() ext-real positive non negative Element of NAT

12 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V63() ext-real positive non negative Element of NAT

13 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V63() ext-real positive non negative Element of NAT

{9,10,11,12,13} is V63() set

{ [b

(((({[0,{},{}]} \/ { [14,{},<*b

K33(SCMPDS-Instr,K163(K191((SCM-OK * SCM-VAL)),K191((SCM-OK * SCM-VAL)))) is Relation-like set

K32(K33(SCMPDS-Instr,K163(K191((SCM-OK * SCM-VAL)),K191((SCM-OK * SCM-VAL))))) is set

COMPLEX is set

(SCM-OK * SCM-VAL) . NAT is set

RetSP is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

RetIC is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

SCMPDS-Exec is non empty Relation-like SCMPDS-Instr -defined K163(K191((SCM-OK * SCM-VAL)),K191((SCM-OK * SCM-VAL))) -valued Function-like V37( SCMPDS-Instr ) V38( SCMPDS-Instr ,K163(K191((SCM-OK * SCM-VAL)),K191((SCM-OK * SCM-VAL)))) Function-yielding V94() Element of K32(K33(SCMPDS-Instr,K163(K191((SCM-OK * SCM-VAL)),K191((SCM-OK * SCM-VAL)))))

{ [b

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

AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCMPDS-Instr,SCM-OK,SCM-VAL,SCMPDS-Exec #) is strict AMI-Struct over 2

() is strict AMI-Struct over 2

the_Values_of () is Relation-like the carrier of () -defined Function-like V37( the carrier of ()) set

the carrier of () is set

the Object-Kind of () is Relation-like the carrier of () -defined 2 -valued Function-like V37( the carrier of ()) V38( the carrier of (),2) Element of K32(K33( the carrier of (),2))

K33( the carrier of (),2) is Relation-like set

K32(K33( the carrier of (),2)) is set

the ValuesF of () is non empty Relation-like 2 -defined Function-like V37(2) set

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

IC is Element of the carrier of ()

the ZeroF of () is Element of the carrier of ()

Values (IC ) is set

(the_Values_of ()) . (IC ) is set

the carrier of () is set

the_Values_of () is Relation-like the carrier of () -defined Function-like V37( the carrier of ()) set

the Object-Kind of () is Relation-like the carrier of () -defined 2 -valued Function-like V37( the carrier of ()) V38( the carrier of (),2) Element of K32(K33( the carrier of (),2))

K33( the carrier of (),2) is Relation-like set

K32(K33( the carrier of (),2)) is set

the ValuesF of () is non empty Relation-like 2 -defined Function-like V37(2) set

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

IC is Element of the carrier of ()

the ZeroF of () is Element of the carrier of ()

the Element of SCM-Data-Loc is Element of SCM-Data-Loc

S1 is Element of the carrier of ()

S1 is Int-like Element of the carrier of ()

Values S1 is set

(the_Values_of ()) . S1 is set

the InstructionsF of () is non empty Relation-like standard-ins V72() V73() V75() set

{ [14,{},<*b

{ [1,{},<*b

{ [b

{ [b

{ [b

i is Element of the InstructionsF of ()

{[0,{},{}]} \/ { [14,{},<*b

({[0,{},{}]} \/ { [14,{},<*b

(({[0,{},{}]} \/ { [14,{},<*b

((({[0,{},{}]} \/ { [14,{},<*b

i is Element of the InstructionsF of ()

InsCode i is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13(i) is set

K13(K13(i)) is set

i is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V37( the carrier of ()) set

I is Int-like Element of the carrier of ()

i . I is set

d4 is non empty Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible V37( SCM-Memory ) Element of K191((SCM-OK * SCM-VAL))

I3 is Element of SCM-Data-Loc

d4 . I3 is V24() V25() integer ext-real set

i is V24() V25() integer ext-real set

I is V24() V25() integer ext-real set

i + I is V24() V25() integer ext-real set

abs (i + I) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

[1,(abs (i + I))] is V1() set

{1,(abs (i + I))} is non empty set

{1} is non empty V63() V64() set

{{1,(abs (i + I))},{1}} is non empty V63() V64() set

i is V24() V25() integer ext-real set

<*i*> is Relation-like Function-like set

[14,{},<*i*>] is V1() V2() set

[14,{}] is V1() set

{14,{}} is non empty set

{14} is non empty V63() V64() set

{{14,{}},{14}} is non empty V63() V64() set

[[14,{}],<*i*>] is V1() set

{[14,{}],<*i*>} is non empty set

{[14,{}]} is non empty Relation-like Function-like set

{{[14,{}],<*i*>},{[14,{}]}} is non empty V63() V64() set

{[0,{},{}]} \/ { [14,{},<*b

({[0,{},{}]} \/ { [14,{},<*b

(({[0,{},{}]} \/ { [14,{},<*b

((({[0,{},{}]} \/ { [14,{},<*b

i is Element of SCM-Data-Loc

<*i*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like FinSequence-like FinSequence of SCM-Data-Loc

[1,{},<*i*>] is V1() V2() set

[1,{}] is V1() set

{1,{}} is non empty set

{{1,{}},{1}} is non empty V63() V64() set

[[1,{}],<*i*>] is V1() set

{[1,{}],<*i*>} is non empty set

{[1,{}]} is non empty Relation-like Function-like set

{{[1,{}],<*i*>},{[1,{}]}} is non empty V63() V64() set

{[0,{},{}]} \/ { [14,{},<*b

({[0,{},{}]} \/ { [14,{},<*b

(({[0,{},{}]} \/ { [14,{},<*b

((({[0,{},{}]} \/ { [14,{},<*b

i is set

I is Element of SCM-Data-Loc

I3 is V24() V25() integer ext-real set

<*I,I3*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like FinSequence-like FinSequence of SCM-Data-Loc \/ INT

[i,{},<*I,I3*>] is V1() V2() set

[i,{}] is V1() set

{i,{}} is non empty set

{i} is non empty set

{{i,{}},{i}} is non empty V63() V64() set

[[i,{}],<*I,I3*>] is V1() set

{[i,{}],<*I,I3*>} is non empty set

{[i,{}]} is non empty Relation-like Function-like set

{{[i,{}],<*I,I3*>},{[i,{}]}} is non empty V63() V64() set

d4 is Element of Segm 15

[d4,{},<*I,I3*>] is V1() V2() set

[d4,{}] is V1() set

{d4,{}} is non empty set

{d4} is non empty set

{{d4,{}},{d4}} is non empty V63() V64() set

[[d4,{}],<*I,I3*>] is V1() set

{[d4,{}],<*I,I3*>} is non empty set

{[d4,{}]} is non empty Relation-like Function-like set

{{[d4,{}],<*I,I3*>},{[d4,{}]}} is non empty V63() V64() set

{[0,{},{}]} \/ { [14,{},<*b

({[0,{},{}]} \/ { [14,{},<*b

(({[0,{},{}]} \/ { [14,{},<*b

((({[0,{},{}]} \/ { [14,{},<*b

i is set

I is Element of SCM-Data-Loc

I3 is V24() V25() integer ext-real set

d4 is V24() V25() integer ext-real set

<*I,I3,d4*> is set

[i,{},<*I,I3,d4*>] is V1() V2() set

[i,{}] is V1() set

{i,{}} is non empty set

{i} is non empty set

{{i,{}},{i}} is non empty V63() V64() set

[[i,{}],<*I,I3,d4*>] is V1() set

{[i,{}],<*I,I3,d4*>} is non empty set

{[i,{}]} is non empty Relation-like Function-like set

{{[i,{}],<*I,I3,d4*>},{[i,{}]}} is non empty V63() V64() set

d5 is Element of Segm 15

[d5,{},<*I,I3,d4*>] is V1() V2() set

[d5,{}] is V1() set

{d5,{}} is non empty set

{d5} is non empty set

{{d5,{}},{d5}} is non empty V63() V64() set

[[d5,{}],<*I,I3,d4*>] is V1() set

{[d5,{}],<*I,I3,d4*>} is non empty set

{[d5,{}]} is non empty Relation-like Function-like set

{{[d5,{}],<*I,I3,d4*>},{[d5,{}]}} is non empty V63() V64() set

{[0,{},{}]} \/ { [14,{},<*b

({[0,{},{}]} \/ { [14,{},<*b

(({[0,{},{}]} \/ { [14,{},<*b

((({[0,{},{}]} \/ { [14,{},<*b

i is set

I is Element of SCM-Data-Loc

I3 is Element of SCM-Data-Loc

d4 is V24() V25() integer ext-real set

d5 is V24() V25() integer ext-real set

<*I,I3,d4,d5*> is set

[i,{},<*I,I3,d4,d5*>] is V1() V2() set

[i,{}] is V1() set

{i,{}} is non empty set

{i} is non empty set

{{i,{}},{i}} is non empty V63() V64() set

[[i,{}],<*I,I3,d4,d5*>] is V1() set

{[i,{}],<*I,I3,d4,d5*>} is non empty set

{[i,{}]} is non empty Relation-like Function-like set

{{[i,{}],<*I,I3,d4,d5*>},{[i,{}]}} is non empty V63() V64() set

k1 is Element of Segm 15

[k1,{},<*I,I3,d4,d5*>] is V1() V2() set

[k1,{}] is V1() set

{k1,{}} is non empty set

{k1} is non empty set

{{k1,{}},{k1}} is non empty V63() V64() set

[[k1,{}],<*I,I3,d4,d5*>] is V1() set

{[k1,{}],<*I,I3,d4,d5*>} is non empty set

{[k1,{}]} is non empty Relation-like Function-like set

{{[k1,{}],<*I,I3,d4,d5*>},{[k1,{}]}} is non empty V63() V64() set

i is V24() V25() integer ext-real set

<*i*> is Relation-like Function-like set

[14,{},<*i*>] is V1() V2() set

[14,{}] is V1() set

{14,{}} is non empty set

{14} is non empty V63() V64() set

{{14,{}},{14}} is non empty V63() V64() set

[[14,{}],<*i*>] is V1() set

{[14,{}],<*i*>} is non empty set

{[14,{}]} is non empty Relation-like Function-like set

{{[14,{}],<*i*>},{[14,{}]}} is non empty V63() V64() set

i is Int-like Element of the carrier of ()

<*i*> is Relation-like Function-like set

[1,{},<*i*>] is V1() V2() set

[1,{}] is V1() set

{1,{}} is non empty set

{{1,{}},{1}} is non empty V63() V64() set

[[1,{}],<*i*>] is V1() set

{[1,{}],<*i*>} is non empty set

{[1,{}]} is non empty Relation-like Function-like set

{{[1,{}],<*i*>},{[1,{}]}} is non empty V63() V64() set

I is Element of SCM-Data-Loc

<*I*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like FinSequence-like FinSequence of SCM-Data-Loc

[1,{},<*I*>] is V1() V2() set

[[1,{}],<*I*>] is V1() set

{[1,{}],<*I*>} is non empty set

{{[1,{}],<*I*>},{[1,{}]}} is non empty V63() V64() set

i is Int-like Element of the carrier of ()

I is V24() V25() integer ext-real set

<*i,I*> is set

[2,{},<*i,I*>] is V1() V2() set

[2,{}] is V1() set

{2,{}} is non empty set

{2} is non empty V63() V64() set

{{2,{}},{2}} is non empty V63() V64() set

[[2,{}],<*i,I*>] is V1() set

{[2,{}],<*i,I*>} is non empty set

{[2,{}]} is non empty Relation-like Function-like set

{{[2,{}],<*i,I*>},{[2,{}]}} is non empty V63() V64() set

I3 is Element of SCM-Data-Loc

<*I3,I*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like FinSequence-like FinSequence of SCM-Data-Loc \/ INT

[2,{},<*I3,I*>] is V1() V2() set

[[2,{}],<*I3,I*>] is V1() set

{[2,{}],<*I3,I*>} is non empty set

{{[2,{}],<*I3,I*>},{[2,{}]}} is non empty V63() V64() set

[3,{},<*i,I*>] is V1() V2() set

[3,{}] is V1() set

{3,{}} is non empty set

{3} is non empty V63() V64() set

{{3,{}},{3}} is non empty V63() V64() set

[[3,{}],<*i,I*>] is V1() set

{[3,{}],<*i,I*>} is non empty set

{[3,{}]} is non empty Relation-like Function-like set

{{[3,{}],<*i,I*>},{[3,{}]}} is non empty V63() V64() set

I3 is Element of SCM-Data-Loc

<*I3,I*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like FinSequence-like FinSequence of SCM-Data-Loc \/ INT

[3,{},<*I3,I*>] is V1() V2() set

[[3,{}],<*I3,I*>] is V1() set

{[3,{}],<*I3,I*>} is non empty set

{{[3,{}],<*I3,I*>},{[3,{}]}} is non empty V63() V64() set

i is Int-like Element of the carrier of ()

I is V24() V25() integer ext-real set

I3 is V24() V25() integer ext-real set

<*i,I,I3*> is set

[4,{},<*i,I,I3*>] is V1() V2() set

[4,{}] is V1() set

{4,{}} is non empty set

{4} is non empty V63() V64() set

{{4,{}},{4}} is non empty V63() V64() set

[[4,{}],<*i,I,I3*>] is V1() set

{[4,{}],<*i,I,I3*>} is non empty set

{[4,{}]} is non empty Relation-like Function-like set

{{[4,{}],<*i,I,I3*>},{[4,{}]}} is non empty V63() V64() set

d4 is Element of SCM-Data-Loc

<*d4,I,I3*> is set

[4,{},<*d4,I,I3*>] is V1() V2() set

[[4,{}],<*d4,I,I3*>] is V1() set

{[4,{}],<*d4,I,I3*>} is non empty set

{{[4,{}],<*d4,I,I3*>},{[4,{}]}} is non empty V63() V64() set

[5,{},<*i,I,I3*>] is V1() V2() set

[5,{}] is V1() set

{5,{}} is non empty set

{5} is non empty V63() V64() set

{{5,{}},{5}} is non empty V63() V64() set

[[5,{}],<*i,I,I3*>] is V1() set

{[5,{}],<*i,I,I3*>} is non empty set

{[5,{}]} is non empty Relation-like Function-like set

{{[5,{}],<*i,I,I3*>},{[5,{}]}} is non empty V63() V64() set

d4 is Element of SCM-Data-Loc

<*d4,I,I3*> is set

[5,{},<*d4,I,I3*>] is V1() V2() set

[[5,{}],<*d4,I,I3*>] is V1() set

{[5,{}],<*d4,I,I3*>} is non empty set

{{[5,{}],<*d4,I,I3*>},{[5,{}]}} is non empty V63() V64() set

[6,{},<*i,I,I3*>] is V1() V2() set

[6,{}] is V1() set

{6,{}} is non empty set

{6} is non empty V63() V64() set

{{6,{}},{6}} is non empty V63() V64() set

[[6,{}],<*i,I,I3*>] is V1() set

{[6,{}],<*i,I,I3*>} is non empty set

{[6,{}]} is non empty Relation-like Function-like set

{{[6,{}],<*i,I,I3*>},{[6,{}]}} is non empty V63() V64() set

d4 is Element of SCM-Data-Loc

<*d4,I,I3*> is set

[6,{},<*d4,I,I3*>] is V1() V2() set

[[6,{}],<*d4,I,I3*>] is V1() set

{[6,{}],<*d4,I,I3*>} is non empty set

{{[6,{}],<*d4,I,I3*>},{[6,{}]}} is non empty V63() V64() set

[7,{},<*i,I,I3*>] is V1() V2() set

[7,{}] is V1() set

{7,{}} is non empty set

{7} is non empty V63() V64() set

{{7,{}},{7}} is non empty V63() V64() set

[[7,{}],<*i,I,I3*>] is V1() set

{[7,{}],<*i,I,I3*>} is non empty set

{[7,{}]} is non empty Relation-like Function-like set

{{[7,{}],<*i,I,I3*>},{[7,{}]}} is non empty V63() V64() set

d4 is Element of SCM-Data-Loc

<*d4,I,I3*> is set

[7,{},<*d4,I,I3*>] is V1() V2() set

[[7,{}],<*d4,I,I3*>] is V1() set

{[7,{}],<*d4,I,I3*>} is non empty set

{{[7,{}],<*d4,I,I3*>},{[7,{}]}} is non empty V63() V64() set

[8,{},<*i,I,I3*>] is V1() V2() set

[8,{}] is V1() set

{8,{}} is non empty set

{8} is non empty V63() V64() set

{{8,{}},{8}} is non empty V63() V64() set

[[8,{}],<*i,I,I3*>] is V1() set

{[8,{}],<*i,I,I3*>} is non empty set

{[8,{}]} is non empty Relation-like Function-like set

{{[8,{}],<*i,I,I3*>},{[8,{}]}} is non empty V63() V64() set

d4 is Element of SCM-Data-Loc

<*d4,I,I3*> is set

[8,{},<*d4,I,I3*>] is V1() V2() set

[[8,{}],<*d4,I,I3*>] is V1() set

{[8,{}],<*d4,I,I3*>} is non empty set

{{[8,{}],<*d4,I,I3*>},{[8,{}]}} is non empty V63() V64() set

i is Int-like Element of the carrier of ()

I is Int-like Element of the carrier of ()

I3 is V24() V25() integer ext-real set

d4 is V24() V25() integer ext-real set

<*i,I,I3,d4*> is set

[9,{},<*i,I,I3,d4*>] is V1() V2() set

[9,{}] is V1() set

{9,{}} is non empty set

{9} is non empty V63() V64() set

{{9,{}},{9}} is non empty V63() V64() set

[[9,{}],<*i,I,I3,d4*>] is V1() set

{[9,{}],<*i,I,I3,d4*>} is non empty set

{[9,{}]} is non empty Relation-like Function-like set

{{[9,{}],<*i,I,I3,d4*>},{[9,{}]}} is non empty V63() V64() set

d5 is Element of SCM-Data-Loc

k1 is Element of SCM-Data-Loc

<*d5,k1,I3,d4*> is set

[9,{},<*d5,k1,I3,d4*>] is V1() V2() set

[[9,{}],<*d5,k1,I3,d4*>] is V1() set

{[9,{}],<*d5,k1,I3,d4*>} is non empty set

{{[9,{}],<*d5,k1,I3,d4*>},{[9,{}]}} is non empty V63() V64() set

[10,{},<*i,I,I3,d4*>] is V1() V2() set

[10,{}] is V1() set

{10,{}} is non empty set

{10} is non empty V63() V64() set

{{10,{}},{10}} is non empty V63() V64() set

[[10,{}],<*i,I,I3,d4*>] is V1() set

{[10,{}],<*i,I,I3,d4*>} is non empty set

{[10,{}]} is non empty Relation-like Function-like set

{{[10,{}],<*i,I,I3,d4*>},{[10,{}]}} is non empty V63() V64() set

d5 is Element of SCM-Data-Loc

k1 is Element of SCM-Data-Loc

<*d5,k1,I3,d4*> is set

[10,{},<*d5,k1,I3,d4*>] is V1() V2() set

[[10,{}],<*d5,k1,I3,d4*>] is V1() set

{[10,{}],<*d5,k1,I3,d4*>} is non empty set

{{[10,{}],<*d5,k1,I3,d4*>},{[10,{}]}} is non empty V63() V64() set

[11,{},<*i,I,I3,d4*>] is V1() V2() set

[11,{}] is V1() set

{11,{}} is non empty set

{11} is non empty V63() V64() set

{{11,{}},{11}} is non empty V63() V64() set

[[11,{}],<*i,I,I3,d4*>] is V1() set

{[11,{}],<*i,I,I3,d4*>} is non empty set

{[11,{}]} is non empty Relation-like Function-like set

{{[11,{}],<*i,I,I3,d4*>},{[11,{}]}} is non empty V63() V64() set

d5 is Element of SCM-Data-Loc

k1 is Element of SCM-Data-Loc

<*d5,k1,I3,d4*> is set

[11,{},<*d5,k1,I3,d4*>] is V1() V2() set

[[11,{}],<*d5,k1,I3,d4*>] is V1() set

{[11,{}],<*d5,k1,I3,d4*>} is non empty set

{{[11,{}],<*d5,k1,I3,d4*>},{[11,{}]}} is non empty V63() V64() set

[12,{},<*i,I,I3,d4*>] is V1() V2() set

[12,{}] is V1() set

{12,{}} is non empty set

{12} is non empty V63() V64() set

{{12,{}},{12}} is non empty V63() V64() set

[[12,{}],<*i,I,I3,d4*>] is V1() set

{[12,{}],<*i,I,I3,d4*>} is non empty set

{[12,{}]} is non empty Relation-like Function-like set

{{[12,{}],<*i,I,I3,d4*>},{[12,{}]}} is non empty V63() V64() set

d5 is Element of SCM-Data-Loc

k1 is Element of SCM-Data-Loc

<*d5,k1,I3,d4*> is set

[12,{},<*d5,k1,I3,d4*>] is V1() V2() set

[[12,{}],<*d5,k1,I3,d4*>] is V1() set

{[12,{}],<*d5,k1,I3,d4*>} is non empty set

{{[12,{}],<*d5,k1,I3,d4*>},{[12,{}]}} is non empty V63() V64() set

[13,{},<*i,I,I3,d4*>] is V1() V2() set

[13,{}] is V1() set

{13,{}} is non empty set

{13} is non empty V63() V64() set

{{13,{}},{13}} is non empty V63() V64() set

[[13,{}],<*i,I,I3,d4*>] is V1() set

{[13,{}],<*i,I,I3,d4*>} is non empty set

{[13,{}]} is non empty Relation-like Function-like set

{{[13,{}],<*i,I,I3,d4*>},{[13,{}]}} is non empty V63() V64() set

d5 is Element of SCM-Data-Loc

k1 is Element of SCM-Data-Loc

<*d5,k1,I3,d4*> is set

[13,{},<*d5,k1,I3,d4*>] is V1() V2() set

[[13,{}],<*d5,k1,I3,d4*>] is V1() set

{[13,{}],<*d5,k1,I3,d4*>} is non empty set

{{[13,{}],<*d5,k1,I3,d4*>},{[13,{}]}} is non empty V63() V64() set

i is V24() V25() integer ext-real set

(i) is Element of the InstructionsF of ()

<*i*> is Relation-like Function-like set

[14,{},<*i*>] is V1() V2() set

[[14,{}],<*i*>] is V1() set

{[14,{}],<*i*>} is non empty set

{{[14,{}],<*i*>},{[14,{}]}} is non empty V63() V64() set

InsCode (i) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13((i)) is set

K13(K13((i))) is set

i is Int-like Element of the carrier of ()

(i) is Element of the InstructionsF of ()

<*i*> is Relation-like Function-like set

[1,{},<*i*>] is V1() V2() set

[[1,{}],<*i*>] is V1() set

{[1,{}],<*i*>} is non empty set

{{[1,{}],<*i*>},{[1,{}]}} is non empty V63() V64() set

InsCode (i) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13((i)) is set

K13(K13((i))) is set

I is Int-like Element of the carrier of ()

i is V24() V25() integer ext-real set

(I,i) is Element of the InstructionsF of ()

<*I,i*> is set

[2,{},<*I,i*>] is V1() V2() set

[[2,{}],<*I,i*>] is V1() set

{[2,{}],<*I,i*>} is non empty set

{{[2,{}],<*I,i*>},{[2,{}]}} is non empty V63() V64() set

InsCode (I,i) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13((I,i)) is set

K13(K13((I,i))) is set

I is Int-like Element of the carrier of ()

i is V24() V25() integer ext-real set

(I,i) is Element of the InstructionsF of ()

<*I,i*> is set

[3,{},<*I,i*>] is V1() V2() set

[[3,{}],<*I,i*>] is V1() set

{[3,{}],<*I,i*>} is non empty set

{{[3,{}],<*I,i*>},{[3,{}]}} is non empty V63() V64() set

InsCode (I,i) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13((I,i)) is set

K13(K13((I,i))) is set

I3 is Int-like Element of the carrier of ()

i is V24() V25() integer ext-real set

I is V24() V25() integer ext-real set

(I3,i,I) is Element of the InstructionsF of ()

<*I3,i,I*> is set

[4,{},<*I3,i,I*>] is V1() V2() set

[[4,{}],<*I3,i,I*>] is V1() set

{[4,{}],<*I3,i,I*>} is non empty set

{{[4,{}],<*I3,i,I*>},{[4,{}]}} is non empty V63() V64() set

InsCode (I3,i,I) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13((I3,i,I)) is set

K13(K13((I3,i,I))) is set

I3 is Int-like Element of the carrier of ()

i is V24() V25() integer ext-real set

I is V24() V25() integer ext-real set

(I3,i,I) is Element of the InstructionsF of ()

<*I3,i,I*> is set

[5,{},<*I3,i,I*>] is V1() V2() set

[[5,{}],<*I3,i,I*>] is V1() set

{[5,{}],<*I3,i,I*>} is non empty set

{{[5,{}],<*I3,i,I*>},{[5,{}]}} is non empty V63() V64() set

InsCode (I3,i,I) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13((I3,i,I)) is set

K13(K13((I3,i,I))) is set

I3 is Int-like Element of the carrier of ()

i is V24() V25() integer ext-real set

I is V24() V25() integer ext-real set

(I3,i,I) is Element of the InstructionsF of ()

<*I3,i,I*> is set

[6,{},<*I3,i,I*>] is V1() V2() set

[[6,{}],<*I3,i,I*>] is V1() set

{[6,{}],<*I3,i,I*>} is non empty set

{{[6,{}],<*I3,i,I*>},{[6,{}]}} is non empty V63() V64() set

InsCode (I3,i,I) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13((I3,i,I)) is set

K13(K13((I3,i,I))) is set

I3 is Int-like Element of the carrier of ()

i is V24() V25() integer ext-real set

I is V24() V25() integer ext-real set

(I3,i,I) is Element of the InstructionsF of ()

<*I3,i,I*> is set

[7,{},<*I3,i,I*>] is V1() V2() set

[[7,{}],<*I3,i,I*>] is V1() set

{[7,{}],<*I3,i,I*>} is non empty set

{{[7,{}],<*I3,i,I*>},{[7,{}]}} is non empty V63() V64() set

InsCode (I3,i,I) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13((I3,i,I)) is set

K13(K13((I3,i,I))) is set

I3 is Int-like Element of the carrier of ()

i is V24() V25() integer ext-real set

I is V24() V25() integer ext-real set

(I3,i,I) is Element of the InstructionsF of ()

<*I3,i,I*> is set

[8,{},<*I3,i,I*>] is V1() V2() set

[[8,{}],<*I3,i,I*>] is V1() set

{[8,{}],<*I3,i,I*>} is non empty set

{{[8,{}],<*I3,i,I*>},{[8,{}]}} is non empty V63() V64() set

InsCode (I3,i,I) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13((I3,i,I)) is set

K13(K13((I3,i,I))) is set

I3 is Int-like Element of the carrier of ()

d4 is Int-like Element of the carrier of ()

i is V24() V25() integer ext-real set

I is V24() V25() integer ext-real set

(I3,d4,i,I) is Element of the InstructionsF of ()

<*I3,d4,i,I*> is set

[9,{},<*I3,d4,i,I*>] is V1() V2() set

[[9,{}],<*I3,d4,i,I*>] is V1() set

{[9,{}],<*I3,d4,i,I*>} is non empty set

{{[9,{}],<*I3,d4,i,I*>},{[9,{}]}} is non empty V63() V64() set

InsCode (I3,d4,i,I) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13((I3,d4,i,I)) is set

K13(K13((I3,d4,i,I))) is set

I3 is Int-like Element of the carrier of ()

d4 is Int-like Element of the carrier of ()

i is V24() V25() integer ext-real set

I is V24() V25() integer ext-real set

(I3,d4,i,I) is Element of the InstructionsF of ()

<*I3,d4,i,I*> is set

[10,{},<*I3,d4,i,I*>] is V1() V2() set

[[10,{}],<*I3,d4,i,I*>] is V1() set

{[10,{}],<*I3,d4,i,I*>} is non empty set

{{[10,{}],<*I3,d4,i,I*>},{[10,{}]}} is non empty V63() V64() set

InsCode (I3,d4,i,I) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13((I3,d4,i,I)) is set

K13(K13((I3,d4,i,I))) is set

I3 is Int-like Element of the carrier of ()

d4 is Int-like Element of the carrier of ()

i is V24() V25() integer ext-real set

I is V24() V25() integer ext-real set

(I3,d4,i,I) is Element of the InstructionsF of ()

<*I3,d4,i,I*> is set

[11,{},<*I3,d4,i,I*>] is V1() V2() set

[[11,{}],<*I3,d4,i,I*>] is V1() set

{[11,{}],<*I3,d4,i,I*>} is non empty set

{{[11,{}],<*I3,d4,i,I*>},{[11,{}]}} is non empty V63() V64() set

InsCode (I3,d4,i,I) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13((I3,d4,i,I)) is set

K13(K13((I3,d4,i,I))) is set

I3 is Int-like Element of the carrier of ()

d4 is Int-like Element of the carrier of ()

i is V24() V25() integer ext-real set

I is V24() V25() integer ext-real set

(I3,d4,i,I) is Element of the InstructionsF of ()

<*I3,d4,i,I*> is set

[12,{},<*I3,d4,i,I*>] is V1() V2() set

[[12,{}],<*I3,d4,i,I*>] is V1() set

{[12,{}],<*I3,d4,i,I*>} is non empty set

{{[12,{}],<*I3,d4,i,I*>},{[12,{}]}} is non empty V63() V64() set

InsCode (I3,d4,i,I) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13((I3,d4,i,I)) is set

K13(K13((I3,d4,i,I))) is set

I3 is Int-like Element of the carrier of ()

d4 is Int-like Element of the carrier of ()

i is V24() V25() integer ext-real set

I is V24() V25() integer ext-real set

(I3,d4,i,I) is Element of the InstructionsF of ()

<*I3,d4,i,I*> is set

[13,{},<*I3,d4,i,I*>] is V1() V2() set

[[13,{}],<*I3,d4,i,I*>] is V1() set

{[13,{}],<*I3,d4,i,I*>} is non empty set

{{[13,{}],<*I3,d4,i,I*>},{[13,{}]}} is non empty V63() V64() set

InsCode (I3,d4,i,I) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13((I3,d4,i,I)) is set

K13(K13((I3,d4,i,I))) is set

i is Element of the InstructionsF of ()

InsCode i is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13(i) is set

K13(K13(i)) is set

I is V24() V25() integer ext-real Element of INT

<*I*> is Relation-like Function-like set

[14,{},<*I*>] is V1() V2() set

[[14,{}],<*I*>] is V1() set

{[14,{}],<*I*>} is non empty set

{{[14,{}],<*I*>},{[14,{}]}} is non empty V63() V64() set

i is Element of the InstructionsF of ()

InsCode i is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13(i) is set

K13(K13(i)) is set

I is Element of SCM-Data-Loc

<*I*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like FinSequence-like FinSequence of SCM-Data-Loc

[1,{},<*I*>] is V1() V2() set

[[1,{}],<*I*>] is V1() set

{[1,{}],<*I*>} is non empty set

{{[1,{}],<*I*>},{[1,{}]}} is non empty V63() V64() set

i is Element of the InstructionsF of ()

InsCode i is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13(i) is set

K13(K13(i)) is set

I is Element of Segm 15

I3 is Element of SCM-Data-Loc

d4 is V24() V25() integer ext-real Element of INT

<*I3,d4*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like FinSequence-like FinSequence of SCM-Data-Loc \/ INT

[I,{},<*I3,d4*>] is V1() V2() set

[I,{}] is V1() set

{I,{}} is non empty set

{I} is non empty set

{{I,{}},{I}} is non empty V63() V64() set

[[I,{}],<*I3,d4*>] is V1() set

{[I,{}],<*I3,d4*>} is non empty set

{[I,{}]} is non empty Relation-like Function-like set

{{[I,{}],<*I3,d4*>},{[I,{}]}} is non empty V63() V64() set

i is Element of the InstructionsF of ()

InsCode i is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13(i) is set

K13(K13(i)) is set

I is Element of Segm 15

I3 is Element of SCM-Data-Loc

d4 is V24() V25() integer ext-real Element of INT

d5 is V24() V25() integer ext-real Element of INT

<*I3,d4,d5*> is set

[I,{},<*I3,d4,d5*>] is V1() V2() set

[I,{}] is V1() set

{I,{}} is non empty set

{I} is non empty set

{{I,{}},{I}} is non empty V63() V64() set

[[I,{}],<*I3,d4,d5*>] is V1() set

{[I,{}],<*I3,d4,d5*>} is non empty set

{[I,{}]} is non empty Relation-like Function-like set

{{[I,{}],<*I3,d4,d5*>},{[I,{}]}} is non empty V63() V64() set

i is Element of the InstructionsF of ()

InsCode i is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13(i) is set

K13(K13(i)) is set

I is Element of Segm 15

I3 is Element of SCM-Data-Loc

d4 is Element of SCM-Data-Loc

d5 is V24() V25() integer ext-real Element of INT

k1 is V24() V25() integer ext-real Element of INT

<*I3,d4,d5,k1*> is set

[I,{},<*I3,d4,d5,k1*>] is V1() V2() set

[I,{}] is V1() set

{I,{}} is non empty set

{I} is non empty set

{{I,{}},{I}} is non empty V63() V64() set

[[I,{}],<*I3,d4,d5,k1*>] is V1() set

{[I,{}],<*I3,d4,d5,k1*>} is non empty set

{[I,{}]} is non empty Relation-like Function-like set

{{[I,{}],<*I3,d4,d5,k1*>},{[I,{}]}} is non empty V63() V64() set

i is Element of the InstructionsF of ()

InsCode i is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13(i) is set

K13(K13(i)) is set

i is Element of the InstructionsF of ()

InsCode i is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13(i) is set

K13(K13(i)) is set

I is V24() V25() integer ext-real Element of INT

<*I*> is Relation-like Function-like set

[14,{},<*I*>] is V1() V2() set

[[14,{}],<*I*>] is V1() set

{[14,{}],<*I*>} is non empty set

{{[14,{}],<*I*>},{[14,{}]}} is non empty V63() V64() set

(I) is Element of the InstructionsF of ()

i is Element of the InstructionsF of ()

InsCode i is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13(i) is set

K13(K13(i)) is set

I is Element of SCM-Data-Loc

<*I*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like FinSequence-like FinSequence of SCM-Data-Loc

[1,{},<*I*>] is V1() V2() set

[[1,{}],<*I*>] is V1() set

{[1,{}],<*I*>} is non empty set

{{[1,{}],<*I*>},{[1,{}]}} is non empty V63() V64() set

I3 is Int-like Element of the carrier of ()

(I3) is Element of the InstructionsF of ()

<*I3*> is Relation-like Function-like set

[1,{},<*I3*>] is V1() V2() set

[[1,{}],<*I3*>] is V1() set

{[1,{}],<*I3*>} is non empty set

{{[1,{}],<*I3*>},{[1,{}]}} is non empty V63() V64() set

i is Element of the InstructionsF of ()

InsCode i is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of ()

InsCodes the InstructionsF of () is non empty set

K23( the InstructionsF of ()) is set

proj1 the InstructionsF of () is non empty set

proj1 (proj1 the InstructionsF of ()) is set

K13(i) is set

K13(K13(i)) is set

I is Element of Segm 15

I3 is Element of SCM-Data-Loc

d4 is V24() V25() integer ext-real Element of INT

<*I3,d4*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like FinSequence-like FinSequence of SCM-Data-Loc \/ INT

[I,{},<*I3,d4*>] is V1() V2() set

[I,{}] is V1() set

{I,{}} is non empty set

{I} is non empty set

{{I,{}},{I}} is non empty V63() V64() set

[[I,{}],<*I3,d4*>] is V1() set

{[I,{}],<*I3,d4*>} is non empty set

{[I,{}]} is non empty Relation-like Function-like set

{{[I,{}],<*I3,d4*>},{[I,{}]}} is non empty V63() V64() set

d5 is Element of SCM-Data-Loc

k1 is V24() V25() integer ext-real set

<*d5,k1*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like FinSequence-like FinSequence of SCM-Data-Loc \/ INT

[2,{},<*d5,k1*>] is V1() V2() set

[[2,{}],<*d5,k1*>] is V1() set

{[2,{}],<*d5,k1*>} is non