:: SCMPDS_I semantic presentation

REAL is non empty V24() 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
9 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT
Segm 9 is non empty Element of bool NAT
SCM-Data-Loc is non empty set
K158() is set
bool K158() is set
2 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT
[:K158(),2:] is Relation-like set
bool [:K158(),2:] is set
K160() is Relation-like Function-like V36(K158(),2) Element of bool [:K158(),2:]
K161() is Relation-like 2 -defined Function-like total set
K160() * K161() is Relation-like Function-like set
K133((K160() * K161())) is set
SCM-Instr is Relation-like non empty standard-ins homogeneous J/A-independent with_halt set
K120(K133((K160() * K161())),K133((K160() * K161()))) is set
[:SCM-Instr,K120(K133((K160() * K161())),K133((K160() * K161()))):] is Relation-like set
bool [:SCM-Instr,K120(K133((K160() * K161())),K133((K160() * K161()))):] is set
RAT is non empty V24() set
INT is non empty V24() set
1 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT
3 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT
4 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT
5 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT
Seg 1 is non empty V24() 1 -element Element of bool NAT
{ b1 where b1 is V6() V7() V8() V12() V44() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty set
Seg 2 is non empty V24() 2 -element Element of bool NAT
{ b1 where b1 is V6() V7() V8() V12() V44() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty 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 V44() integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued set
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 V44() integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued Element of NAT
K180(NAT,0) is functional non empty Element of bool NAT
14 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT
6 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT
7 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT
8 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT
10 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT
11 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT
12 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT
13 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT
15 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT
Segm 15 is non empty Element of bool NAT
SCM-Data-Loc \/ INT is non empty set
T is V44() integer 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
{ [14,{},<*b1*>] where b1 is V44() integer Element of INT : verum } is set
{[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V44() integer Element of INT : verum } is non empty set
{ [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } is set
({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V44() integer Element of INT : verum } ) \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } is non empty set
{2,3} is non empty set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3 is V44() integer Element of INT : b1 in {2,3} } is set
(({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V44() integer 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 V44() integer Element of INT : b1 in {2,3} } is non empty set
{4,5,6,7,8} is set
{ [b1,{},<*b2,b3,b4*>] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3, b4 is V44() integer Element of INT : b1 in {4,5,6,7,8} } is set
((({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V44() integer 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 V44() integer 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 V44() integer Element of INT : b1 in {4,5,6,7,8} } is non empty set
{9,10,11,12,13} 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 V44() integer Element of INT : b1 in {9,10,11,12,13} } is set
(((({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V44() integer 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 V44() integer 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 V44() integer 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 SCM-Data-Loc , b4, b5 is V44() integer Element of INT : b1 in {9,10,11,12,13} } is non empty set
() is set
<*0*> 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,0] is V21() set
{1,0} is non empty set
{{1,0},{1}} is non empty set
{[1,0]} is Relation-like Function-like non empty set
[14,{},<*0*>] is V21() V22() set
[14,{}] is V21() set
{14,{}} is non empty set
{14} is non empty set
{{14,{}},{14}} is non empty set
[[14,{}],<*0*>] is V21() set
{[14,{}],<*0*>} is non empty set
{[14,{}]} is Relation-like Function-like non empty set
{{[14,{}],<*0*>},{[14,{}]}} is non empty set
T is Element of SCM-Data-Loc
f1 is V44() integer set
<*T,f1*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like set
<*T*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,T] is V21() set
{1,T} is non empty set
{{1,T},{1}} is non empty set
{[1,T]} is Relation-like Function-like non empty set
<*f1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f1] is V21() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is Relation-like Function-like non empty set
K75(<*T*>,<*f1*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set
K210(1,1) is V6() V7() V8() V12() V44() integer ext-real Element of NAT
f2 is set
proj2 <*T,f1*> is non empty set
dom <*T,f1*> is non empty Element of bool NAT
p is set
<*T,f1*> . p is set
T is Element of ()
f2 is Element of Segm 15
f1 is Element of SCM-Data-Loc
<*f1*> 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,f1] is V21() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is Relation-like Function-like non empty set
[f2,{},<*f1*>] is V21() V22() set
[f2,{}] is V21() set
{f2,{}} is non empty set
{f2} is non empty set
{{f2,{}},{f2}} is non empty set
[[f2,{}],<*f1*>] is V21() set
{[f2,{}],<*f1*>} is non empty set
{[f2,{}]} is Relation-like Function-like non empty set
{{[f2,{}],<*f1*>},{[f2,{}]}} is non empty set
T `3_3 is set
<*f1*> /. 1 is Element of SCM-Data-Loc
c1 is Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
p is Element of SCM-Data-Loc
c1 /. 1 is Element of SCM-Data-Loc
c2 is Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
i is Element of SCM-Data-Loc
c2 /. 1 is Element of SCM-Data-Loc
T is Element of Segm 15
f1 is Element of ()
(f1) is Element of SCM-Data-Loc
f2 is Element of SCM-Data-Loc
<*f2*> 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,f2] is V21() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is Relation-like Function-like non empty set
[T,{},<*f2*>] is V21() V22() set
[T,{}] is V21() set
{T,{}} is non empty set
{T} is non empty set
{{T,{}},{T}} is non empty set
[[T,{}],<*f2*>] is V21() set
{[T,{}],<*f2*>} is non empty set
{[T,{}]} is Relation-like Function-like non empty set
{{[T,{}],<*f2*>},{[T,{}]}} is non empty set
f1 `3_3 is set
p is Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
p /. 1 is Element of SCM-Data-Loc
T is Element of ()
f2 is Element of Segm 15
f1 is V44() integer set
<*f1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f1] is V21() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is Relation-like Function-like non empty set
[f2,{},<*f1*>] is V21() V22() set
[f2,{}] is V21() set
{f2,{}} is non empty set
{f2} is non empty set
{{f2,{}},{f2}} is non empty set
[[f2,{}],<*f1*>] is V21() set
{[f2,{}],<*f1*>} is non empty set
{[f2,{}]} is Relation-like Function-like non empty set
{{[f2,{}],<*f1*>},{[f2,{}]}} is non empty set
T `3_3 is set
p is V44() integer Element of INT
<*p*> is Relation-like NAT -defined INT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
[1,p] is V21() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is Relation-like Function-like non empty set
<*p*> /. 1 is V44() integer Element of INT
c1 is Relation-like NAT -defined INT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
p is V44() integer set
c1 /. 1 is V44() integer Element of INT
c2 is Relation-like NAT -defined INT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
i is V44() integer set
c2 /. 1 is V44() integer Element of INT
T is Element of Segm 15
f1 is Element of ()
(f1) is V44() integer set
f2 is V44() integer set
<*f2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V21() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is Relation-like Function-like non empty set
[T,{},<*f2*>] is V21() V22() set
[T,{}] is V21() set
{T,{}} is non empty set
{T} is non empty set
{{T,{}},{T}} is non empty set
[[T,{}],<*f2*>] is V21() set
{[T,{}],<*f2*>} is non empty set
{[T,{}]} is Relation-like Function-like non empty set
{{[T,{}],<*f2*>},{[T,{}]}} is non empty set
f1 `3_3 is set
p is Relation-like NAT -defined INT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
p /. 1 is V44() integer Element of INT
T is Element of ()
p is Element of Segm 15
f1 is Element of SCM-Data-Loc
f2 is V44() integer set
(f1,f2) is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
<*f1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f1] is V21() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is Relation-like Function-like non empty set
<*f2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V21() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is Relation-like Function-like non empty set
K75(<*f1*>,<*f2*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set
[p,{},(f1,f2)] is V21() V22() set
[p,{}] is V21() set
{p,{}} is non empty set
{p} is non empty set
{{p,{}},{p}} is non empty set
[[p,{}],(f1,f2)] is V21() set
{[p,{}],(f1,f2)} is non empty set
{[p,{}]} is Relation-like Function-like non empty set
{{[p,{}],(f1,f2)},{[p,{}]}} is non empty set
T `3_3 is set
(f1,f2) /. 1 is Element of SCM-Data-Loc \/ INT
c2 is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
i is Element of SCM-Data-Loc
c2 /. 1 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
c1 is Element of SCM-Data-Loc
f /. 1 is Element of SCM-Data-Loc \/ INT
(f1,f2) /. 2 is Element of SCM-Data-Loc \/ INT
c2 is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
i is V44() integer set
c2 /. 2 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
c1 is V44() integer set
f /. 2 is Element of SCM-Data-Loc \/ INT
T is Element of Segm 15
f1 is Element of ()
(f1) is Element of SCM-Data-Loc
(f1) is V44() integer set
f2 is Element of SCM-Data-Loc
p is V44() integer set
(f2,p) is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
<*f2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V21() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is Relation-like Function-like non empty set
<*p*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V21() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is Relation-like Function-like non empty set
K75(<*f2*>,<*p*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set
[T,{},(f2,p)] is V21() V22() set
[T,{}] is V21() set
{T,{}} is non empty set
{T} is non empty set
{{T,{}},{T}} is non empty set
[[T,{}],(f2,p)] is V21() set
{[T,{}],(f2,p)} is non empty set
{[T,{}]} is Relation-like Function-like non empty set
{{[T,{}],(f2,p)},{[T,{}]}} is non empty set
f1 `3_3 is set
i is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
i /. 1 is Element of SCM-Data-Loc \/ INT
c1 is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
c1 /. 2 is Element of SCM-Data-Loc \/ INT
T is Element of ()
i is Element of Segm 15
f1 is Element of SCM-Data-Loc
f2 is V44() integer set
p is V44() integer set
<*f1,f2,p*> is Relation-like NAT -defined Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like set
<*f1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f1] is V21() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is Relation-like Function-like non empty set
<*f2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V21() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is Relation-like Function-like non empty set
K75(<*f1*>,<*f2*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set
<*p*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V21() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is Relation-like Function-like non empty set
K75(K75(<*f1*>,<*f2*>),<*p*>) is Relation-like NAT -defined Function-like non empty V24() K210(K210(1,1),1) -element FinSequence-like FinSubsequence-like set
K210(K210(1,1),1) is V6() V7() V8() V12() V44() integer ext-real Element of NAT
[i,{},<*f1,f2,p*>] is V21() V22() set
[i,{}] is V21() set
{i,{}} is non empty set
{i} is non empty set
{{i,{}},{i}} is non empty set
[[i,{}],<*f1,f2,p*>] is V21() set
{[i,{}],<*f1,f2,p*>} is non empty set
{[i,{}]} is Relation-like Function-like non empty set
{{[i,{}],<*f1,f2,p*>},{[i,{}]}} is non empty set
T `3_3 is set
c1 is Element of SCM-Data-Loc \/ INT
c2 is Element of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc \/ INT
<*c1,c2,f*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
<*c1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c1] is V21() set
{1,c1} is non empty set
{{1,c1},{1}} is non empty set
{[1,c1]} is Relation-like Function-like non empty set
<*c2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c2] is V21() set
{1,c2} is non empty set
{{1,c2},{1}} is non empty set
{[1,c2]} is Relation-like Function-like non empty set
K75(<*c1*>,<*c2*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set
<*f*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f] is V21() set
{1,f} is non empty set
{{1,f},{1}} is non empty set
{[1,f]} is Relation-like Function-like non empty set
K75(K75(<*c1*>,<*c2*>),<*f*>) is Relation-like NAT -defined Function-like non empty V24() K210(K210(1,1),1) -element FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f /. 1 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
c1 is Element of SCM-Data-Loc
f /. 1 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
c2 is Element of SCM-Data-Loc
f /. 1 is Element of SCM-Data-Loc \/ INT
c1 is Element of SCM-Data-Loc \/ INT
c2 is Element of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc \/ INT
<*c1,c2,f*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
<*c1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c1] is V21() set
{1,c1} is non empty set
{{1,c1},{1}} is non empty set
{[1,c1]} is Relation-like Function-like non empty set
<*c2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c2] is V21() set
{1,c2} is non empty set
{{1,c2},{1}} is non empty set
{[1,c2]} is Relation-like Function-like non empty set
K75(<*c1*>,<*c2*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set
<*f*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f] is V21() set
{1,f} is non empty set
{{1,f},{1}} is non empty set
{[1,f]} is Relation-like Function-like non empty set
K75(K75(<*c1*>,<*c2*>),<*f*>) is Relation-like NAT -defined Function-like non empty V24() K210(K210(1,1),1) -element FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f /. 2 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
c1 is V44() integer set
f /. 2 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
c2 is V44() integer set
f /. 2 is Element of SCM-Data-Loc \/ INT
c1 is Element of SCM-Data-Loc \/ INT
c2 is Element of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc \/ INT
<*c1,c2,f*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
<*c1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c1] is V21() set
{1,c1} is non empty set
{{1,c1},{1}} is non empty set
{[1,c1]} is Relation-like Function-like non empty set
<*c2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c2] is V21() set
{1,c2} is non empty set
{{1,c2},{1}} is non empty set
{[1,c2]} is Relation-like Function-like non empty set
K75(<*c1*>,<*c2*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set
<*f*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f] is V21() set
{1,f} is non empty set
{{1,f},{1}} is non empty set
{[1,f]} is Relation-like Function-like non empty set
K75(K75(<*c1*>,<*c2*>),<*f*>) is Relation-like NAT -defined Function-like non empty V24() K210(K210(1,1),1) -element FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f /. 3 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
c1 is V44() integer set
f /. 3 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
c2 is V44() integer set
f /. 3 is Element of SCM-Data-Loc \/ INT
T is Element of Segm 15
f1 is Element of ()
(f1) is Element of SCM-Data-Loc
(f1) is V44() integer set
(f1) is V44() integer set
f2 is Element of SCM-Data-Loc
p is V44() integer set
i is V44() integer set
<*f2,p,i*> is Relation-like NAT -defined Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like set
<*f2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V21() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is Relation-like Function-like non empty set
<*p*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V21() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is Relation-like Function-like non empty set
K75(<*f2*>,<*p*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set
<*i*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,i] is V21() set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like non empty set
K75(K75(<*f2*>,<*p*>),<*i*>) is Relation-like NAT -defined Function-like non empty V24() K210(K210(1,1),1) -element FinSequence-like FinSubsequence-like set
[T,{},<*f2,p,i*>] is V21() V22() set
[T,{}] is V21() set
{T,{}} is non empty set
{T} is non empty set
{{T,{}},{T}} is non empty set
[[T,{}],<*f2,p,i*>] is V21() set
{[T,{}],<*f2,p,i*>} is non empty set
{[T,{}]} is Relation-like Function-like non empty set
{{[T,{}],<*f2,p,i*>},{[T,{}]}} is non empty set
f1 `3_3 is set
c1 is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
c1 /. 1 is Element of SCM-Data-Loc \/ INT
c2 is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
c2 /. 2 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f /. 3 is Element of SCM-Data-Loc \/ INT
T is Element of ()
c1 is Element of Segm 15
f1 is Element of SCM-Data-Loc
f2 is Element of SCM-Data-Loc
p is V44() integer set
i is V44() integer set
<*f1,f2,p,i*> is Relation-like NAT -defined Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like set
[c1,{},<*f1,f2,p,i*>] is V21() V22() set
[c1,{}] is V21() set
{c1,{}} is non empty set
{c1} is non empty set
{{c1,{}},{c1}} is non empty set
[[c1,{}],<*f1,f2,p,i*>] is V21() set
{[c1,{}],<*f1,f2,p,i*>} is non empty set
{[c1,{}]} is Relation-like Function-like non empty set
{{[c1,{}],<*f1,f2,p,i*>},{[c1,{}]}} is non empty set
T `3_3 is set
c2 is Element of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc \/ INT
<*c2,f,f,f*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f /. 1 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
c2 is Element of SCM-Data-Loc
f /. 1 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc
f /. 1 is Element of SCM-Data-Loc \/ INT
c2 is Element of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc \/ INT
<*c2,f,f,f*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f /. 2 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
c2 is Element of SCM-Data-Loc
f /. 2 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc
f /. 2 is Element of SCM-Data-Loc \/ INT
c2 is Element of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc \/ INT
<*c2,f,f,f*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f /. 3 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
c2 is V44() integer set
f /. 3 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f is V44() integer set
f /. 3 is Element of SCM-Data-Loc \/ INT
c2 is Element of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc \/ INT
f is Element of SCM-Data-Loc \/ INT
<*c2,f,f,f*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f /. 4 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
c2 is V44() integer set
f /. 4 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f is V44() integer set
f /. 4 is Element of SCM-Data-Loc \/ INT
T is Element of Segm 15
f1 is Element of ()
(f1) is Element of SCM-Data-Loc
(f1) is Element of SCM-Data-Loc
(f1) is V44() integer set
(f1) is V44() integer set
f2 is Element of SCM-Data-Loc
p is Element of SCM-Data-Loc
i is V44() integer set
c1 is V44() integer set
<*f2,p,i,c1*> is Relation-like NAT -defined Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like set
[T,{},<*f2,p,i,c1*>] is V21() V22() set
[T,{}] is V21() set
{T,{}} is non empty set
{T} is non empty set
{{T,{}},{T}} is non empty set
[[T,{}],<*f2,p,i,c1*>] is V21() set
{[T,{}],<*f2,p,i,c1*>} is non empty set
{[T,{}]} is Relation-like Function-like non empty set
{{[T,{}],<*f2,p,i,c1*>},{[T,{}]}} is non empty set
f1 `3_3 is set
c2 is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
c2 /. 1 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f /. 2 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f /. 3 is Element of SCM-Data-Loc \/ INT
f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
f /. 4 is Element of SCM-Data-Loc \/ INT
() is V6() V7() V8() V12() V44() integer ext-real Element of NAT
() is V6() V7() V8() V12() V44() integer ext-real Element of NAT
{ [b1,{},(b2,b3)] where b1 is Element of Segm 15, b2 is Element of SCM-Data-Loc , b3 is V44() integer Element of INT : b1 in {2,3} } is set
T is Element of ()
T `1_3 is set
K41(T) is set
K41(K41(T)) is set
(({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V44() integer 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 V44() integer Element of INT : b1 in {2,3} } is non empty set
((({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V44() integer 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 V44() integer 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 V44() integer Element of INT : b1 in {4,5,6,7,8} } is non empty set
f1 is V44() integer Element of INT
<*f1*> is Relation-like NAT -defined INT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
[1,f1] is V21() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is Relation-like Function-like non empty set
[14,{},<*f1*>] is V21() V22() set
[[14,{}],<*f1*>] is V21() set
{[14,{}],<*f1*>} is non empty set
{{[14,{}],<*f1*>},{[14,{}]}} is non empty set
f1 is Element of SCM-Data-Loc
<*f1*> 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,f1] is V21() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is Relation-like Function-like non empty set
[1,{},<*f1*>] is V21() V22() set
[1,{}] is V21() set
{1,{}} is non empty set
{{1,{}},{1}} is non empty set
[[1,{}],<*f1*>] is V21() set
{[1,{}],<*f1*>} is non empty set
{[1,{}]} is Relation-like Function-like non empty set
{{[1,{}],<*f1*>},{[1,{}]}} is non empty set
f1 is Element of Segm 15
f2 is Element of SCM-Data-Loc
p is V44() integer Element of INT
(f2,p) is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
<*f2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V21() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is Relation-like Function-like non empty set
<*p*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V21() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is Relation-like Function-like non empty set
K75(<*f2*>,<*p*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set
[f1,{},(f2,p)] is V21() V22() set
[f1,{}] is V21() set
{f1,{}} is non empty set
{f1} is non empty set
{{f1,{}},{f1}} is non empty set
[[f1,{}],(f2,p)] is V21() set
{[f1,{}],(f2,p)} is non empty set
{[f1,{}]} is Relation-like Function-like non empty set
{{[f1,{}],(f2,p)},{[f1,{}]}} is non empty set
f1 is Element of Segm 15
f2 is Element of SCM-Data-Loc
p is V44() integer Element of INT
i is V44() integer Element of INT
<*f2,p,i*> is Relation-like NAT -defined Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like set
<*f2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V21() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is Relation-like Function-like non empty set
<*p*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V21() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is Relation-like Function-like non empty set
K75(<*f2*>,<*p*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set
<*i*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,i] is V21() set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like non empty set
K75(K75(<*f2*>,<*p*>),<*i*>) is Relation-like NAT -defined Function-like non empty V24() K210(K210(1,1),1) -element FinSequence-like FinSubsequence-like set
[f1,{},<*f2,p,i*>] is V21() V22() set
[f1,{}] is V21() set
{f1,{}} is non empty set
{f1} is non empty set
{{f1,{}},{f1}} is non empty set
[[f1,{}],<*f2,p,i*>] is V21() set
{[f1,{}],<*f2,p,i*>} is non empty set
{[f1,{}]} is Relation-like Function-like non empty set
{{[f1,{}],<*f2,p,i*>},{[f1,{}]}} is non empty set
f1 is Element of Segm 15
f2 is Element of SCM-Data-Loc
p is Element of SCM-Data-Loc
i is V44() integer Element of INT
c1 is V44() integer Element of INT
<*f2,p,i,c1*> is Relation-like NAT -defined Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like set
[f1,{},<*f2,p,i,c1*>] is V21() V22() set
[f1,{}] is V21() set
{f1,{}} is non empty set
{f1} is non empty set
{{f1,{}},{f1}} is non empty set
[[f1,{}],<*f2,p,i,c1*>] is V21() set
{[f1,{}],<*f2,p,i,c1*>} is non empty set
{[f1,{}]} is Relation-like Function-like non empty set
{{[f1,{}],<*f2,p,i,c1*>},{[f1,{}]}} is non empty set
proj2 () is set
T is set
f1 is set
[f1,T] is V21() set
{f1,T} is non empty set
{f1} is non empty set
{{f1,T},{f1}} is non empty set
(({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V44() integer 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 V44() integer Element of INT : b1 in {2,3} } is non empty set
((({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V44() integer 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 V44() integer 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 V44() integer Element of INT : b1 in {4,5,6,7,8} } is non empty set
{ [14,{},<*b1*>] where b1 is V44() integer Element of INT : verum } \/ { [1,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } is set
{[0,{},{}]} \/ ( { [14,{},<*b1*>] where b1 is V44() integer 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 V44() integer 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 V44() integer Element of INT : b1 in {2,3} } is non empty set
p is V44() integer Element of INT
<*p*> is Relation-like NAT -defined INT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
[1,p] is V21() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is Relation-like Function-like non empty set
[14,{},<*p*>] is V21() V22() set
[[14,{}],<*p*>] is V21() set
{[14,{}],<*p*>} is non empty set
{{[14,{}],<*p*>},{[14,{}]}} is non empty set
p is Element of SCM-Data-Loc
<*p*> 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,p] is V21() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is Relation-like Function-like non empty set
[1,{},<*p*>] is V21() V22() set
[1,{}] is V21() set
{1,{}} is non empty set
{{1,{}},{1}} is non empty set
[[1,{}],<*p*>] is V21() set
{[1,{}],<*p*>} is non empty set
{[1,{}]} is Relation-like Function-like non empty set
{{[1,{}],<*p*>},{[1,{}]}} is non empty set
p is Element of Segm 15
i is Element of SCM-Data-Loc
c1 is V44() integer Element of INT
(i,c1) is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
<*i*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,i] is V21() set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like non empty set
<*c1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c1] is V21() set
{1,c1} is non empty set
{{1,c1},{1}} is non empty set
{[1,c1]} is Relation-like Function-like non empty set
K75(<*i*>,<*c1*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set
[p,{},(i,c1)] is V21() V22() set
[p,{}] is V21() set
{p,{}} is non empty set
{p} is non empty set
{{p,{}},{p}} is non empty set
[[p,{}],(i,c1)] is V21() set
{[p,{}],(i,c1)} is non empty set
{[p,{}]} is Relation-like Function-like non empty set
{{[p,{}],(i,c1)},{[p,{}]}} is non empty set
p is Element of Segm 15
i is Element of SCM-Data-Loc
c1 is V44() integer Element of INT
c2 is V44() integer Element of INT
<*i,c1,c2*> is Relation-like NAT -defined Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like set
<*i*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,i] is V21() set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like non empty set
<*c1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c1] is V21() set
{1,c1} is non empty set
{{1,c1},{1}} is non empty set
{[1,c1]} is Relation-like Function-like non empty set
K75(<*i*>,<*c1*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set
<*c2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c2] is V21() set
{1,c2} is non empty set
{{1,c2},{1}} is non empty set
{[1,c2]} is Relation-like Function-like non empty set
K75(K75(<*i*>,<*c1*>),<*c2*>) is Relation-like NAT -defined Function-like non empty V24() K210(K210(1,1),1) -element FinSequence-like FinSubsequence-like set
[p,{},<*i,c1,c2*>] is V21() V22() set
[p,{}] is V21() set
{p,{}} is non empty set
{p} is non empty set
{{p,{}},{p}} is non empty set
[[p,{}],<*i,c1,c2*>] is V21() set
{[p,{}],<*i,c1,c2*>} is non empty set
{[p,{}]} is Relation-like Function-like non empty set
{{[p,{}],<*i,c1,c2*>},{[p,{}]}} is non empty set
p is Element of Segm 15
i is Element of SCM-Data-Loc
c1 is Element of SCM-Data-Loc
c2 is V44() integer Element of INT
f is V44() integer Element of INT
<*i,c1,c2,f*> is Relation-like NAT -defined Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like set
[p,{},<*i,c1,c2,f*>] is V21() V22() set
[p,{}] is V21() set
{p,{}} is non empty set
{p} is non empty set
{{p,{}},{p}} is non empty set
[[p,{}],<*i,c1,c2,f*>] is V21() set
{[p,{}],<*i,c1,c2,f*>} is non empty set
{[p,{}]} is Relation-like Function-like non empty set
{{[p,{}],<*i,c1,c2,f*>},{[p,{}]}} is non empty set
(({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V44() integer 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 V44() integer Element of INT : b1 in {2,3} } is non empty set
((({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V44() integer 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 V44() integer 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 V44() integer Element of INT : b1 in {4,5,6,7,8} } is non empty set
T is non empty set
T * is functional non empty FinSequence-membered set
NAT * is functional non empty FinSequence-membered set
[:NAT,(NAT *),(T *):] is set
f1 is set
(({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V44() integer 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 V44() integer Element of INT : b1 in {2,3} } is non empty set
((({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V44() integer 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 V44() integer 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 V44() integer Element of INT : b1 in {4,5,6,7,8} } is non empty set
f2 is V44() integer Element of INT
<*f2*> is Relation-like NAT -defined INT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
[1,f2] is V21() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is Relation-like Function-like non empty set
[14,{},<*f2*>] is V21() V22() set
[[14,{}],<*f2*>] is V21() set
{[14,{}],<*f2*>} is non empty set
{{[14,{}],<*f2*>},{[14,{}]}} is non empty set
f2 is Element of SCM-Data-Loc
<*f2*> 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,f2] is V21() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is Relation-like Function-like non empty set
[1,{},<*f2*>] is V21() V22() set
[1,{}] is V21() set
{1,{}} is non empty set
{{1,{}},{1}} is non empty set
[[1,{}],<*f2*>] is V21() set
{[1,{}],<*f2*>} is non empty set
{[1,{}]} is Relation-like Function-like non empty set
{{[1,{}],<*f2*>},{[1,{}]}} is non empty set
f2 is Element of Segm 15
p is Element of SCM-Data-Loc
i is V44() integer Element of INT
(p,i) is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
<*p*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V21() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is Relation-like Function-like non empty set
<*i*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,i] is V21() set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like non empty set
K75(<*p*>,<*i*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set
[f2,{},(p,i)] is V21() V22() set
[f2,{}] is V21() set
{f2,{}} is non empty set
{f2} is non empty set
{{f2,{}},{f2}} is non empty set
[[f2,{}],(p,i)] is V21() set
{[f2,{}],(p,i)} is non empty set
{[f2,{}]} is Relation-like Function-like non empty set
{{[f2,{}],(p,i)},{[f2,{}]}} is non empty set
f2 is Element of Segm 15
p is Element of SCM-Data-Loc
i is V44() integer Element of INT
c1 is V44() integer Element of INT
<*p,i,c1*> is Relation-like NAT -defined Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like set
<*p*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V21() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is Relation-like Function-like non empty set
<*i*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,i] is V21() set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like non empty set
K75(<*p*>,<*i*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set
<*c1*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c1] is V21() set
{1,c1} is non empty set
{{1,c1},{1}} is non empty set
{[1,c1]} is Relation-like Function-like non empty set
K75(K75(<*p*>,<*i*>),<*c1*>) is Relation-like NAT -defined Function-like non empty V24() K210(K210(1,1),1) -element FinSequence-like FinSubsequence-like set
[f2,{},<*p,i,c1*>] is V21() V22() set
[f2,{}] is V21() set
{f2,{}} is non empty set
{f2} is non empty set
{{f2,{}},{f2}} is non empty set
[[f2,{}],<*p,i,c1*>] is V21() set
{[f2,{}],<*p,i,c1*>} is non empty set
{[f2,{}]} is Relation-like Function-like non empty set
{{[f2,{}],<*p,i,c1*>},{[f2,{}]}} is non empty set
f2 is Element of Segm 15
p is Element of SCM-Data-Loc
i is Element of SCM-Data-Loc
c1 is V44() integer Element of INT
c2 is V44() integer Element of INT
<*p,i,c1,c2*> is Relation-like NAT -defined Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like set
[f2,{},<*p,i,c1,c2*>] is V21() V22() set
[f2,{}] is V21() set
{f2,{}} is non empty set
{f2} is non empty set
{{f2,{}},{f2}} is non empty set
[[f2,{}],<*p,i,c1,c2*>] is V21() set
{[f2,{}],<*p,i,c1,c2*>} is non empty set
{[f2,{}]} is Relation-like Function-like non empty set
{{[f2,{}],<*p,i,c1,c2*>},{[f2,{}]}} is non empty set
(({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V44() integer 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 V44() integer Element of INT : b1 in {2,3} } is non empty set
((({[0,{},{}]} \/ { [14,{},<*b1*>] where b1 is V44() integer 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 V44() integer 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 V44() integer Element of INT : b1 in {4,5,6,7,8} } is non empty set
T is Element of ()
InsCode T is V6() V7() V8() V12() V44() integer ext-real Element of InsCodes ()
InsCodes () is non empty set
K51(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K41(T) is set
K41(K41(T)) is set
T is Element of ()
InsCode T is V6() V7() V8() V12() V44() integer ext-real Element of InsCodes ()
InsCodes () is non empty set
K51(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K41(T) is set
K41(K41(T)) is set
T `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(T) `3_3 is set
T is Element of ()
InsCode T is V6() V7() V8() V12() V44() integer ext-real Element of InsCodes ()
InsCodes () is non empty set
K51(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K41(T) is set
K41(K41(T)) is set
T `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(T) `3_3 is set
f1 is V44() integer Element of INT
<*f1*> is Relation-like NAT -defined INT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
[1,f1] is V21() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is Relation-like Function-like non empty set
[14,{},<*f1*>] is V21() V22() set
[[14,{}],<*f1*>] is V21() set
{[14,{}],<*f1*>} is non empty set
{{[14,{}],<*f1*>},{[14,{}]}} is non empty set
T is Element of ()
InsCode T is V6() V7() V8() V12() V44() integer ext-real Element of InsCodes ()
InsCodes () is non empty set
K51(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K41(T) is set
K41(K41(T)) is set
T `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(T) `3_3 is set
f1 is Element of SCM-Data-Loc
<*f1*> 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,f1] is V21() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is Relation-like Function-like non empty set
[1,{},<*f1*>] is V21() V22() set
[1,{}] is V21() set
{1,{}} is non empty set
{{1,{}},{1}} is non empty set
[[1,{}],<*f1*>] is V21() set
{[1,{}],<*f1*>} is non empty set
{[1,{}]} is Relation-like Function-like non empty set
{{[1,{}],<*f1*>},{[1,{}]}} is non empty set
T is Element of ()
InsCode T is V6() V7() V8() V12() V44() integer ext-real Element of InsCodes ()
InsCodes () is non empty set
K51(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K41(T) is set
K41(K41(T)) is set
T `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(T) `3_3 is set
f1 is Element of Segm 15
f2 is Element of SCM-Data-Loc
p is V44() integer Element of INT
(f2,p) is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT
<*f2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V21() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is Relation-like Function-like non empty set
<*p*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V21() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is Relation-like Function-like non empty set
K75(<*f2*>,<*p*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set
[f1,{},(f2,p)] is V21() V22() set
[f1,{}] is V21() set
{f1,{}} is non empty set
{f1} is non empty set
{{f1,{}},{f1}} is non empty set
[[f1,{}],(f2,p)] is V21() set
{[f1,{}],(f2,p)} is non empty set
{[f1,{}]} is Relation-like Function-like non empty set
{{[f1,{}],(f2,p)},{[f1,{}]}} is non empty set
T is Element of ()
InsCode T is V6() V7() V8() V12() V44() integer ext-real Element of InsCodes ()
InsCodes () is non empty set
K51(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K41(T) is set
K41(K41(T)) is set
T `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(T) `3_3 is set
f1 is Element of Segm 15
f2 is Element of SCM-Data-Loc
p is V44() integer Element of INT
i is V44() integer Element of INT
<*f2,p,i*> is Relation-like NAT -defined Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like set
<*f2*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V21() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is Relation-like Function-like non empty set
<*p*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V21() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is Relation-like Function-like non empty set
K75(<*f2*>,<*p*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set
<*i*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like set
[1,i] is V21() set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like non empty set
K75(K75(<*f2*>,<*p*>),<*i*>) is Relation-like NAT -defined Function-like non empty V24() K210(K210(1,1),1) -element FinSequence-like FinSubsequence-like set
[f1,{},<*f2,p,i*>] is V21() V22() set
[f1,{}] is V21() set
{f1,{}} is non empty set
{f1} is non empty set
{{f1,{}},{f1}} is non empty set
[[f1,{}],<*f2,p,i*>] is V21() set
{[f1,{}],<*f2,p,i*>} is non empty set
{[f1,{}]} is Relation-like Function-like non empty set
{{[f1,{}],<*f2,p,i*>},{[f1,{}]}} is non empty set
T is Element of ()
InsCode T is V6() V7() V8() V12() V44() integer ext-real Element of InsCodes ()
InsCodes () is non empty set
K51(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K41(T) is set
K41(K41(T)) is set
T `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(T) `3_3 is set
f1 is Element of Segm 15
f2 is Element of SCM-Data-Loc
p is Element of SCM-Data-Loc
i is V44() integer Element of INT
c1 is V44() integer Element of INT
<*f2,p,i,c1*> is Relation-like NAT -defined Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like set
[f1,{},<*f2,p,i,c1*>] is V21() V22() set
[f1,{}] is V21() set
{f1,{}} is non empty set
{f1} is non empty set
{{f1,{}},{f1}} is non empty set
[[f1,{}],<*f2,p,i,c1*>] is V21() set
{[f1,{}],<*f2,p,i,c1*>} is non empty set
{[f1,{}]} is Relation-like Function-like non empty set
{{[f1,{}],<*f2,p,i,c1*>},{[f1,{}]}} is non empty set
T is Element of ()
InsCode T is V6() V7() V8() V12() V44() integer ext-real Element of InsCodes ()
InsCodes () is non empty set
K51(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K41(T) is set
K41(K41(T)) is set
f1 is Element of ()
InsCode f1 is V6() V7() V8() V12() V44() integer ext-real Element of InsCodes ()
K41(f1) is set
K41(K41(f1)) is set
T `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(T) `3_3 is set
dom (T `2_3) is Element of bool NAT
f1 `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(f1) `3_3 is set
dom (f1 `2_3) is Element of bool NAT
InsCodes () is non empty set
K51(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
T is Element of InsCodes ()
JumpParts T is functional non empty V40() set
{ (b1 `2_3) where b1 is Element of () : InsCode b1 = T } is set
f1 is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
proj1 f1 is set
f2 is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
proj1 f2 is set
p is set
[T,f1,p] is V21() V22() set
[T,f1] is V21() set
{T,f1} is non empty set
{T} is non empty set
{{T,f1},{T}} is non empty set
[[T,f1],p] is V21() set
{[T,f1],p} is non empty set
{[T,f1]} is Relation-like Function-like non empty set
{{[T,f1],p},{[T,f1]}} is non empty set
[T,f2,p] is V21() V22() set
[T,f2] is V21() set
{T,f2} is non empty set
{{T,f2},{T}} is non empty set
[[T,f2],p] is V21() set
{[T,f2],p} is non empty set
{[T,f2]} is Relation-like Function-like non empty set
{{[T,f2],p},{[T,f2]}} is non empty set
i is Element of ()
InsCode i is V6() V7() V8() V12() V44() integer ext-real Element of InsCodes ()
K41(i) is set
K41(K41(i)) is set
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) `3_3 is set