REAL is set
NAT is non empty V17() V18() V19() Element of bool REAL
bool REAL is set
NAT is non empty V17() V18() V19() set
bool NAT is set
bool NAT is set
9 is non empty V17() V18() V19() V23() V59() V94() ext-real positive Element of NAT
Segm 9 is non empty Element of bool NAT
SCM-Data-Loc is non empty set
K163() is set
bool K163() is set
2 is non empty V17() V18() V19() V23() V59() V94() ext-real positive Element of NAT
[:K163(),2:] is Relation-like set
bool [:K163(),2:] is set
K165() is Relation-like Function-like V36(K163(),2) Element of bool [:K163(),2:]
K166() is Relation-like 2 -defined Function-like total set
K165() * K166() is Relation-like Function-like set
K138((K165() * K166())) is set
SCM-Instr is non empty Relation-like standard-ins homogeneous J/A-independent with_halt set
K110(K138((K165() * K166())),K138((K165() * K166()))) is set
[:SCM-Instr,K110(K138((K165() * K166())),K138((K165() * K166()))):] is Relation-like set
bool [:SCM-Instr,K110(K138((K165() * K166())),K138((K165() * K166()))):] is set
K287() is V87(2) L8(2)
the U5 of K287() is non empty Relation-like standard-ins homogeneous J/A-independent with_halt set
the U1 of K287() is set
K251(2,K287()) is Relation-like the U1 of K287() -defined Function-like total set
RAT is set
INT is set
1 is non empty V17() V18() V19() V23() V59() V94() ext-real positive Element of NAT
3 is non empty V17() V18() V19() V23() V59() V94() ext-real positive Element of NAT
{} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() FinSequence-like FinSubsequence-like FinSequence-membered V59() V94() ext-real complex-valued ext-real-valued real-valued natural-valued set
the empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() FinSequence-like FinSubsequence-like FinSequence-membered V59() V94() ext-real complex-valued ext-real-valued real-valued natural-valued set is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() FinSequence-like FinSubsequence-like FinSequence-membered V59() V94() ext-real complex-valued ext-real-valued real-valued natural-valued set
8 is non empty V17() V18() V19() V23() V59() V94() ext-real positive Element of NAT
0 is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() FinSequence-like FinSubsequence-like FinSequence-membered V59() V94() ext-real complex-valued ext-real-valued real-valued natural-valued Element of NAT
4 is non empty V17() V18() V19() V23() V59() V94() ext-real positive Element of NAT
5 is non empty V17() V18() V19() V23() V59() V94() ext-real positive Element of NAT
6 is non empty V17() V18() V19() V23() V59() V94() ext-real positive Element of NAT
7 is non empty V17() V18() V19() V23() V59() V94() ext-real positive Element of NAT
12 is non empty V17() V18() V19() V23() V59() V94() ext-real positive Element of NAT
10 is non empty V17() V18() V19() V23() V59() V94() ext-real positive Element of NAT
11 is non empty V17() V18() V19() V23() V59() V94() ext-real positive Element of NAT
[0,{},{}] is V1() V2() set
[0,{}] is V1() set
{0,{}} is non empty functional set
{0} is non empty functional set
{{0,{}},{0}} is non empty set
[[0,{}],{}] is V1() set
{[0,{}],{}} is non empty set
{[0,{}]} is non empty Relation-like Function-like set
{{[0,{}],{}},{[0,{}]}} is non empty set
NAT * is non empty functional FinSequence-membered set
proj2 SCM-Instr is non empty functional FinSequence-membered set
[:NAT,(NAT *),(proj2 SCM-Instr):] is set
INT \ NAT is Element of bool INT
bool INT is set
() is set
13 is non empty V17() V18() V19() V23() V59() V94() ext-real positive Element of NAT
Segm 13 is non empty Element of bool NAT
{9,10} is non empty set
{ [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM-Data-Loc , b4 is Element of () : b1 in {9,10} } is set
SCM-Instr \/ { [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM-Data-Loc , b4 is Element of () : b1 in {9,10} } is non empty set
{11,12} is non empty set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 13, b2 is Element of SCM-Data-Loc , b3 is Element of () : b1 in {11,12} } is set
(SCM-Instr \/ { [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM-Data-Loc , b4 is Element of () : b1 in {9,10} } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 13, b2 is Element of SCM-Data-Loc , b3 is Element of () : b1 in {11,12} } is non empty set
() is non empty set
proj2 () is set
[:NAT,(NAT *),(proj2 ()):] is set
T is set
f1 is Element of Segm 13
f2 is Element of SCM-Data-Loc
II is Element of ()
p is Element of SCM-Data-Loc
<*f2,II,p*> is non empty Relation-like NAT -defined Function-like V24() 3 -element FinSequence-like FinSubsequence-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{1} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
<*II*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,II] is V1() set
{1,II} is non empty set
{{1,II},{1}} is non empty set
{[1,II]} is non empty Relation-like Function-like set
K91(<*f2*>,<*II*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
K311(1,1) is V17() V18() V19() V23() V59() V94() ext-real Element of NAT
<*p*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V1() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty Relation-like Function-like set
K91(K91(<*f2*>,<*II*>),<*p*>) is non empty Relation-like NAT -defined Function-like V24() K311(K311(1,1),1) -element FinSequence-like FinSubsequence-like set
K311(K311(1,1),1) is V17() V18() V19() V23() V59() V94() ext-real Element of NAT
[f1,{},<*f2,II,p*>] is V1() V2() set
[f1,{}] is V1() set
{f1,{}} is non empty set
{f1} is non empty set
{{f1,{}},{f1}} is non empty set
[[f1,{}],<*f2,II,p*>] is V1() set
{[f1,{}],<*f2,II,p*>} is non empty set
{[f1,{}]} is non empty Relation-like Function-like set
{{[f1,{}],<*f2,II,p*>},{[f1,{}]}} is non empty set
f1 is Element of Segm 13
f2 is Element of SCM-Data-Loc
p is Element of ()
<*f2,p*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{1} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
<*p*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V1() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty Relation-like Function-like set
K91(<*f2*>,<*p*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
K311(1,1) is V17() V18() V19() V23() V59() V94() ext-real Element of NAT
[f1,{},<*f2,p*>] is V1() V2() set
[f1,{}] is V1() set
{f1,{}} is non empty set
{f1} is non empty set
{{f1,{}},{f1}} is non empty set
[[f1,{}],<*f2,p*>] is V1() set
{[f1,{}],<*f2,p*>} is non empty set
{[f1,{}]} is non empty Relation-like Function-like set
{{[f1,{}],<*f2,p*>},{[f1,{}]}} is non empty set
{ [13,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } is set
f1 is Element of SCM-Data-Loc
<*f1*> is non empty Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,f1] is V1() set
{1,f1} is non empty set
{1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty Relation-like Function-like set
[13,{},<*f1*>] is V1() V2() set
[13,{}] is V1() set
{13,{}} is non empty set
{13} is non empty set
{{13,{}},{13}} is non empty set
[[13,{}],<*f1*>] is V1() set
{[13,{}],<*f1*>} is non empty set
{[13,{}]} is non empty Relation-like Function-like set
{{[13,{}],<*f1*>},{[13,{}]}} is non empty set
f2 is Element of Segm 13
{ [13,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } is set
T is set
f1 is set
[f1,T] is V1() set
{f1,T} is non empty set
{f1} is non empty set
{{f1,T},{f1}} is non empty set
p is Element of Segm 13
II is Element of SCM-Data-Loc
t is Element of ()
ii is Element of SCM-Data-Loc
<*II,t,ii*> is non empty Relation-like NAT -defined Function-like V24() 3 -element FinSequence-like FinSubsequence-like set
<*II*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,II] is V1() set
{1,II} is non empty set
{1} is non empty set
{{1,II},{1}} is non empty set
{[1,II]} is non empty Relation-like Function-like set
<*t*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,t] is V1() set
{1,t} is non empty set
{{1,t},{1}} is non empty set
{[1,t]} is non empty Relation-like Function-like set
K91(<*II*>,<*t*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
K311(1,1) is V17() V18() V19() V23() V59() V94() ext-real Element of NAT
<*ii*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,ii] is V1() set
{1,ii} is non empty set
{{1,ii},{1}} is non empty set
{[1,ii]} is non empty Relation-like Function-like set
K91(K91(<*II*>,<*t*>),<*ii*>) is non empty Relation-like NAT -defined Function-like V24() K311(K311(1,1),1) -element FinSequence-like FinSubsequence-like set
K311(K311(1,1),1) is V17() V18() V19() V23() V59() V94() ext-real Element of NAT
[p,{},<*II,t,ii*>] is V1() V2() set
[p,{}] is V1() set
{p,{}} is non empty set
{p} is non empty set
{{p,{}},{p}} is non empty set
[[p,{}],<*II,t,ii*>] is V1() set
{[p,{}],<*II,t,ii*>} is non empty set
{[p,{}]} is non empty Relation-like Function-like set
{{[p,{}],<*II,t,ii*>},{[p,{}]}} is non empty set
p is Element of Segm 13
II is Element of SCM-Data-Loc
ii is Element of ()
<*II,ii*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like set
<*II*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,II] is V1() set
{1,II} is non empty set
{1} is non empty set
{{1,II},{1}} is non empty set
{[1,II]} is non empty Relation-like Function-like set
<*ii*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,ii] is V1() set
{1,ii} is non empty set
{{1,ii},{1}} is non empty set
{[1,ii]} is non empty Relation-like Function-like set
K91(<*II*>,<*ii*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
K311(1,1) is V17() V18() V19() V23() V59() V94() ext-real Element of NAT
[p,{},<*II,ii*>] is V1() V2() set
[p,{}] is V1() set
{p,{}} is non empty set
{p} is non empty set
{{p,{}},{p}} is non empty set
[[p,{}],<*II,ii*>] is V1() set
{[p,{}],<*II,ii*>} is non empty set
{[p,{}]} is non empty Relation-like Function-like set
{{[p,{}],<*II,ii*>},{[p,{}]}} is non empty set
{ [13,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } is set
p is Element of SCM-Data-Loc
<*p*> is non empty Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,p] is V1() set
{1,p} is non empty set
{1} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty Relation-like Function-like set
[13,{},<*p*>] is V1() V2() set
[13,{}] is V1() set
{13,{}} is non empty set
{13} is non empty set
{{13,{}},{13}} is non empty set
[[13,{}],<*p*>] is V1() set
{[13,{}],<*p*>} is non empty set
{[13,{}]} is non empty Relation-like Function-like set
{{[13,{}],<*p*>},{[13,{}]}} is non empty set
{ [13,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } is set
T is non empty set
T * is non empty functional FinSequence-membered set
[:NAT,(NAT *),(T *):] is set
T is Element of ()
T `1_3 is V17() V18() V19() V23() V59() V94() ext-real set
K5(T) is set
K5(K5(T)) is set
f1 is Element of Segm 13
f2 is Element of SCM-Data-Loc
p is Element of ()
<*f2,p*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{1} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
<*p*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V1() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty Relation-like Function-like set
K91(<*f2*>,<*p*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
K311(1,1) is V17() V18() V19() V23() V59() V94() ext-real Element of NAT
[f1,{},<*f2,p*>] is V1() V2() set
[f1,{}] is V1() set
{f1,{}} is non empty set
{f1} is non empty set
{{f1,{}},{f1}} is non empty set
[[f1,{}],<*f2,p*>] is V1() set
{[f1,{}],<*f2,p*>} is non empty set
{[f1,{}]} is non empty Relation-like Function-like set
{{[f1,{}],<*f2,p*>},{[f1,{}]}} is non empty set
f1 is Element of Segm 13
f2 is Element of SCM-Data-Loc
II is Element of ()
p is Element of SCM-Data-Loc
<*f2,II,p*> is non empty Relation-like NAT -defined Function-like V24() 3 -element FinSequence-like FinSubsequence-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
<*II*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,II] is V1() set
{1,II} is non empty set
{{1,II},{1}} is non empty set
{[1,II]} is non empty Relation-like Function-like set
K91(<*f2*>,<*II*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
<*p*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V1() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty Relation-like Function-like set
K91(K91(<*f2*>,<*II*>),<*p*>) is non empty Relation-like NAT -defined Function-like V24() K311(K311(1,1),1) -element FinSequence-like FinSubsequence-like set
K311(K311(1,1),1) is V17() V18() V19() V23() V59() V94() ext-real Element of NAT
[f1,{},<*f2,II,p*>] is V1() V2() set
[f1,{}] is V1() set
{f1,{}} is non empty set
{f1} is non empty set
{{f1,{}},{f1}} is non empty set
[[f1,{}],<*f2,II,p*>] is V1() set
{[f1,{}],<*f2,II,p*>} is non empty set
{[f1,{}]} is non empty Relation-like Function-like set
{{[f1,{}],<*f2,II,p*>},{[f1,{}]}} is non empty set
{ [13,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum } is set
f1 is Element of SCM-Data-Loc
<*f1*> is non empty Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,f1] is V1() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty Relation-like Function-like set
[13,{},<*f1*>] is V1() V2() set
[13,{}] is V1() set
{13,{}} is non empty set
{13} is non empty set
{{13,{}},{13}} is non empty set
[[13,{}],<*f1*>] is V1() set
{[13,{}],<*f1*>} is non empty set
{[13,{}]} is non empty Relation-like Function-like set
{{[13,{}],<*f1*>},{[13,{}]}} is non empty set
T is set
f1 is Element of SCM-Data-Loc
f2 is Element of SCM-Data-Loc
p is Element of ()
<*f1,p,f2*> is non empty Relation-like NAT -defined Function-like V24() 3 -element FinSequence-like FinSubsequence-like set
<*f1*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f1] is V1() set
{1,f1} is non empty set
{1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty Relation-like Function-like set
<*p*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V1() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty Relation-like Function-like set
K91(<*f1*>,<*p*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
K311(1,1) is V17() V18() V19() V23() V59() V94() ext-real Element of NAT
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
K91(K91(<*f1*>,<*p*>),<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K311(K311(1,1),1) -element FinSequence-like FinSubsequence-like set
K311(K311(1,1),1) is V17() V18() V19() V23() V59() V94() ext-real Element of NAT
[T,{},<*f1,p,f2*>] is V1() V2() set
[T,{}] is V1() set
{T,{}} is non empty set
{T} is non empty set
{{T,{}},{T}} is non empty set
[[T,{}],<*f1,p,f2*>] is V1() set
{[T,{}],<*f1,p,f2*>} is non empty set
{[T,{}]} is non empty Relation-like Function-like set
{{[T,{}],<*f1,p,f2*>},{[T,{}]}} is non empty set
II is Element of Segm 13
[II,{},<*f1,p,f2*>] is V1() V2() set
[II,{}] is V1() set
{II,{}} is non empty set
{II} is non empty set
{{II,{}},{II}} is non empty set
[[II,{}],<*f1,p,f2*>] is V1() set
{[II,{}],<*f1,p,f2*>} is non empty set
{[II,{}]} is non empty Relation-like Function-like set
{{[II,{}],<*f1,p,f2*>},{[II,{}]}} is non empty set
T is set
f1 is Element of SCM-Data-Loc
f2 is Element of ()
<*f1,f2*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like set
<*f1*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f1] is V1() set
{1,f1} is non empty set
{1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty Relation-like Function-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
K91(<*f1*>,<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
K311(1,1) is V17() V18() V19() V23() V59() V94() ext-real Element of NAT
[T,{},<*f1,f2*>] is V1() V2() set
[T,{}] is V1() set
{T,{}} is non empty set
{T} is non empty set
{{T,{}},{T}} is non empty set
[[T,{}],<*f1,f2*>] is V1() set
{[T,{}],<*f1,f2*>} is non empty set
{[T,{}]} is non empty Relation-like Function-like set
{{[T,{}],<*f1,f2*>},{[T,{}]}} is non empty set
p is Element of Segm 13
[p,{},<*f1,f2*>] is V1() V2() set
[p,{}] is V1() set
{p,{}} is non empty set
{p} is non empty set
{{p,{}},{p}} is non empty set
[[p,{}],<*f1,f2*>] is V1() set
{[p,{}],<*f1,f2*>} is non empty set
{[p,{}]} is non empty Relation-like Function-like set
{{[p,{}],<*f1,f2*>},{[p,{}]}} is non empty set
T is Element of ()
II is Element of Segm 13
f1 is Element of SCM-Data-Loc
f2 is Element of ()
p is Element of SCM-Data-Loc
<*f1,f2,p*> is non empty Relation-like NAT -defined Function-like V24() 3 -element FinSequence-like FinSubsequence-like set
<*f1*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f1] is V1() set
{1,f1} is non empty set
{1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty Relation-like Function-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
K91(<*f1*>,<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
K311(1,1) is V17() V18() V19() V23() V59() V94() ext-real Element of NAT
<*p*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V1() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty Relation-like Function-like set
K91(K91(<*f1*>,<*f2*>),<*p*>) is non empty Relation-like NAT -defined Function-like V24() K311(K311(1,1),1) -element FinSequence-like FinSubsequence-like set
K311(K311(1,1),1) is V17() V18() V19() V23() V59() V94() ext-real Element of NAT
[II,{},<*f1,f2,p*>] is V1() V2() set
[II,{}] is V1() set
{II,{}} is non empty set
{II} is non empty set
{{II,{}},{II}} is non empty set
[[II,{}],<*f1,f2,p*>] is V1() set
{[II,{}],<*f1,f2,p*>} is non empty set
{[II,{}]} is non empty Relation-like Function-like set
{{[II,{}],<*f1,f2,p*>},{[II,{}]}} is non empty set
T `3_3 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set
ii is Element of SCM-Data-Loc
t is Element of SCM-Data-Loc
f1 is Element of SCM-Data-Loc
c2 is Element of ()
f2 is Element of SCM-Data-Loc
<*f1,c2,f2*> is non empty Relation-like NAT -defined Function-like V24() 3 -element FinSequence-like FinSubsequence-like set
<*f1*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f1] is V1() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty Relation-like Function-like set
<*c2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c2] is V1() set
{1,c2} is non empty set
{{1,c2},{1}} is non empty set
{[1,c2]} is non empty Relation-like Function-like set
K91(<*f1*>,<*c2*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
K91(K91(<*f1*>,<*c2*>),<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K311(K311(1,1),1) -element FinSequence-like FinSubsequence-like set
c2 is Element of SCM-Data-Loc
f2 is Element of ()
b2 is Element of SCM-Data-Loc
<*c2,f2,b2*> is non empty Relation-like NAT -defined Function-like V24() 3 -element FinSequence-like FinSubsequence-like set
<*c2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c2] is V1() set
{1,c2} is non empty set
{{1,c2},{1}} is non empty set
{[1,c2]} is non empty Relation-like Function-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
K91(<*c2*>,<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
<*b2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,b2] is V1() set
{1,b2} is non empty set
{{1,b2},{1}} is non empty set
{[1,b2]} is non empty Relation-like Function-like set
K91(K91(<*c2*>,<*f2*>),<*b2*>) is non empty Relation-like NAT -defined Function-like V24() K311(K311(1,1),1) -element FinSequence-like FinSubsequence-like set
<*f1,c2,f2*> . 1 is set
ii is Element of SCM-Data-Loc
t is Element of SCM-Data-Loc
f1 is Element of SCM-Data-Loc
c2 is Element of ()
f2 is Element of SCM-Data-Loc
<*f1,c2,f2*> is non empty Relation-like NAT -defined Function-like V24() 3 -element FinSequence-like FinSubsequence-like set
<*f1*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f1] is V1() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty Relation-like Function-like set
<*c2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c2] is V1() set
{1,c2} is non empty set
{{1,c2},{1}} is non empty set
{[1,c2]} is non empty Relation-like Function-like set
K91(<*f1*>,<*c2*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
K91(K91(<*f1*>,<*c2*>),<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K311(K311(1,1),1) -element FinSequence-like FinSubsequence-like set
c2 is Element of SCM-Data-Loc
f2 is Element of ()
b2 is Element of SCM-Data-Loc
<*c2,f2,b2*> is non empty Relation-like NAT -defined Function-like V24() 3 -element FinSequence-like FinSubsequence-like set
<*c2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c2] is V1() set
{1,c2} is non empty set
{{1,c2},{1}} is non empty set
{[1,c2]} is non empty Relation-like Function-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
K91(<*c2*>,<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
<*b2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,b2] is V1() set
{1,b2} is non empty set
{{1,b2},{1}} is non empty set
{[1,b2]} is non empty Relation-like Function-like set
K91(K91(<*c2*>,<*f2*>),<*b2*>) is non empty Relation-like NAT -defined Function-like V24() K311(K311(1,1),1) -element FinSequence-like FinSubsequence-like set
<*f1,c2,f2*> . 3 is set
ii is Element of ()
t is Element of ()
f1 is Element of SCM-Data-Loc
c2 is Element of ()
f2 is Element of SCM-Data-Loc
<*f1,c2,f2*> is non empty Relation-like NAT -defined Function-like V24() 3 -element FinSequence-like FinSubsequence-like set
<*f1*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f1] is V1() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty Relation-like Function-like set
<*c2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c2] is V1() set
{1,c2} is non empty set
{{1,c2},{1}} is non empty set
{[1,c2]} is non empty Relation-like Function-like set
K91(<*f1*>,<*c2*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
K91(K91(<*f1*>,<*c2*>),<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K311(K311(1,1),1) -element FinSequence-like FinSubsequence-like set
c2 is Element of SCM-Data-Loc
f2 is Element of ()
b2 is Element of SCM-Data-Loc
<*c2,f2,b2*> is non empty Relation-like NAT -defined Function-like V24() 3 -element FinSequence-like FinSubsequence-like set
<*c2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c2] is V1() set
{1,c2} is non empty set
{{1,c2},{1}} is non empty set
{[1,c2]} is non empty Relation-like Function-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
K91(<*c2*>,<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
<*b2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,b2] is V1() set
{1,b2} is non empty set
{{1,b2},{1}} is non empty set
{[1,b2]} is non empty Relation-like Function-like set
K91(K91(<*c2*>,<*f2*>),<*b2*>) is non empty Relation-like NAT -defined Function-like V24() K311(K311(1,1),1) -element FinSequence-like FinSubsequence-like set
<*f1,c2,f2*> . 2 is set
T is Element of ()
f1 is Element of SCM-Data-Loc
<*f1*> is non empty Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,f1] is V1() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty Relation-like Function-like set
[13,{},<*f1*>] is V1() V2() set
[13,{}] is V1() set
{13,{}} is non empty set
{13} is non empty set
{{13,{}},{13}} is non empty set
[[13,{}],<*f1*>] is V1() set
{[13,{}],<*f1*>} is non empty set
{[13,{}]} is non empty Relation-like Function-like set
{{[13,{}],<*f1*>},{[13,{}]}} is non empty set
T `3_3 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set
f2 is Element of SCM-Data-Loc
p is Element of SCM-Data-Loc
II is Element of SCM-Data-Loc
<*II*> is non empty Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,II] is V1() set
{1,II} is non empty set
{{1,II},{1}} is non empty set
{[1,II]} is non empty Relation-like Function-like set
ii is Element of SCM-Data-Loc
<*ii*> is non empty Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc
[1,ii] is V1() set
{1,ii} is non empty set
{{1,ii},{1}} is non empty set
{[1,ii]} is non empty Relation-like Function-like set
<*II*> /. 1 is Element of SCM-Data-Loc
T is Element of ()
p is Element of Segm 13
f1 is Element of SCM-Data-Loc
f2 is Element of ()
<*f1,f2*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like set
<*f1*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f1] is V1() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty Relation-like Function-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
K91(<*f1*>,<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
[p,{},<*f1,f2*>] is V1() V2() set
[p,{}] is V1() set
{p,{}} is non empty set
{p} is non empty set
{{p,{}},{p}} is non empty set
[[p,{}],<*f1,f2*>] is V1() set
{[p,{}],<*f1,f2*>} is non empty set
{[p,{}]} is non empty Relation-like Function-like set
{{[p,{}],<*f1,f2*>},{[p,{}]}} is non empty set
T `3_3 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like set
II is Element of SCM-Data-Loc
ii is Element of SCM-Data-Loc
t is Element of SCM-Data-Loc
f1 is Element of ()
<*t,f1*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like set
<*t*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,t] is V1() set
{1,t} is non empty set
{{1,t},{1}} is non empty set
{[1,t]} is non empty Relation-like Function-like set
<*f1*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f1] is V1() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty Relation-like Function-like set
K91(<*t*>,<*f1*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
c2 is Element of SCM-Data-Loc
f2 is Element of ()
<*c2,f2*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like set
<*c2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c2] is V1() set
{1,c2} is non empty set
{{1,c2},{1}} is non empty set
{[1,c2]} is non empty Relation-like Function-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
K91(<*c2*>,<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
<*t,f1*> . 1 is set
II is Element of ()
ii is Element of ()
t is Element of SCM-Data-Loc
f1 is Element of ()
<*t,f1*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like set
<*t*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,t] is V1() set
{1,t} is non empty set
{{1,t},{1}} is non empty set
{[1,t]} is non empty Relation-like Function-like set
<*f1*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f1] is V1() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty Relation-like Function-like set
K91(<*t*>,<*f1*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
c2 is Element of SCM-Data-Loc
f2 is Element of ()
<*c2,f2*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like set
<*c2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,c2] is V1() set
{1,c2} is non empty set
{{1,c2},{1}} is non empty set
{[1,c2]} is non empty Relation-like Function-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
K91(<*c2*>,<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
<*t,f1*> . 2 is set
T is Element of ()
InsCode T is V17() V18() V19() V23() V59() V94() ext-real Element of InsCodes ()
InsCodes () is non empty set
K15(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K5(T) is set
K5(K5(T)) is set
f1 is Element of Segm 13
f2 is Element of SCM-Data-Loc
II is Element of ()
p is Element of SCM-Data-Loc
<*f2,II,p*> is non empty Relation-like NAT -defined Function-like V24() 3 -element FinSequence-like FinSubsequence-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
<*II*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,II] is V1() set
{1,II} is non empty set
{{1,II},{1}} is non empty set
{[1,II]} is non empty Relation-like Function-like set
K91(<*f2*>,<*II*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
<*p*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V1() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty Relation-like Function-like set
K91(K91(<*f2*>,<*II*>),<*p*>) is non empty Relation-like NAT -defined Function-like V24() K311(K311(1,1),1) -element FinSequence-like FinSubsequence-like set
[f1,{},<*f2,II,p*>] is V1() V2() set
[f1,{}] is V1() set
{f1,{}} is non empty set
{f1} is non empty set
{{f1,{}},{f1}} is non empty set
[[f1,{}],<*f2,II,p*>] is V1() set
{[f1,{}],<*f2,II,p*>} is non empty set
{[f1,{}]} is non empty Relation-like Function-like set
{{[f1,{}],<*f2,II,p*>},{[f1,{}]}} is non empty set
f1 is Element of Segm 13
f2 is Element of SCM-Data-Loc
p is Element of ()
<*f2,p*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
<*p*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V1() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty Relation-like Function-like set
K91(<*f2*>,<*p*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
[f1,{},<*f2,p*>] is V1() V2() set
[f1,{}] is V1() set
{f1,{}} is non empty set
{f1} is non empty set
{{f1,{}},{f1}} is non empty set
[[f1,{}],<*f2,p*>] is V1() set
{[f1,{}],<*f2,p*>} is non empty set
{[f1,{}]} is non empty Relation-like Function-like set
{{[f1,{}],<*f2,p*>},{[f1,{}]}} is non empty set
T is Element of ()
InsCode T is V17() V18() V19() V23() V59() V94() ext-real Element of InsCodes ()
InsCodes () is non empty set
K15(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K5(T) is set
K5(K5(T)) is set
T is Element of ()
InsCode T is V17() V18() V19() V23() V59() V94() ext-real Element of InsCodes ()
InsCodes () is non empty set
K15(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K5(T) is set
K5(K5(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
K5(T) `3_3 is set
f1 is Element of Segm 13
f2 is Element of SCM-Data-Loc
II is Element of ()
p is Element of SCM-Data-Loc
<*f2,II,p*> is non empty Relation-like NAT -defined Function-like V24() 3 -element FinSequence-like FinSubsequence-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
<*II*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,II] is V1() set
{1,II} is non empty set
{{1,II},{1}} is non empty set
{[1,II]} is non empty Relation-like Function-like set
K91(<*f2*>,<*II*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
<*p*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V1() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty Relation-like Function-like set
K91(K91(<*f2*>,<*II*>),<*p*>) is non empty Relation-like NAT -defined Function-like V24() K311(K311(1,1),1) -element FinSequence-like FinSubsequence-like set
[f1,{},<*f2,II,p*>] is V1() V2() set
[f1,{}] is V1() set
{f1,{}} is non empty set
{f1} is non empty set
{{f1,{}},{f1}} is non empty set
[[f1,{}],<*f2,II,p*>] is V1() set
{[f1,{}],<*f2,II,p*>} is non empty set
{[f1,{}]} is non empty Relation-like Function-like set
{{[f1,{}],<*f2,II,p*>},{[f1,{}]}} is non empty set
T is Element of ()
InsCode T is V17() V18() V19() V23() V59() V94() ext-real Element of InsCodes ()
InsCodes () is non empty set
K15(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K5(T) is set
K5(K5(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
K5(T) `3_3 is set
f1 is Element of Segm 13
f2 is Element of SCM-Data-Loc
p is Element of ()
<*f2,p*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like set
<*f2*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty Relation-like Function-like set
<*p*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V1() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty Relation-like Function-like set
K91(<*f2*>,<*p*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
[f1,{},<*f2,p*>] is V1() V2() set
[f1,{}] is V1() set
{f1,{}} is non empty set
{f1} is non empty set
{{f1,{}},{f1}} is non empty set
[[f1,{}],<*f2,p*>] is V1() set
{[f1,{}],<*f2,p*>} is non empty set
{[f1,{}]} is non empty Relation-like Function-like set
{{[f1,{}],<*f2,p*>},{[f1,{}]}} is non empty set
T is Element of ()
InsCode T is V17() V18() V19() V23() V59() V94() ext-real Element of InsCodes ()
InsCodes () is non empty set
K15(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K5(T) is set
K5(K5(T)) is set
f1 is Element of ()
InsCode f1 is V17() V18() V19() V23() V59() V94() ext-real Element of InsCodes ()
K5(f1) is set
K5(K5(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
K5(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
K5(f1) `3_3 is set
dom (f1 `2_3) is Element of bool NAT
T is Element of ()
InsCode T is V17() V18() V19() V23() V59() V94() ext-real Element of InsCodes ()
InsCodes () is non empty set
K15(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K5(T) is set
K5(K5(T)) is set
JumpParts (InsCode T) is non empty functional V55() set
{ (b1 `2_3) where b1 is Element of () : InsCode b1 = InsCode T } is set
f1 is Element of SCM-Instr
InsCode f1 is V17() V18() V19() V23() V59() V94() ext-real Element of InsCodes SCM-Instr
InsCodes SCM-Instr is non empty set
K15(SCM-Instr) is set
proj1 SCM-Instr is non empty set
proj1 (proj1 SCM-Instr) is set
K5(f1) is set
K5(K5(f1)) is set
JumpParts (InsCode f1) is non empty functional V55() V56() set
{ (b1 `2_3) where b1 is Element of SCM-Instr : InsCode b1 = InsCode f1 } is set
f2 is set
p is Element of ()
p `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
K5(p) is set
K5(p) `3_3 is set
InsCode p is V17() V18() V19() V23() V59() V94() ext-real Element of InsCodes ()
K5(K5(p)) is set
II is Element of SCM-Instr
InsCode II is V17() V18() V19() V23() V59() V94() ext-real Element of InsCodes SCM-Instr
K5(II) is set
K5(K5(II)) is set
f2 is set
p is Element of SCM-Instr
p `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
K5(p) is set
K5(p) `3_3 is set
InsCode p is V17() V18() V19() V23() V59() V94() ext-real Element of InsCodes SCM-Instr
K5(K5(p)) is set
II is Element of ()
InsCode II is V17() V18() V19() V23() V59() V94() ext-real Element of InsCodes ()
K5(II) is set
K5(K5(II)) is set
InsCodes () is non empty set
K15(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
{{}} is non empty functional set
T is Element of InsCodes ()
JumpParts T is non empty functional V55() set
{ (b1 `2_3) where b1 is Element of () : InsCode b1 = T } is set
f1 is set
f2 is Element of ()
f2 `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
K5(f2) is set
K5(f2) `3_3 is set
InsCode f2 is V17() V18() V19() V23() V59() V94() ext-real Element of InsCodes ()
K5(K5(f2)) is set
p is Element of Segm 13
II is Element of SCM-Data-Loc
t is Element of ()
ii is Element of SCM-Data-Loc
<*II,t,ii*> is non empty Relation-like NAT -defined Function-like V24() 3 -element FinSequence-like FinSubsequence-like set
<*II*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,II] is V1() set
{1,II} is non empty set
{{1,II},{1}} is non empty set
{[1,II]} is non empty Relation-like Function-like set
<*t*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,t] is V1() set
{1,t} is non empty set
{{1,t},{1}} is non empty set
{[1,t]} is non empty Relation-like Function-like set
K91(<*II*>,<*t*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
<*ii*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,ii] is V1() set
{1,ii} is non empty set
{{1,ii},{1}} is non empty set
{[1,ii]} is non empty Relation-like Function-like set
K91(K91(<*II*>,<*t*>),<*ii*>) is non empty Relation-like NAT -defined Function-like V24() K311(K311(1,1),1) -element FinSequence-like FinSubsequence-like set
[p,{},<*II,t,ii*>] is V1() V2() set
[p,{}] is V1() set
{p,{}} is non empty set
{p} is non empty set
{{p,{}},{p}} is non empty set
[[p,{}],<*II,t,ii*>] is V1() set
{[p,{}],<*II,t,ii*>} is non empty set
{[p,{}]} is non empty Relation-like Function-like set
{{[p,{}],<*II,t,ii*>},{[p,{}]}} is non empty set
the Element of SCM-Data-Loc is Element of SCM-Data-Loc
the Element of () is Element of ()
p is set
<* the Element of SCM-Data-Loc , the Element of (), the Element of SCM-Data-Loc *> is non empty Relation-like NAT -defined Function-like V24() 3 -element FinSequence-like FinSubsequence-like set
<* the Element of SCM-Data-Loc *> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1, the Element of SCM-Data-Loc ] is V1() 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 non empty Relation-like Function-like set
<* the Element of ()*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1, the Element of ()] is V1() set
{1, the Element of ()} is non empty set
{{1, the Element of ()},{1}} is non empty set
{[1, the Element of ()]} is non empty Relation-like Function-like set
K91(<* the Element of SCM-Data-Loc *>,<* the Element of ()*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
K91(K91(<* the Element of SCM-Data-Loc *>,<* the Element of ()*>),<* the Element of SCM-Data-Loc *>) is non empty Relation-like NAT -defined Function-like V24() K311(K311(1,1),1) -element FinSequence-like FinSubsequence-like set
[T,{},<* the Element of SCM-Data-Loc , the Element of (), the Element of SCM-Data-Loc *>] is V1() V2() set
[T,{}] is V1() set
{T,{}} is non empty set
{T} is non empty set
{{T,{}},{T}} is non empty set
[[T,{}],<* the Element of SCM-Data-Loc , the Element of (), the Element of SCM-Data-Loc *>] is V1() set
{[T,{}],<* the Element of SCM-Data-Loc , the Element of (), the Element of SCM-Data-Loc *>} is non empty set
{[T,{}]} is non empty Relation-like Function-like set
{{[T,{}],<* the Element of SCM-Data-Loc , the Element of (), the Element of SCM-Data-Loc *>},{[T,{}]}} is non empty set
[T,{},<* the Element of SCM-Data-Loc , the Element of (), the Element of SCM-Data-Loc *>] `2_3 is set
K5([T,{},<* the Element of SCM-Data-Loc , the Element of (), the Element of SCM-Data-Loc *>]) is set
K5([T,{},<* the Element of SCM-Data-Loc , the Element of (), the Element of SCM-Data-Loc *>]) `3_3 is set
[T,{},<* the Element of SCM-Data-Loc , the Element of (), the Element of SCM-Data-Loc *>] `1_3 is set
K5(K5([T,{},<* the Element of SCM-Data-Loc , the Element of (), the Element of SCM-Data-Loc *>])) is set
T is Element of InsCodes ()
JumpParts T is non empty functional V55() set
{ (b1 `2_3) where b1 is Element of () : InsCode b1 = T } is set
f1 is set
f2 is Element of ()
f2 `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
K5(f2) is set
K5(f2) `3_3 is set
InsCode f2 is V17() V18() V19() V23() V59() V94() ext-real Element of InsCodes ()
K5(K5(f2)) is set
p is Element of Segm 13
II is Element of SCM-Data-Loc
ii is Element of ()
<*II,ii*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like set
<*II*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,II] is V1() set
{1,II} is non empty set
{{1,II},{1}} is non empty set
{[1,II]} is non empty Relation-like Function-like set
<*ii*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1,ii] is V1() set
{1,ii} is non empty set
{{1,ii},{1}} is non empty set
{[1,ii]} is non empty Relation-like Function-like set
K91(<*II*>,<*ii*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
[p,{},<*II,ii*>] is V1() V2() set
[p,{}] is V1() set
{p,{}} is non empty set
{p} is non empty set
{{p,{}},{p}} is non empty set
[[p,{}],<*II,ii*>] is V1() set
{[p,{}],<*II,ii*>} is non empty set
{[p,{}]} is non empty Relation-like Function-like set
{{[p,{}],<*II,ii*>},{[p,{}]}} is non empty set
the Element of SCM-Data-Loc is Element of SCM-Data-Loc
the Element of () is Element of ()
p is set
<* the Element of SCM-Data-Loc , the Element of ()*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like set
<* the Element of SCM-Data-Loc *> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1, the Element of SCM-Data-Loc ] is V1() 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 non empty Relation-like Function-like set
<* the Element of ()*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like set
[1, the Element of ()] is V1() set
{1, the Element of ()} is non empty set
{{1, the Element of ()},{1}} is non empty set
{[1, the Element of ()]} is non empty Relation-like Function-like set
K91(<* the Element of SCM-Data-Loc *>,<* the Element of ()*>) is non empty Relation-like NAT -defined Function-like V24() K311(1,1) -element FinSequence-like FinSubsequence-like set
[T,{},<* the Element of SCM-Data-Loc , the Element of ()*>] is V1() V2() set
[T,{}] is V1() set
{T,{}} is non empty set
{T} is non empty set
{{T,{}},{T}} is non empty set
[[T,{}],<* the Element of SCM-Data-Loc , the Element of ()*>] is V1() set
{[T,{}],<* the Element of SCM-Data-Loc , the Element of ()*>} is non empty set
{[T,{}]} is non empty Relation-like Function-like set
{{[T,{}],<* the Element of SCM-Data-Loc , the Element of ()*>},{[T,{}]}} is non empty set
[T,{},<* the Element of SCM-Data-Loc , the Element of ()*>] `2_3 is set
K5([T,{},<* the Element of SCM-Data-Loc , the Element of ()*>]) is set
K5([T,{},<* the Element of SCM-Data-Loc , the Element of ()*>]) `3_3 is set
[T,{},<* the Element of SCM-Data-Loc , the Element of ()*>] `1_3 is set
K5(K5([T,{},<* the Element of SCM-Data-Loc , the Element of ()*>])) is set
T is Element of InsCodes ()
JumpParts T is non empty functional V55() 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 V1() V2() set
[T,f1] is V1() set
{T,f1} is non empty set
{T} is non empty set
{{T,f1},{T}} is non empty set
[[T,f1],p] is V1() set
{[T,f1],p} is non empty set
{[T,f1]} is non empty Relation-like Function-like set
{{[T,f1],p},{[T,f1]}} is non empty set
[T,f2,p] is V1() V2() set
[T,f2] is V1() set
{T,f2} is non empty set
{{T,f2},{T}} is non empty set
[[T,f2],p] is V1() set
{[T,f2],p} is non empty set
{[T,f2]} is non empty Relation-like Function-like set
{{[T,f2],p},{[T,f2]}} is non empty set
[T,f1,p] `1_3 is set
K5([T,f1,p]) is set
K5(K5([T,f1,p])) is set
II is Element of ()
InsCode II is V17() V18() V19() V23() V59() V94() ext-real Element of InsCodes ()
K5(II) is set
K5(K5(II)) is set
ii is Element of SCM-Instr
InsCode ii is V17() V18() V19() V23() V59() V94() ext-real Element of InsCodes SCM-Instr
InsCodes SCM-Instr is non empty set
K15(SCM-Instr) is set
proj1 SCM-Instr is non empty set
proj1 (proj1 SCM-Instr) is set
K5(ii) is set
K5(K5(ii)) is set
t is Element of InsCodes SCM-Instr
[t,f1,p] is V1() V2() set
[t,f1] is V1() set
{t,f1} is non empty set
{t} is non empty set
{{t,f1},{t}} is non empty set
[[t,f1],p] is V1() set
{[t,f1],p} is non empty set
{[t,f1]} is non empty Relation-like Function-like set
{{[t,f1],p},{[t,f1]}} is non empty set
JumpParts t is non empty functional V55() V56() set
{ (b1 `2_3) where b1 is Element of SCM-Instr : InsCode b1 = t } is set
[t,f2,p] is V1() V2() set
[t,f2] is V1() set
{t,f2} is non empty set
{{t,f2},{t}} is non empty set
[[t,f2],p] is V1() set
{[t,f2],p} is non empty set
{[t,f2]} is non empty Relation-like Function-like set
{{[t,f2],p},{[t,f2]}} is non empty set