:: SCMRINGI semantic presentation

REAL is set
NAT is V6() V7() V8() non empty Element of bool REAL
bool REAL is set
NAT is V6() V7() V8() non empty set
bool NAT is set
bool NAT is set
2 is V6() V7() V8() V12() non empty ext-real positive non negative Element of NAT
[:2,2:] is Relation-like set
[:[:2,2:],2:] is Relation-like set
bool [:[:2,2:],2:] is set
9 is V6() V7() V8() V12() non empty ext-real positive non negative Element of NAT
Segm 9 is non empty Element of bool NAT
SCM-Data-Loc is non empty set
1 is V6() V7() V8() V12() non empty ext-real positive non negative Element of NAT
K168(NAT,1) is non empty Element of bool NAT
[:K168(NAT,1),NAT:] is Relation-like Element of bool [:NAT,REAL:]
[:NAT,REAL:] is Relation-like set
bool [:NAT,REAL:] is set
RAT is set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty V24() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued set
INT is set
3 is V6() V7() V8() V12() non empty ext-real positive non negative Element of NAT
Seg 1 is non empty V24() 1 -element Element of bool NAT
{ b₁ where b₁ is V6() V7() V8() V12() ext-real Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty set
Seg 2 is non empty V24() 2 -element Element of bool NAT
{ b₁ where b₁ is V6() V7() V8() V12() ext-real Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{1,2} is non empty set
7 is V6() V7() V8() V12() non empty ext-real positive non negative Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty V24() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued Element of NAT
4 is V6() V7() V8() V12() non empty ext-real positive non negative Element of NAT
5 is V6() V7() V8() V12() non empty ext-real positive non negative Element of NAT
6 is V6() V7() V8() V12() non empty ext-real positive non negative Element of NAT
K168(NAT,0) is functional non empty Element of bool NAT
8 is V6() V7() V8() V12() non empty ext-real positive non negative Element of NAT
Segm 8 is non empty Element of bool NAT
SCM-Instr is Relation-like non empty standard-ins homogeneous J/A-independent with_halt set
SCM-Halt is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty V24() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued Element of Segm 9
[SCM-Halt,{},{}] is V21() V22() set
[SCM-Halt,{}] is V21() set
{SCM-Halt,{}} is functional non empty set
{SCM-Halt} is functional non empty set
{{SCM-Halt,{}},{SCM-Halt}} is non empty set
[[SCM-Halt,{}],{}] is V21() set
{[SCM-Halt,{}],{}} is non empty set
{[SCM-Halt,{}]} is Relation-like Function-like non empty set
{{[SCM-Halt,{}],{}},{[SCM-Halt,{}]}} is non empty set
{[SCM-Halt,{},{}]} is Relation-like non empty standard-ins homogeneous J/A-independent with_halt set
{ [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V6() V7() V8() V12() ext-real Element of NAT : b₁ = 6 } is set
{[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V6() V7() V8() V12() ext-real Element of NAT : b₁ = 6 } is non empty set
K169(NAT,7,8) is non empty Element of bool NAT
{ [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V6() V7() V8() V12() ext-real Element of NAT , b₃ is Element of SCM-Data-Loc : b₁ in K169(NAT,7,8) } is set
({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V6() V7() V8() V12() ext-real Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V6() V7() V8() V12() ext-real Element of NAT , b₃ is Element of SCM-Data-Loc : b₁ in K169(NAT,7,8) } is non empty set
K172(NAT,1,2,3,4,5) is Element of bool NAT
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 9, b₂, b₃ is Element of SCM-Data-Loc : b₁ in K172(NAT,1,2,3,4,5) } is set
(({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V6() V7() V8() V12() ext-real Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V6() V7() V8() V12() ext-real Element of NAT , b₃ is Element of SCM-Data-Loc : b₁ in K169(NAT,7,8) } ) \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 9, b₂, b₃ is Element of SCM-Data-Loc : b₁ in K172(NAT,1,2,3,4,5) } is non empty set
the Element of SCM-Data-Loc is Element of SCM-Data-Loc
{1,2,3,4,5} is set
<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
<* the Element of SCM-Data-Loc *> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1, the Element of SCM-Data-Loc ] is V21() set
{1, the Element of SCM-Data-Loc } is non empty set
{{1, the Element of SCM-Data-Loc },{1}} is non empty set
{[1, the Element of SCM-Data-Loc ]} is Relation-like Function-like non empty set
K75(<* the Element of SCM-Data-Loc *>,<* the Element of SCM-Data-Loc *>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
K313(1,1) is V6() V7() V8() V12() ext-real Element of NAT
[1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] is V21() V22() set
[1,{}] is V21() set
{1,{}} is non empty set
{{1,{}},{1}} is non empty set
[[1,{}],<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] is V21() set
{[1,{}],<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>} is non empty set
{[1,{}]} is Relation-like Function-like non empty set
{{[1,{}],<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>},{[1,{}]}} is non empty set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 9, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4,5} } is set
[2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] is V21() V22() set
[2,{}] is V21() set
{2,{}} is non empty set
{2} is non empty set
{{2,{}},{2}} is non empty set
[[2,{}],<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] is V21() set
{[2,{}],<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>} is non empty set
{[2,{}]} is Relation-like Function-like non empty set
{{[2,{}],<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>},{[2,{}]}} is non empty set
[0,{},{}] is V21() V22() set
[0,{}] is V21() set
{0,{}} is functional non empty set
{0} is functional non empty set
{{0,{}},{0}} is non empty set
[[0,{}],{}] is V21() set
{[0,{}],{}} is non empty set
{[0,{}]} is Relation-like Function-like non empty set
{{[0,{}],{}},{[0,{}]}} is non empty set
{[0,{},{}]} is Relation-like non empty standard-ins homogeneous J/A-independent with_halt set
{1,2,3,4} is set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } is set
{[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } is non empty set
{ [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } is set
({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } is non empty set
{ [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } is set
(({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } is non empty set
S is non empty 1-sorted
the carrier of S is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set
S is non empty 1-sorted
(S) is non empty set
the carrier of S is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set
the Element of SCM-Data-Loc is Element of SCM-Data-Loc
{ [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
(({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ ( { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } ) is non empty set
{ [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } \/ ( { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } ) is set
({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ ( { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } \/ ( { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } )) is non empty set
{[0,{},{}]} \/ ( { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } \/ ( { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } )) is non empty set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } \/ ({[0,{},{}]} \/ ( { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } \/ ( { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } ))) is non empty set
<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
<* the Element of SCM-Data-Loc *> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1, the Element of SCM-Data-Loc ] is V21() set
{1, the Element of SCM-Data-Loc } is non empty set
{{1, the Element of SCM-Data-Loc },{1}} is non empty set
{[1, the Element of SCM-Data-Loc ]} is Relation-like Function-like non empty set
K75(<* the Element of SCM-Data-Loc *>,<* the Element of SCM-Data-Loc *>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
K313(1,1) is V6() V7() V8() V12() ext-real Element of NAT
[2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] is V21() V22() set
[2,{}] is V21() set
{2,{}} is non empty set
{2} is non empty set
{{2,{}},{2}} is non empty set
[[2,{}],<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] is V21() set
{[2,{}],<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>} is non empty set
{[2,{}]} is Relation-like Function-like non empty set
{{[2,{}],<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>},{[2,{}]}} is non empty set
[1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] is V21() V22() set
[1,{}] is V21() set
{1,{}} is non empty set
{{1,{}},{1}} is non empty set
[[1,{}],<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] is V21() set
{[1,{}],<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>} is non empty set
{[1,{}]} is Relation-like Function-like non empty set
{{[1,{}],<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>},{[1,{}]}} is non empty set
S is non empty 1-sorted
(S) is non empty non trivial set
the carrier of S is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set
d1 is Element of (S)
I1 is Element of Segm 8
i1 is Element of SCM-Data-Loc
D1 is Element of SCM-Data-Loc
<*i1,D1*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
<*i1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
<*D1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
K75(<*i1*>,<*D1*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
K313(1,1) is V6() V7() V8() V12() ext-real Element of NAT
[I1,{},<*i1,D1*>] is V21() V22() set
[I1,{}] is V21() set
{I1,{}} is non empty set
{I1} is non empty set
{{I1,{}},{I1}} is non empty set
[[I1,{}],<*i1,D1*>] is V21() set
{[I1,{}],<*i1,D1*>} is non empty set
{[I1,{}]} is Relation-like Function-like non empty set
{{[I1,{}],<*i1,D1*>},{[I1,{}]}} is non empty set
d1 `3_3 is set
<*i1,D1*> /. 1 is Element of SCM-Data-Loc
i1 is Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
D2 is Element of SCM-Data-Loc
i1 /. 1 is Element of SCM-Data-Loc
a is Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
x is Element of SCM-Data-Loc
a /. 1 is Element of SCM-Data-Loc
<*i1,D1*> /. 2 is Element of SCM-Data-Loc
i1 is Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
D2 is Element of SCM-Data-Loc
i1 /. 2 is Element of SCM-Data-Loc
a is Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
x is Element of SCM-Data-Loc
a /. 2 is Element of SCM-Data-Loc
S is Element of Segm 8
d1 is non empty 1-sorted
(d1) is non empty non trivial set
the carrier of d1 is non empty set
{ [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of d1 : verum } is set
((({[0,{},{}]} \/ { [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 8, b<sub>2</sub>, b<sub>3</sub> is Element of SCM-Data-Loc : b<sub>1</sub> in {1,2,3,4} } ) \/ { [6,<*b<sub>1</sub>*>,{}] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b<sub>1</sub>*>,<*b<sub>2</sub>*>] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT , b<sub>2</sub> is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of d1 : verum } is non empty set
i1 is Element of (d1)
(d1,i1) is Element of SCM-Data-Loc
(d1,i1) is Element of SCM-Data-Loc
D1 is Element of SCM-Data-Loc
I1 is Element of SCM-Data-Loc
<*D1,I1*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
<*D1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
<*I1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,I1] is V21() set
{1,I1} is non empty set
{{1,I1},{1}} is non empty set
{[1,I1]} is Relation-like Function-like non empty set
K75(<*D1*>,<*I1*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[S,{},<*D1,I1*>] is V21() V22() set
[S,{}] is V21() set
{S,{}} is non empty set
{S} is non empty set
{{S,{}},{S}} is non empty set
[[S,{}],<*D1,I1*>] is V21() set
{[S,{}],<*D1,I1*>} is non empty set
{[S,{}]} is Relation-like Function-like non empty set
{{[S,{}],<*D1,I1*>},{[S,{}]}} is non empty set
i1 `3_3 is set
D2 is Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
D2 /. 1 is Element of SCM-Data-Loc
x is Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
x /. 2 is Element of SCM-Data-Loc
S is non empty 1-sorted
(S) is non empty non trivial set
the carrier of S is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set
d1 is Element of (S)
D1 is Element of Segm 8
i1 is V6() V7() V8() V12() ext-real Element of NAT
<*i1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
[D1,<*i1*>,{}] is V21() V22() set
[D1,<*i1*>] is V21() set
{D1,<*i1*>} is non empty set
{D1} is non empty set
{{D1,<*i1*>},{D1}} is non empty set
[[D1,<*i1*>],{}] is V21() set
{[D1,<*i1*>],{}} is non empty set
{[D1,<*i1*>]} is Relation-like Function-like non empty set
{{[D1,<*i1*>],{}},{[D1,<*i1*>]}} is non empty set
d1 `2_3 is set
K41(d1) is set
K41(d1) `3_3 is set
<*i1*> /. 1 is V6() V7() V8() V12() ext-real Element of NAT
x is Relation-like NAT -defined NAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
I1 is V6() V7() V8() V12() ext-real Element of NAT
x /. 1 is V6() V7() V8() V12() ext-real Element of NAT
i1 is Relation-like NAT -defined NAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
D2 is V6() V7() V8() V12() ext-real Element of NAT
i1 /. 1 is V6() V7() V8() V12() ext-real Element of NAT
S is Element of Segm 8
d1 is non empty 1-sorted
(d1) is non empty non trivial set
the carrier of d1 is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of d1 : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of d1 : verum } is non empty set
i1 is Element of (d1)
(d1,i1) is V6() V7() V8() V12() ext-real Element of NAT
D1 is V6() V7() V8() V12() ext-real Element of NAT
<*D1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
[S,<*D1*>,{}] is V21() V22() set
[S,<*D1*>] is V21() set
{S,<*D1*>} is non empty set
{S} is non empty set
{{S,<*D1*>},{S}} is non empty set
[[S,<*D1*>],{}] is V21() set
{[S,<*D1*>],{}} is non empty set
{[S,<*D1*>]} is Relation-like Function-like non empty set
{{[S,<*D1*>],{}},{[S,<*D1*>]}} is non empty set
i1 `2_3 is set
K41(i1) is set
K41(i1) `3_3 is set
I1 is Relation-like NAT -defined NAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
I1 /. 1 is V6() V7() V8() V12() ext-real Element of NAT
S is non empty 1-sorted
(S) is non empty non trivial set
the carrier of S is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set
d1 is Element of (S)
I1 is Element of Segm 8
i1 is V6() V7() V8() V12() ext-real Element of NAT
<*i1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
D1 is Element of SCM-Data-Loc
<*D1*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
[I1,<*i1*>,<*D1*>] is V21() V22() set
[I1,<*i1*>] is V21() set
{I1,<*i1*>} is non empty set
{I1} is non empty set
{{I1,<*i1*>},{I1}} is non empty set
[[I1,<*i1*>],<*D1*>] is V21() set
{[I1,<*i1*>],<*D1*>} is non empty set
{[I1,<*i1*>]} is Relation-like Function-like non empty set
{{[I1,<*i1*>],<*D1*>},{[I1,<*i1*>]}} is non empty set
d1 `2_3 is set
K41(d1) is set
K41(d1) `3_3 is set
<*i1*> /. 1 is V6() V7() V8() V12() ext-real Element of NAT
i1 is V6() V7() V8() V12() ext-real Element of NAT
<*i1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
D2 is V6() V7() V8() V12() ext-real Element of NAT
<*i1*> /. 1 is V6() V7() V8() V12() ext-real Element of NAT
a is V6() V7() V8() V12() ext-real Element of NAT
<*a*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,a] is V21() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like non empty set
x is V6() V7() V8() V12() ext-real Element of NAT
<*a*> /. 1 is V6() V7() V8() V12() ext-real Element of NAT
d1 `3_3 is set
<*D1*> /. 1 is Element of SCM-Data-Loc
i1 is Element of SCM-Data-Loc
<*i1*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
D2 is Element of SCM-Data-Loc
<*i1*> /. 1 is Element of SCM-Data-Loc
a is Element of SCM-Data-Loc
<*a*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,a] is V21() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like non empty set
x is Element of SCM-Data-Loc
<*a*> /. 1 is Element of SCM-Data-Loc
S is Element of Segm 8
d1 is non empty 1-sorted
(d1) is non empty non trivial set
the carrier of d1 is non empty set
{ [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of d1 : verum } is set
((({[0,{},{}]} \/ { [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 8, b<sub>2</sub>, b<sub>3</sub> is Element of SCM-Data-Loc : b<sub>1</sub> in {1,2,3,4} } ) \/ { [6,<*b<sub>1</sub>*>,{}] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b<sub>1</sub>*>,<*b<sub>2</sub>*>] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT , b<sub>2</sub> is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of d1 : verum } is non empty set
i1 is Element of (d1)
(d1,i1) is V6() V7() V8() V12() ext-real Element of NAT
(d1,i1) is Element of SCM-Data-Loc
D1 is V6() V7() V8() V12() ext-real Element of NAT
<*D1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
I1 is Element of SCM-Data-Loc
<*I1*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,I1] is V21() set
{1,I1} is non empty set
{{1,I1},{1}} is non empty set
{[1,I1]} is Relation-like Function-like non empty set
[S,<*D1*>,<*I1*>] is V21() V22() set
[S,<*D1*>] is V21() set
{S,<*D1*>} is non empty set
{S} is non empty set
{{S,<*D1*>},{S}} is non empty set
[[S,<*D1*>],<*I1*>] is V21() set
{[S,<*D1*>],<*I1*>} is non empty set
{[S,<*D1*>]} is Relation-like Function-like non empty set
{{[S,<*D1*>],<*I1*>},{[S,<*D1*>]}} is non empty set
i1 `2_3 is set
K41(i1) is set
K41(i1) `3_3 is set
D2 is V6() V7() V8() V12() ext-real Element of NAT
<*D2*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,D2] is V21() set
{1,D2} is non empty set
{{1,D2},{1}} is non empty set
{[1,D2]} is Relation-like Function-like non empty set
<*D2*> /. 1 is V6() V7() V8() V12() ext-real Element of NAT
i1 `3_3 is set
x is Element of SCM-Data-Loc
<*x*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,x] is V21() set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like non empty set
<*x*> /. 1 is Element of SCM-Data-Loc
S is non empty 1-sorted
the carrier of S is non empty set
d1 is Element of SCM-Data-Loc
i1 is Element of the carrier of S
<*d1,i1*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like set
<*d1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,d1] is V21() set
{1,d1} is non empty set
{{1,d1},{1}} is non empty set
{[1,d1]} is Relation-like Function-like non empty set
<*i1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
K75(<*d1*>,<*i1*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
SCM-Data-Loc \/ the carrier of S is non empty set
D1 is set
proj2 <*d1,i1*> is non empty set
dom <*d1,i1*> is non empty Element of bool NAT
I1 is set
<*d1,i1*> . I1 is set
S is non empty 1-sorted
(S) is non empty non trivial set
the carrier of S is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set
d1 is Element of (S)
I1 is Element of Segm 8
i1 is Element of SCM-Data-Loc
D1 is Element of the carrier of S
(S,i1,D1) is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of S -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ the carrier of S
SCM-Data-Loc \/ the carrier of S is non empty set
<*i1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
<*D1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
K75(<*i1*>,<*D1*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[I1,{},(S,i1,D1)] is V21() V22() set
[I1,{}] is V21() set
{I1,{}} is non empty set
{I1} is non empty set
{{I1,{}},{I1}} is non empty set
[[I1,{}],(S,i1,D1)] is V21() set
{[I1,{}],(S,i1,D1)} is non empty set
{[I1,{}]} is Relation-like Function-like non empty set
{{[I1,{}],(S,i1,D1)},{[I1,{}]}} is non empty set
d1 `3_3 is set
(S,i1,D1) /. 1 is Element of SCM-Data-Loc \/ the carrier of S
i1 is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of S -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ the carrier of S
D2 is Element of SCM-Data-Loc
i1 /. 1 is Element of SCM-Data-Loc \/ the carrier of S
a is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of S -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ the carrier of S
x is Element of SCM-Data-Loc
a /. 1 is Element of SCM-Data-Loc \/ the carrier of S
(S,i1,D1) /. 2 is Element of SCM-Data-Loc \/ the carrier of S
i1 is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of S -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ the carrier of S
D2 is Element of the carrier of S
i1 /. 2 is Element of SCM-Data-Loc \/ the carrier of S
a is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of S -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ the carrier of S
x is Element of the carrier of S
a /. 2 is Element of SCM-Data-Loc \/ the carrier of S
S is Element of Segm 8
d1 is non empty 1-sorted
(d1) is non empty non trivial set
the carrier of d1 is non empty set
{ [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of d1 : verum } is set
((({[0,{},{}]} \/ { [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 8, b<sub>2</sub>, b<sub>3</sub> is Element of SCM-Data-Loc : b<sub>1</sub> in {1,2,3,4} } ) \/ { [6,<*b<sub>1</sub>*>,{}] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b<sub>1</sub>*>,<*b<sub>2</sub>*>] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT , b<sub>2</sub> is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of d1 : verum } is non empty set
i1 is Element of (d1)
(d1,i1) is Element of SCM-Data-Loc
(d1,i1) is Element of the carrier of d1
D1 is Element of SCM-Data-Loc
I1 is Element of the carrier of d1
(d1,D1,I1) is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of d1 -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ the carrier of d1
SCM-Data-Loc \/ the carrier of d1 is non empty set
<*D1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
<*I1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,I1] is V21() set
{1,I1} is non empty set
{{1,I1},{1}} is non empty set
{[1,I1]} is Relation-like Function-like non empty set
K75(<*D1*>,<*I1*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[S,{},(d1,D1,I1)] is V21() V22() set
[S,{}] is V21() set
{S,{}} is non empty set
{S} is non empty set
{{S,{}},{S}} is non empty set
[[S,{}],(d1,D1,I1)] is V21() set
{[S,{}],(d1,D1,I1)} is non empty set
{[S,{}]} is Relation-like Function-like non empty set
{{[S,{}],(d1,D1,I1)},{[S,{}]}} is non empty set
i1 `3_3 is set
D2 is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of d1 -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ the carrier of d1
D2 /. 1 is Element of SCM-Data-Loc \/ the carrier of d1
x is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of d1 -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ the carrier of d1
x /. 2 is Element of SCM-Data-Loc \/ the carrier of d1
NAT * is functional non empty FinSequence-membered set
S is non empty 1-sorted
(S) is non empty non trivial set
the carrier of S is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set
proj2 (S) is set
[:NAT,(NAT *),(proj2 (S)):] is set
i1 is set
D1 is Element of Segm 8
I1 is Element of SCM-Data-Loc
D2 is Element of SCM-Data-Loc
<*I1,D2*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
<*I1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,I1] is V21() set
{1,I1} is non empty set
{{1,I1},{1}} is non empty set
{[1,I1]} is Relation-like Function-like non empty set
<*D2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,D2] is V21() set
{1,D2} is non empty set
{{1,D2},{1}} is non empty set
{[1,D2]} is Relation-like Function-like non empty set
K75(<*I1*>,<*D2*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[D1,{},<*I1,D2*>] is V21() V22() set
[D1,{}] is V21() set
{D1,{}} is non empty set
{D1} is non empty set
{{D1,{}},{D1}} is non empty set
[[D1,{}],<*I1,D2*>] is V21() set
{[D1,{}],<*I1,D2*>} is non empty set
{[D1,{}]} is Relation-like Function-like non empty set
{{[D1,{}],<*I1,D2*>},{[D1,{}]}} is non empty set
D1 is V6() V7() V8() V12() ext-real Element of NAT
<*D1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
[6,<*D1*>,{}] is V21() V22() set
[6,<*D1*>] is V21() set
{6,<*D1*>} is non empty set
{6} is non empty set
{{6,<*D1*>},{6}} is non empty set
[[6,<*D1*>],{}] is V21() set
{[6,<*D1*>],{}} is non empty set
{[6,<*D1*>]} is Relation-like Function-like non empty set
{{[6,<*D1*>],{}},{[6,<*D1*>]}} is non empty set
D1 is V6() V7() V8() V12() ext-real Element of NAT
<*D1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
I1 is Element of SCM-Data-Loc
<*I1*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,I1] is V21() set
{1,I1} is non empty set
{{1,I1},{1}} is non empty set
{[1,I1]} is Relation-like Function-like non empty set
[7,<*D1*>,<*I1*>] is V21() V22() set
[7,<*D1*>] is V21() set
{7,<*D1*>} is non empty set
{7} is non empty set
{{7,<*D1*>},{7}} is non empty set
[[7,<*D1*>],<*I1*>] is V21() set
{[7,<*D1*>],<*I1*>} is non empty set
{[7,<*D1*>]} is Relation-like Function-like non empty set
{{[7,<*D1*>],<*I1*>},{[7,<*D1*>]}} is non empty set
{ [5,{},(S,b₁,b₂)] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
D1 is Element of SCM-Data-Loc
I1 is Element of the carrier of S
(S,D1,I1) is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of S -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ the carrier of S
SCM-Data-Loc \/ the carrier of S is non empty set
<*D1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
<*I1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,I1] is V21() set
{1,I1} is non empty set
{{1,I1},{1}} is non empty set
{[1,I1]} is Relation-like Function-like non empty set
K75(<*D1*>,<*I1*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[5,{},(S,D1,I1)] is V21() V22() set
[5,{}] is V21() set
{5,{}} is non empty set
{5} is non empty set
{{5,{}},{5}} is non empty set
[[5,{}],(S,D1,I1)] is V21() set
{[5,{}],(S,D1,I1)} is non empty set
{[5,{}]} is Relation-like Function-like non empty set
{{[5,{}],(S,D1,I1)},{[5,{}]}} is non empty set
{ [5,{},(S,b₁,b₂)] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
S is non empty 1-sorted
(S) is non empty non trivial set
the carrier of S is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set
proj2 (S) is set
d1 is set
i1 is set
[i1,d1] is V21() set
{i1,d1} is non empty set
{i1} is non empty set
{{i1,d1},{i1}} is non empty set
I1 is Element of Segm 8
D2 is Element of SCM-Data-Loc
x is Element of SCM-Data-Loc
<*D2,x*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
<*D2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,D2] is V21() set
{1,D2} is non empty set
{{1,D2},{1}} is non empty set
{[1,D2]} is Relation-like Function-like non empty set
<*x*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,x] is V21() set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like non empty set
K75(<*D2*>,<*x*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[I1,{},<*D2,x*>] is V21() V22() set
[I1,{}] is V21() set
{I1,{}} is non empty set
{I1} is non empty set
{{I1,{}},{I1}} is non empty set
[[I1,{}],<*D2,x*>] is V21() set
{[I1,{}],<*D2,x*>} is non empty set
{[I1,{}]} is Relation-like Function-like non empty set
{{[I1,{}],<*D2,x*>},{[I1,{}]}} is non empty set
I1 is V6() V7() V8() V12() ext-real Element of NAT
<*I1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,I1] is V21() set
{1,I1} is non empty set
{{1,I1},{1}} is non empty set
{[1,I1]} is Relation-like Function-like non empty set
[6,<*I1*>,{}] is V21() V22() set
[6,<*I1*>] is V21() set
{6,<*I1*>} is non empty set
{6} is non empty set
{{6,<*I1*>},{6}} is non empty set
[[6,<*I1*>],{}] is V21() set
{[6,<*I1*>],{}} is non empty set
{[6,<*I1*>]} is Relation-like Function-like non empty set
{{[6,<*I1*>],{}},{[6,<*I1*>]}} is non empty set
I1 is V6() V7() V8() V12() ext-real Element of NAT
<*I1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,I1] is V21() set
{1,I1} is non empty set
{{1,I1},{1}} is non empty set
{[1,I1]} is Relation-like Function-like non empty set
D2 is Element of SCM-Data-Loc
<*D2*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,D2] is V21() set
{1,D2} is non empty set
{{1,D2},{1}} is non empty set
{[1,D2]} is Relation-like Function-like non empty set
[7,<*I1*>,<*D2*>] is V21() V22() set
[7,<*I1*>] is V21() set
{7,<*I1*>} is non empty set
{7} is non empty set
{{7,<*I1*>},{7}} is non empty set
[[7,<*I1*>],<*D2*>] is V21() set
{[7,<*I1*>],<*D2*>} is non empty set
{[7,<*I1*>]} is Relation-like Function-like non empty set
{{[7,<*I1*>],<*D2*>},{[7,<*I1*>]}} is non empty set
{ [5,{},(S,b₁,b₂)] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
I1 is Element of SCM-Data-Loc
D2 is Element of the carrier of S
(S,I1,D2) is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of S -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ the carrier of S
SCM-Data-Loc \/ the carrier of S is non empty set
<*I1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,I1] is V21() set
{1,I1} is non empty set
{{1,I1},{1}} is non empty set
{[1,I1]} is Relation-like Function-like non empty set
<*D2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,D2] is V21() set
{1,D2} is non empty set
{{1,D2},{1}} is non empty set
{[1,D2]} is Relation-like Function-like non empty set
K75(<*I1*>,<*D2*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[5,{},(S,I1,D2)] is V21() V22() set
[5,{}] is V21() set
{5,{}} is non empty set
{5} is non empty set
{{5,{}},{5}} is non empty set
[[5,{}],(S,I1,D2)] is V21() set
{[5,{}],(S,I1,D2)} is non empty set
{[5,{}]} is Relation-like Function-like non empty set
{{[5,{}],(S,I1,D2)},{[5,{}]}} is non empty set
{ [5,{},(S,b₁,b₂)] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
S is non empty 1-sorted
(S) is non empty non trivial set
the carrier of S is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set
S is non empty 1-sorted
(S) is non empty non trivial set
the carrier of S is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set
{ [5,{},(S,b₁,b₂)] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
d1 is Element of (S)
d1 `1_3 is set
K41(d1) is set
K41(K41(d1)) is set
i1 is Element of Segm 8
D1 is Element of SCM-Data-Loc
I1 is Element of SCM-Data-Loc
<*D1,I1*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
<*D1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
<*I1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,I1] is V21() set
{1,I1} is non empty set
{{1,I1},{1}} is non empty set
{[1,I1]} is Relation-like Function-like non empty set
K75(<*D1*>,<*I1*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[i1,{},<*D1,I1*>] is V21() V22() set
[i1,{}] is V21() set
{i1,{}} is non empty set
{i1} is non empty set
{{i1,{}},{i1}} is non empty set
[[i1,{}],<*D1,I1*>] is V21() set
{[i1,{}],<*D1,I1*>} is non empty set
{[i1,{}]} is Relation-like Function-like non empty set
{{[i1,{}],<*D1,I1*>},{[i1,{}]}} is non empty set
i1 is V6() V7() V8() V12() ext-real Element of NAT
<*i1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
[6,<*i1*>,{}] is V21() V22() set
[6,<*i1*>] is V21() set
{6,<*i1*>} is non empty set
{6} is non empty set
{{6,<*i1*>},{6}} is non empty set
[[6,<*i1*>],{}] is V21() set
{[6,<*i1*>],{}} is non empty set
{[6,<*i1*>]} is Relation-like Function-like non empty set
{{[6,<*i1*>],{}},{[6,<*i1*>]}} is non empty set
i1 is V6() V7() V8() V12() ext-real Element of NAT
<*i1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
D1 is Element of SCM-Data-Loc
<*D1*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
[7,<*i1*>,<*D1*>] is V21() V22() set
[7,<*i1*>] is V21() set
{7,<*i1*>} is non empty set
{7} is non empty set
{{7,<*i1*>},{7}} is non empty set
[[7,<*i1*>],<*D1*>] is V21() set
{[7,<*i1*>],<*D1*>} is non empty set
{[7,<*i1*>]} is Relation-like Function-like non empty set
{{[7,<*i1*>],<*D1*>},{[7,<*i1*>]}} is non empty set
i1 is Element of SCM-Data-Loc
D1 is Element of the carrier of S
(S,i1,D1) is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of S -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ the carrier of S
SCM-Data-Loc \/ the carrier of S is non empty set
<*i1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
<*D1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
K75(<*i1*>,<*D1*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[5,{},(S,i1,D1)] is V21() V22() set
[5,{}] is V21() set
{5,{}} is non empty set
{5} is non empty set
{{5,{}},{5}} is non empty set
[[5,{}],(S,i1,D1)] is V21() set
{[5,{}],(S,i1,D1)} is non empty set
{[5,{}]} is Relation-like Function-like non empty set
{{[5,{}],(S,i1,D1)},{[5,{}]}} is non empty set
the non empty trivial V47() 1 -element right_complementable strict V92() V93() V94() V102() V103() V105() V107() V110() V111() doubleLoopStr is non empty trivial V47() 1 -element right_complementable strict V92() V93() V94() V102() V103() V105() V107() V110() V111() doubleLoopStr
S is non empty right_complementable V92() V93() V94() V103() V110() V111() doubleLoopStr
(S) is non empty non trivial set
the carrier of S is non empty set
{ [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 8, b<sub>2</sub>, b<sub>3</sub> is Element of SCM-Data-Loc : b<sub>1</sub> in {1,2,3,4} } ) \/ { [6,<*b<sub>1</sub>*>,{}] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b<sub>1</sub>*>,<*b<sub>2</sub>*>] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT , b<sub>2</sub> is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of S : verum } is non empty set
proj2 (S) is functional FinSequence-membered set
d1 is non empty set
d1 * is functional non empty FinSequence-membered set
[:NAT,(NAT *),(d1 *):] is set
[:NAT,(NAT *),(proj2 (S)):] is set
S is non empty right_complementable V92() V93() V94() V103() V110() V111() doubleLoopStr
(S) is Relation-like non empty non trivial standard-ins set
the carrier of S is non empty set
{ [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 8, b<sub>2</sub>, b<sub>3</sub> is Element of SCM-Data-Loc : b<sub>1</sub> in {1,2,3,4} } ) \/ { [6,<*b<sub>1</sub>*>,{}] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b<sub>1</sub>*>,<*b<sub>2</sub>*>] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT , b<sub>2</sub> is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of S : verum } is non empty set
d1 is Element of (S)
InsCode d1 is V6() V7() V8() V12() ext-real Element of InsCodes (S)
InsCodes (S) is non empty set
K51((S)) is set
proj1 (S) is non empty set
proj1 (proj1 (S)) is set
K41(d1) is set
K41(K41(d1)) is set
S is non empty 1-sorted
(S) is non empty non trivial set
the carrier of S is non empty set
{ [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 8, b<sub>2</sub>, b<sub>3</sub> is Element of SCM-Data-Loc : b<sub>1</sub> in {1,2,3,4} } ) \/ { [6,<*b<sub>1</sub>*>,{}] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b<sub>1</sub>*>,<*b<sub>2</sub>*>] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT , b<sub>2</sub> is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of S : verum } is non empty set
d1 is Element of (S)
d1 `1_3 is set
K41(d1) is set
K41(K41(d1)) is set
d1 `2_3 is set
K41(d1) `3_3 is set
i1 is Element of Segm 8
D1 is Element of SCM-Data-Loc
I1 is Element of SCM-Data-Loc
<*D1,I1*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
<*D1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
<*I1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,I1] is V21() set
{1,I1} is non empty set
{{1,I1},{1}} is non empty set
{[1,I1]} is Relation-like Function-like non empty set
K75(<*D1*>,<*I1*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[i1,{},<*D1,I1*>] is V21() V22() set
[i1,{}] is V21() set
{i1,{}} is non empty set
{i1} is non empty set
{{i1,{}},{i1}} is non empty set
[[i1,{}],<*D1,I1*>] is V21() set
{[i1,{}],<*D1,I1*>} is non empty set
{[i1,{}]} is Relation-like Function-like non empty set
{{[i1,{}],<*D1,I1*>},{[i1,{}]}} is non empty set
S is non empty 1-sorted
(S) is non empty non trivial set
the carrier of S is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set
d1 is Element of (S)
d1 `1_3 is set
K41(d1) is set
K41(K41(d1)) is set
d1 `2_3 is set
K41(d1) `3_3 is set
{ [5,{},(S,b<sub>1</sub>,b<sub>2</sub>)] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of S : verum } is set
i1 is Element of SCM-Data-Loc
D1 is Element of the carrier of S
(S,i1,D1) is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of S -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ the carrier of S
SCM-Data-Loc \/ the carrier of S is non empty set
<*i1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
<*D1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
K75(<*i1*>,<*D1*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[5,{},(S,i1,D1)] is V21() V22() set
[5,{}] is V21() set
{5,{}} is non empty set
{5} is non empty set
{{5,{}},{5}} is non empty set
[[5,{}],(S,i1,D1)] is V21() set
{[5,{}],(S,i1,D1)} is non empty set
{[5,{}]} is Relation-like Function-like non empty set
{{[5,{}],(S,i1,D1)},{[5,{}]}} is non empty set
S is non empty right_complementable V92() V93() V94() V103() V110() V111() doubleLoopStr
(S) is Relation-like non empty non trivial standard-ins set
the carrier of S is non empty set
{ [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 8, b<sub>2</sub>, b<sub>3</sub> is Element of SCM-Data-Loc : b<sub>1</sub> in {1,2,3,4} } ) \/ { [6,<*b<sub>1</sub>*>,{}] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b<sub>1</sub>*>,<*b<sub>2</sub>*>] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT , b<sub>2</sub> is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of S : verum } is non empty set
d1 is Element of (S)
InsCode d1 is V6() V7() V8() V12() ext-real Element of InsCodes (S)
InsCodes (S) is non empty set
K51((S)) is set
proj1 (S) is non empty set
proj1 (proj1 (S)) is set
K41(d1) is set
K41(K41(d1)) is set
d1 `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set
K41(d1) `3_3 is set
dom (d1 `2_3) is Element of bool NAT
i1 is V6() V7() V8() V12() ext-real Element of NAT
<*i1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
[6,<*i1*>,{}] is V21() V22() set
[6,<*i1*>] is V21() set
{6,<*i1*>} is non empty set
{6} is non empty set
{{6,<*i1*>},{6}} is non empty set
[[6,<*i1*>],{}] is V21() set
{[6,<*i1*>],{}} is non empty set
{[6,<*i1*>]} is Relation-like Function-like non empty set
{{[6,<*i1*>],{}},{[6,<*i1*>]}} is non empty set
S is non empty right_complementable V92() V93() V94() V103() V110() V111() doubleLoopStr
(S) is Relation-like non empty non trivial standard-ins set
the carrier of S is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set
d1 is Element of (S)
InsCode d1 is V6() V7() V8() V12() ext-real Element of InsCodes (S)
InsCodes (S) is non empty set
K51((S)) is set
proj1 (S) is non empty set
proj1 (proj1 (S)) is set
K41(d1) is set
K41(K41(d1)) is set
d1 `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set
K41(d1) `3_3 is set
dom (d1 `2_3) is Element of bool NAT
i1 is V6() V7() V8() V12() ext-real Element of NAT
<*i1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
D1 is Element of SCM-Data-Loc
<*D1*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
[7,<*i1*>,<*D1*>] is V21() V22() set
[7,<*i1*>] is V21() set
{7,<*i1*>} is non empty set
{7} is non empty set
{{7,<*i1*>},{7}} is non empty set
[[7,<*i1*>],<*D1*>] is V21() set
{[7,<*i1*>],<*D1*>} is non empty set
{[7,<*i1*>]} is Relation-like Function-like non empty set
{{[7,<*i1*>],<*D1*>},{[7,<*i1*>]}} is non empty set
S is non empty right_complementable V92() V93() V94() V103() V110() V111() doubleLoopStr
(S) is Relation-like non empty non trivial standard-ins set
the carrier of S is non empty set
{ [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 8, b<sub>2</sub>, b<sub>3</sub> is Element of SCM-Data-Loc : b<sub>1</sub> in {1,2,3,4} } ) \/ { [6,<*b<sub>1</sub>*>,{}] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b<sub>1</sub>*>,<*b<sub>2</sub>*>] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT , b<sub>2</sub> is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of S : verum } is non empty set
d1 is Element of (S)
InsCode d1 is V6() V7() V8() V12() ext-real Element of InsCodes (S)
InsCodes (S) is non empty set
K51((S)) is set
proj1 (S) is non empty set
proj1 (proj1 (S)) is set
K41(d1) is set
K41(K41(d1)) is set
i1 is Element of (S)
InsCode i1 is V6() V7() V8() V12() ext-real Element of InsCodes (S)
K41(i1) is set
K41(K41(i1)) is set
d1 `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set
K41(d1) `3_3 is set
dom (d1 `2_3) is Element of bool NAT
i1 `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set
K41(i1) `3_3 is set
dom (i1 `2_3) is Element of bool NAT
S is non empty right_complementable V92() V93() V94() V103() V110() V111() doubleLoopStr
(S) is Relation-like non empty non trivial standard-ins homogeneous set
the carrier of S is non empty set
{ [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 8, b<sub>2</sub>, b<sub>3</sub> is Element of SCM-Data-Loc : b<sub>1</sub> in {1,2,3,4} } ) \/ { [6,<*b<sub>1</sub>*>,{}] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b<sub>1</sub>*>,<*b<sub>2</sub>*>] where b<sub>1</sub> is V6() V7() V8() V12() ext-real Element of NAT , b<sub>2</sub> is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b<sub>1</sub>,b<sub>2</sub>*>] where b<sub>1</sub> is Element of SCM-Data-Loc , b<sub>2</sub> is Element of the carrier of S : verum } is non empty set
InsCodes (S) is non empty set
K51((S)) is set
proj1 (S) is non empty set
proj1 (proj1 (S)) is set
d1 is Element of InsCodes (S)
JumpParts d1 is functional non empty set
{ (b<sub>1</sub> `2_3) where b₁ is Element of (S) : InsCode b₁ = d1 } is set
i1 is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
proj1 i1 is set
D1 is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
proj1 D1 is set
I1 is set
[d1,i1,I1] is V21() V22() set
[d1,i1] is V21() set
{d1,i1} is non empty set
{d1} is non empty set
{{d1,i1},{d1}} is non empty set
[[d1,i1],I1] is V21() set
{[d1,i1],I1} is non empty set
{[d1,i1]} is Relation-like Function-like non empty set
{{[d1,i1],I1},{[d1,i1]}} is non empty set
[d1,D1,I1] is V21() V22() set
[d1,D1] is V21() set
{d1,D1} is non empty set
{{d1,D1},{d1}} is non empty set
[[d1,D1],I1] is V21() set
{[d1,D1],I1} is non empty set
{[d1,D1]} is Relation-like Function-like non empty set
{{[d1,D1],I1},{[d1,D1]}} is non empty set
D2 is Element of (S)
InsCode D2 is V6() V7() V8() V12() ext-real Element of InsCodes (S)
K41(D2) is set
K41(K41(D2)) is set
D2 `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set
K41(D2) `3_3 is set
D2 `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set
K41(D2) `3_3 is set
x is Element of Segm 8
i1 is Element of SCM-Data-Loc
a is Element of SCM-Data-Loc
<*i1,a*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
<*i1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
<*a*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,a] is V21() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like non empty set
K75(<*i1*>,<*a*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[x,{},<*i1,a*>] is V21() V22() set
[x,{}] is V21() set
{x,{}} is non empty set
{x} is non empty set
{{x,{}},{x}} is non empty set
[[x,{}],<*i1,a*>] is V21() set
{[x,{}],<*i1,a*>} is non empty set
{[x,{}]} is Relation-like Function-like non empty set
{{[x,{}],<*i1,a*>},{[x,{}]}} is non empty set
{ [5,{},(S,b₁,b₂)] where b₁ is Element of SCM-Data-Loc , b₂ is right_complementable Element of the carrier of S : verum } is set
D2 `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set
K41(D2) `3_3 is set
x is Element of SCM-Data-Loc
i1 is right_complementable Element of the carrier of S
(S,x,i1) is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of S -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ the carrier of S
SCM-Data-Loc \/ the carrier of S is non empty set
<*x*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,x] is V21() set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like non empty set
<*i1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
K75(<*x*>,<*i1*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[5,{},(S,x,i1)] is V21() V22() set
[5,{}] is V21() set
{5,{}} is non empty set
{5} is non empty set
{{5,{}},{5}} is non empty set
[[5,{}],(S,x,i1)] is V21() set
{[5,{}],(S,x,i1)} is non empty set
{[5,{}]} is Relation-like Function-like non empty set
{{[5,{}],(S,x,i1)},{[5,{}]}} is non empty set
x is Element of (S)
InsCode x is V6() V7() V8() V12() ext-real Element of InsCodes (S)
K41(x) is set
K41(K41(x)) is set
i1 is V6() V7() V8() V12() ext-real Element of NAT
<*i1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
[6,<*i1*>,{}] is V21() V22() set
[6,<*i1*>] is V21() set
{6,<*i1*>} is non empty set
{6} is non empty set
{{6,<*i1*>},{6}} is non empty set
[[6,<*i1*>],{}] is V21() set
{[6,<*i1*>],{}} is non empty set
{[6,<*i1*>]} is Relation-like Function-like non empty set
{{[6,<*i1*>],{}},{[6,<*i1*>]}} is non empty set
D1 . 1 is V6() V7() V8() V12() V39() V139() ext-real set
[d1,D1,{}] is V21() V22() set
[[d1,D1],{}] is V21() set
{[d1,D1],{}} is non empty set
{{[d1,D1],{}},{[d1,D1]}} is non empty set
a is V6() V7() V8() V12() ext-real Element of NAT
<*a*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,a] is V21() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like non empty set
[6,<*a*>,{}] is V21() V22() set
[6,<*a*>] is V21() set
{6,<*a*>} is non empty set
{{6,<*a*>},{6}} is non empty set
[[6,<*a*>],{}] is V21() set
{[6,<*a*>],{}} is non empty set
{[6,<*a*>]} is Relation-like Function-like non empty set
{{[6,<*a*>],{}},{[6,<*a*>]}} is non empty set
I is Element of (S)
I `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set
K41(I) is set
K41(I) `3_3 is set
x is Element of (S)
InsCode x is V6() V7() V8() V12() ext-real Element of InsCodes (S)
K41(x) is set
K41(K41(x)) is set
i1 is V6() V7() V8() V12() ext-real Element of NAT
<*i1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
a is Element of SCM-Data-Loc
<*a*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,a] is V21() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like non empty set
[7,<*i1*>,<*a*>] is V21() V22() set
[7,<*i1*>] is V21() set
{7,<*i1*>} is non empty set
{7} is non empty set
{{7,<*i1*>},{7}} is non empty set
[[7,<*i1*>],<*a*>] is V21() set
{[7,<*i1*>],<*a*>} is non empty set
{[7,<*i1*>]} is Relation-like Function-like non empty set
{{[7,<*i1*>],<*a*>},{[7,<*i1*>]}} is non empty set
D1 . 1 is V6() V7() V8() V12() V39() V139() ext-real set
l is V6() V7() V8() V12() ext-real Element of NAT
<*l*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,l] is V21() set
{1,l} is non empty set
{{1,l},{1}} is non empty set
{[1,l]} is Relation-like Function-like non empty set
[d1,<*l*>,<*a*>] is V21() V22() set
[d1,<*l*>] is V21() set
{d1,<*l*>} is non empty set
{{d1,<*l*>},{d1}} is non empty set
[[d1,<*l*>],<*a*>] is V21() set
{[d1,<*l*>],<*a*>} is non empty set
{[d1,<*l*>]} is Relation-like Function-like non empty set
{{[d1,<*l*>],<*a*>},{[d1,<*l*>]}} is non empty set
[d1,D1,I1] `1_3 is set
K41([d1,D1,I1]) is set
K41(K41([d1,D1,I1])) is set
[([d1,D1,I1] `1_3),<*l*>,<*a*>] is V21() V22() set
[([d1,D1,I1] `1_3),<*l*>] is V21() set
{([d1,D1,I1] `1_3),<*l*>} is non empty set
{([d1,D1,I1] `1_3)} is non empty set
{{([d1,D1,I1] `1_3),<*l*>},{([d1,D1,I1] `1_3)}} is non empty set
[[([d1,D1,I1] `1_3),<*l*>],<*a*>] is V21() set
{[([d1,D1,I1] `1_3),<*l*>],<*a*>} is non empty set
{[([d1,D1,I1] `1_3),<*l*>]} is Relation-like Function-like non empty set
{{[([d1,D1,I1] `1_3),<*l*>],<*a*>},{[([d1,D1,I1] `1_3),<*l*>]}} is non empty set
{ [5,{},(S,b₁,b₂)] where b₁ is Element of SCM-Data-Loc , b₂ is right_complementable Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},(S,b₁,b₂)] where b₁ is Element of SCM-Data-Loc , b₂ is right_complementable Element of the carrier of S : verum } is non empty set
I is Element of (S)
InsCode I is V6() V7() V8() V12() ext-real Element of InsCodes (S)
K41(I) is set
K41(K41(I)) is set
i2 is V6() V7() V8() V12() ext-real Element of NAT
<*i2*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,i2] is V21() set
{1,i2} is non empty set
{{1,i2},{1}} is non empty set
{[1,i2]} is Relation-like Function-like non empty set
b is Element of SCM-Data-Loc
<*b*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,b] is V21() set
{1,b} is non empty set
{{1,b},{1}} is non empty set
{[1,b]} is Relation-like Function-like non empty set
[7,<*i2*>,<*b*>] is V21() V22() set
[7,<*i2*>] is V21() set
{7,<*i2*>} is non empty set
{{7,<*i2*>},{7}} is non empty set
[[7,<*i2*>],<*b*>] is V21() set
{[7,<*i2*>],<*b*>} is non empty set
{[7,<*i2*>]} is Relation-like Function-like non empty set
{{[7,<*i2*>],<*b*>},{[7,<*i2*>]}} is non empty set
[d1,<*i2*>,<*b*>] is V21() V22() set
[d1,<*i2*>] is V21() set
{d1,<*i2*>} is non empty set
{{d1,<*i2*>},{d1}} is non empty set
[[d1,<*i2*>],<*b*>] is V21() set
{[d1,<*i2*>],<*b*>} is non empty set
{[d1,<*i2*>]} is Relation-like Function-like non empty set
{{[d1,<*i2*>],<*b*>},{[d1,<*i2*>]}} is non empty set
S is non empty 1-sorted
(S) is non empty non trivial set
the carrier of S is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set
d1 is set
i1 is Element of SCM-Data-Loc
D1 is Element of SCM-Data-Loc
<*i1,D1*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
<*i1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
<*D1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
K75(<*i1*>,<*D1*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[d1,{},<*i1,D1*>] is V21() V22() set
[d1,{}] is V21() set
{d1,{}} is non empty set
{d1} is non empty set
{{d1,{}},{d1}} is non empty set
[[d1,{}],<*i1,D1*>] is V21() set
{[d1,{}],<*i1,D1*>} is non empty set
{[d1,{}]} is Relation-like Function-like non empty set
{{[d1,{}],<*i1,D1*>},{[d1,{}]}} is non empty set
x is Element of Segm 8
I1 is Element of SCM-Data-Loc
D2 is Element of SCM-Data-Loc
<*I1,D2*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
<*I1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,I1] is V21() set
{1,I1} is non empty set
{{1,I1},{1}} is non empty set
{[1,I1]} is Relation-like Function-like non empty set
<*D2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,D2] is V21() set
{1,D2} is non empty set
{{1,D2},{1}} is non empty set
{[1,D2]} is Relation-like Function-like non empty set
K75(<*I1*>,<*D2*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[x,{},<*I1,D2*>] is V21() V22() set
[x,{}] is V21() set
{x,{}} is non empty set
{x} is non empty set
{{x,{}},{x}} is non empty set
[[x,{}],<*I1,D2*>] is V21() set
{[x,{}],<*I1,D2*>} is non empty set
{[x,{}]} is Relation-like Function-like non empty set
{{[x,{}],<*I1,D2*>},{[x,{}]}} is non empty set
S is non empty 1-sorted
the carrier of S is non empty set
(S) is non empty non trivial set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set
d1 is Element of the carrier of S
i1 is Element of SCM-Data-Loc
(S,i1,d1) is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of S -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ the carrier of S
SCM-Data-Loc \/ the carrier of S is non empty set
<*i1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
<*d1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,d1] is V21() set
{1,d1} is non empty set
{{1,d1},{1}} is non empty set
{[1,d1]} is Relation-like Function-like non empty set
K75(<*i1*>,<*d1*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[5,{},(S,i1,d1)] is V21() V22() set
[5,{}] is V21() set
{5,{}} is non empty set
{5} is non empty set
{{5,{}},{5}} is non empty set
[[5,{}],(S,i1,d1)] is V21() set
{[5,{}],(S,i1,d1)} is non empty set
{[5,{}]} is Relation-like Function-like non empty set
{{[5,{}],(S,i1,d1)},{[5,{}]}} is non empty set
D1 is Element of SCM-Data-Loc
(S,D1,d1) is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of S -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ the carrier of S
<*D1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
K75(<*D1*>,<*d1*>) is Relation-like NAT -defined Function-like non empty V24() K313(1,1) -element FinSequence-like FinSubsequence-like set
[5,{},(S,D1,d1)] is V21() V22() set
[[5,{}],(S,D1,d1)] is V21() set
{[5,{}],(S,D1,d1)} is non empty set
{{[5,{}],(S,D1,d1)},{[5,{}]}} is non empty set
{ [5,{},(S,b₁,b₂)] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
S is non empty 1-sorted
(S) is non empty non trivial set
the carrier of S is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set
d1 is V6() V7() V8() V12() ext-real Element of NAT
<*d1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,d1] is V21() set
{1,d1} is non empty set
{{1,d1},{1}} is non empty set
{[1,d1]} is Relation-like Function-like non empty set
[6,<*d1*>,{}] is V21() V22() set
[6,<*d1*>] is V21() set
{6,<*d1*>} is non empty set
{6} is non empty set
{{6,<*d1*>},{6}} is non empty set
[[6,<*d1*>],{}] is V21() set
{[6,<*d1*>],{}} is non empty set
{[6,<*d1*>]} is Relation-like Function-like non empty set
{{[6,<*d1*>],{}},{[6,<*d1*>]}} is non empty set
i1 is V6() V7() V8() V12() ext-real Element of NAT
<*i1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
[6,<*i1*>,{}] is V21() V22() set
[6,<*i1*>] is V21() set
{6,<*i1*>} is non empty set
{{6,<*i1*>},{6}} is non empty set
[[6,<*i1*>],{}] is V21() set
{[6,<*i1*>],{}} is non empty set
{[6,<*i1*>]} is Relation-like Function-like non empty set
{{[6,<*i1*>],{}},{[6,<*i1*>]}} is non empty set
S is non empty 1-sorted
(S) is non empty non trivial set
the carrier of S is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set
d1 is Element of SCM-Data-Loc
<*d1*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,d1] is V21() set
{1,d1} is non empty set
{{1,d1},{1}} is non empty set
{[1,d1]} is Relation-like Function-like non empty set
i1 is V6() V7() V8() V12() ext-real Element of NAT
<*i1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,i1] is V21() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is Relation-like Function-like non empty set
[7,<*i1*>,<*d1*>] is V21() V22() set
[7,<*i1*>] is V21() set
{7,<*i1*>} is non empty set
{7} is non empty set
{{7,<*i1*>},{7}} is non empty set
[[7,<*i1*>],<*d1*>] is V21() set
{[7,<*i1*>],<*d1*>} is non empty set
{[7,<*i1*>]} is Relation-like Function-like non empty set
{{[7,<*i1*>],<*d1*>},{[7,<*i1*>]}} is non empty set
I1 is V6() V7() V8() V12() ext-real Element of NAT
<*I1*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
[1,I1] is V21() set
{1,I1} is non empty set
{{1,I1},{1}} is non empty set
{[1,I1]} is Relation-like Function-like non empty set
D1 is Element of SCM-Data-Loc
<*D1*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,D1] is V21() set
{1,D1} is non empty set
{{1,D1},{1}} is non empty set
{[1,D1]} is Relation-like Function-like non empty set
[7,<*I1*>,<*D1*>] is V21() V22() set
[7,<*I1*>] is V21() set
{7,<*I1*>} is non empty set
{{7,<*I1*>},{7}} is non empty set
[[7,<*I1*>],<*D1*>] is V21() set
{[7,<*I1*>],<*D1*>} is non empty set
{[7,<*I1*>]} is Relation-like Function-like non empty set
{{[7,<*I1*>],<*D1*>},{[7,<*I1*>]}} is non empty set
S is non empty 1-sorted
(S) is non empty non trivial set
the carrier of S is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is set
((({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() ext-real Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() ext-real Element of NAT , b₂ is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of SCM-Data-Loc , b₂ is Element of the carrier of S : verum } is non empty set