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,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } is set
{[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } is non empty set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V63() ext-real positive non negative Element of NAT
{ [1,{},<*b1*>] where b1 is Element of K208() : verum } is set
({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of K208() : verum } is non empty set
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
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of K208(), b3 is V24() V25() integer ext-real Element of INT : b1 in {2,3} } is set
(({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of K208() : verum } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of K208(), b3 is V24() V25() integer ext-real Element of INT : b1 in {2,3} } is non empty set
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
{ [b1,{},<*b2,b3,b4*>] where b1 is Element of Segm 15, b2 is Element of K208(), b3, b4 is V24() V25() integer ext-real Element of INT : b1 in {4,5,6,7,8} } is set
((({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of K208() : verum } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of K208(), b3 is V24() V25() integer ext-real Element of INT : b1 in {2,3} } ) \/ { [b1,{},<*b2,b3,b4*>] where b1 is Element of Segm 15, b2 is Element of K208(), b3, b4 is V24() V25() integer ext-real Element of INT : b1 in {4,5,6,7,8} } is non empty set
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
{ [b1,{},<*b2,b3,b4,b5*>] where b1 is Element of Segm 15, b2, b3 is Element of K208(), b4, b5 is V24() V25() integer ext-real Element of INT : b1 in {9,10,11,12,13} } is set
(((({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of K208() : verum } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of K208(), b3 is V24() V25() integer ext-real Element of INT : b1 in {2,3} } ) \/ { [b1,{},<*b2,b3,b4*>] where b1 is Element of Segm 15, b2 is Element of K208(), b3, b4 is V24() V25() integer ext-real Element of INT : b1 in {4,5,6,7,8} } ) \/ { [b1,{},<*b2,b3,b4,b5*>] where b1 is Element of Segm 15, b2, b3 is Element of K208(), b4, b5 is V24() V25() integer ext-real Element of INT : b1 in {9,10,11,12,13} } is non empty set
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)))))
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of K208(), b3 is V24() V25() integer ext-real Element of INT : b1 in {2,3} } is set
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,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } is set
{ [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } is set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3 is V24() V25() integer ext-real Element of INT : b1 in {2,3} } is set
{ [b1,{},<*b2,b3,b4*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3, b4 is V24() V25() integer ext-real Element of INT : b1 in {4,5,6,7,8} } is set
{ [b1,{},<*b2,b3,b4,b5*>] where b1 is Element of Segm 15, b2, b3 is Element of SCM-Data-Loc , b4, b5 is V24() V25() integer ext-real Element of INT : b1 in {9,10,11,12,13} } is set
i is Element of the InstructionsF of ()
{[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } is non empty set
({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } is non empty set
(({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3 is V24() V25() integer ext-real Element of INT : b1 in {2,3} } is non empty set
((({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3 is V24() V25() integer ext-real Element of INT : b1 in {2,3} } ) \/ { [b1,{},<*b2,b3,b4*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3, b4 is V24() V25() integer ext-real Element of INT : b1 in {4,5,6,7,8} } is non empty 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 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,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } is non empty set
({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } is non empty set
(({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3 is V24() V25() integer ext-real Element of INT : b1 in {2,3} } is non empty set
((({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3 is V24() V25() integer ext-real Element of INT : b1 in {2,3} } ) \/ { [b1,{},<*b2,b3,b4*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3, b4 is V24() V25() integer ext-real Element of INT : b1 in {4,5,6,7,8} } is non empty 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,{}] 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,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } is non empty set
({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } is non empty set
(({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3 is V24() V25() integer ext-real Element of INT : b1 in {2,3} } is non empty set
((({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3 is V24() V25() integer ext-real Element of INT : b1 in {2,3} } ) \/ { [b1,{},<*b2,b3,b4*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3, b4 is V24() V25() integer ext-real Element of INT : b1 in {4,5,6,7,8} } is non empty set
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,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } is non empty set
({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } is non empty set
(({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3 is V24() V25() integer ext-real Element of INT : b1 in {2,3} } is non empty set
((({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3 is V24() V25() integer ext-real Element of INT : b1 in {2,3} } ) \/ { [b1,{},<*b2,b3,b4*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3, b4 is V24() V25() integer ext-real Element of INT : b1 in {4,5,6,7,8} } is non empty set
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,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } is non empty set
({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } is non empty set
(({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3 is V24() V25() integer ext-real Element of INT : b1 in {2,3} } is non empty set
((({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V24() V25() integer ext-real Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3 is V24() V25() integer ext-real Element of INT : b1 in {2,3} } ) \/ { [b1,{},<*b2,b3,b4*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3, b4 is V24() V25() integer ext-real Element of INT : b1 in {4,5,6,7,8} } is non empty set
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