:: MODELC_2 semantic presentation

REAL is set
NAT is non empty V24() V25() V26() V55() V66() V67() Element of bool REAL
bool REAL is non empty set
COMPLEX is set
RAT is set
INT is set
NAT is non empty V24() V25() V26() V55() V66() V67() set
bool NAT is non empty V55() set
bool NAT is non empty V55() set
BOOLEAN is non empty set
CTL_WFF is non empty set
bool CTL_WFF is non empty set
1 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
{} is functional empty V24() V25() V26() V28() V29() V30() V31() V34() ext-real non positive non negative V55() V66() V68( {} ) FinSequence-membered V74() set
2 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
3 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
0 is functional empty V24() V25() V26() V28() V29() V30() V31() V34() ext-real non positive non negative V55() V66() V68( {} ) FinSequence-membered V74() Element of NAT
Seg 1 is non empty trivial V55() V68(1) Element of bool NAT
K240() is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() boolean set
K241() is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() boolean set
FALSE is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() boolean Element of BOOLEAN
H is set
r is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() set
H is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() set
W is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() set
W + 1 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
H + 1 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
6 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
H is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() set
6 + H is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
<*(6 + H)*> is Relation-like NAT -defined NAT -valued Function-like non empty trivial V55() V68(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> is Relation-like NAT -defined NAT -valued Function-like non empty trivial V55() V68(1) FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ H is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> is Relation-like NAT -defined NAT -valued Function-like non empty trivial V55() V68(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ H is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ H) ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> is Relation-like NAT -defined NAT -valued Function-like non empty trivial V55() V68(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ H is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*2*> ^ H) ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> is Relation-like NAT -defined NAT -valued Function-like non empty trivial V55() V68(1) FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> ^ H is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
4 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
<*4*> is Relation-like NAT -defined NAT -valued Function-like non empty trivial V55() V68(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ H is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ H) ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
5 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
<*5*> is Relation-like NAT -defined NAT -valued Function-like non empty trivial V55() V68(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*5*> ^ H is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*5*> ^ H) ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
H is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() set
<*H*> is Relation-like NAT -defined Function-like non empty trivial V55() V68(1) FinSequence-like FinSubsequence-like set
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*H*> ^ r is Relation-like NAT -defined Function-like non empty V55() FinSequence-like FinSubsequence-like set
len r is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
1 + (len r) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*H*> ^ r) ^ W is Relation-like NAT -defined Function-like non empty V55() FinSequence-like FinSubsequence-like set
len ((<*H*> ^ r) ^ W) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len W is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
(1 + (len r)) + (len W) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
r ^ W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len (r ^ W) is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
(len r) + (len W) is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
len <*H*> is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len <*H*>) + (len (r ^ W)) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len <*H*>) + (len r) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
((len <*H*>) + (len r)) + (len W) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
<*H*> ^ (r ^ W) is Relation-like NAT -defined Function-like non empty V55() FinSequence-like FinSubsequence-like set
len (<*H*> ^ (r ^ W)) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
NAT * is functional non empty FinSequence-membered set
H is set
(0) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
6 + 0 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
<*(6 + 0)*> is Relation-like NAT -defined NAT -valued Function-like non empty trivial V55() V68(1) FinSequence-like FinSubsequence-like FinSequence of NAT
u is non empty set
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
r is non empty set
W is set
W is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() set
(W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
6 + W is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
<*(6 + W)*> is Relation-like NAT -defined NAT -valued Function-like non empty trivial V55() V68(1) FinSequence-like FinSubsequence-like FinSequence of NAT
u is non empty set
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
u is non empty set
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
u is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(W,u) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ W) ^ u is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
nH2 is non empty set
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
u is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(W,u) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*2*> ^ W) ^ u is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
nH2 is non empty set
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
u is non empty set
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
u is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(W,u) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ W) ^ u is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
nH2 is non empty set
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
u is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(W,u) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*5*> ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*5*> ^ W) ^ u is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
nH2 is non empty set
W is non empty set
u is set
H is non empty set
r is non empty set
() is non empty set
the Element of () is Element of ()
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
H is set
H is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() set
(H) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
6 + H is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
<*(6 + H)*> is Relation-like NAT -defined NAT -valued Function-like non empty trivial V55() V68(1) FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ H is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(H) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> ^ H is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H,r) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ H is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ H) ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,r) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ H is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*2*> ^ H) ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,r) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ H is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ H) ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,r) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*5*> ^ H is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*5*> ^ H) ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(0) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
6 + 0 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
<*(6 + 0)*> is Relation-like NAT -defined NAT -valued Function-like non empty trivial V55() V68(1) FinSequence-like FinSubsequence-like FinSequence of NAT
{H} is non empty trivial V68(1) set
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
() \ {H} is Element of bool ()
bool () is non empty set
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
u is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
nH2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(u,nH2) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*5*> ^ u is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*5*> ^ u) ^ nH2 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(r,W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*5*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*5*> ^ r) ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
u is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
nH2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(u,nH2) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*4*> ^ u is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ u) ^ nH2 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(r,W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ r) ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(r) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
u is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
nH2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(u,nH2) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ u is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*2*> ^ u) ^ nH2 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(r,W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*2*> ^ r) ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
u is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
nH2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(u,nH2) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*1*> ^ u is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ u) ^ nH2 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(r,W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ r) ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*0*> ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(r) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
r is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() set
(r) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
6 + r is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
<*(6 + r)*> is Relation-like NAT -defined NAT -valued Function-like non empty trivial V55() V68(1) FinSequence-like FinSubsequence-like FinSequence of NAT
r is set
H is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
H . 1 is set
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(r) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*0*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
H . 1 is set
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(r,W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*1*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ r) ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
r ^ W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ (r ^ W) is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
H . 1 is set
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(r,W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*2*> ^ r) ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
r ^ W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ (r ^ W) is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
H . 1 is set
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(r) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
H . 1 is set
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(r,W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*4*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ r) ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
r ^ W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (r ^ W) is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
H . 1 is set
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(r,W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*5*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*5*> ^ r) ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
r ^ W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*5*> ^ (r ^ W) is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
H . 1 is set
r is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() set
(r) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
6 + r is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
<*(6 + r)*> is Relation-like NAT -defined NAT -valued Function-like non empty trivial V55() V68(1) FinSequence-like FinSubsequence-like FinSequence of NAT
3 + r is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
3 + (3 + r) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
3 + 0 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
2 + r is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
4 + (2 + r) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
4 + 0 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
1 + r is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
5 + (1 + r) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
5 + 0 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
5 + r is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
1 + (5 + r) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
1 + 0 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
4 + r is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
2 + (4 + r) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
2 + 0 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
H is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
H . 1 is set
H is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
len H is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
r is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() set
(r) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
6 + r is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
<*(6 + r)*> is Relation-like NAT -defined NAT -valued Function-like non empty trivial V55() V68(1) FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(r) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*0*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len r is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
1 + (len r) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(r,W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*1*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ r) ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len r is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
1 + (len r) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len W is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
(1 + (len r)) + (len W) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(r,W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*2*> ^ r) ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len r is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
1 + (len r) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len W is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
(1 + (len r)) + (len W) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(r) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len r is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
1 + (len r) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(r,W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*4*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ r) ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len r is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
1 + (len r) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len W is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
(1 + (len r)) + (len W) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(r,W) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*5*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*5*> ^ r) ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len r is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
1 + (len r) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len W is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
(1 + (len r)) + (len W) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
H is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
W is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
r ^ W is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
u is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() set
nH2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
len nH2 is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
k is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
r1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
k ^ r1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
dom k is Element of bool NAT
len k is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
Seg (len k) is V55() V68( len k) Element of bool NAT
len <*0*> is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
j is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(j) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*0*> ^ j is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(k ^ r1) . 1 is set
k . 1 is set
j1 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(j1) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*0*> ^ j1 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len j is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
(len <*0*>) + (len j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(<*0*> ^ j1) ^ r1 is Relation-like NAT -defined Function-like non empty V55() FinSequence-like FinSubsequence-like set
j1 ^ r1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
<*0*> ^ (j1 ^ r1) is Relation-like NAT -defined Function-like non empty V55() FinSequence-like FinSubsequence-like set
j is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
j1 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(j,j1) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*5*> ^ j is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*5*> ^ j) ^ j1 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len j1 is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
len j is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
1 + (len j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len j1) + (1 + (len j)) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len j1) + 1 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
((len j1) + 1) + (len j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len (<*5*> ^ j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len <*5*> is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len <*5*>) + (len j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len (<*5*> ^ j)) + (len j1) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
f2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
f2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(f2,f2) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*5*> ^ f2 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*5*> ^ f2) ^ f2 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len f2 is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
(len f2) + 1 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len f2 is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
((len f2) + 1) + (len f2) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len r1 is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
(((len f2) + 1) + (len f2)) + (len r1) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len f2) + (len r1) is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
((len f2) + 1) + ((len f2) + (len r1)) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
j ^ G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
len (k ^ r1) is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
(len k) + (len r1) is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
len (<*5*> ^ f2) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len <*5*>) + (len f2) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len (<*5*> ^ f2)) + (len f2) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
f2 ^ f2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*5*> ^ (f2 ^ f2) is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*5*> ^ (f2 ^ f2)) ^ r1 is Relation-like NAT -defined Function-like non empty V55() FinSequence-like FinSubsequence-like set
(f2 ^ f2) ^ r1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
<*5*> ^ ((f2 ^ f2) ^ r1) is Relation-like NAT -defined Function-like non empty V55() FinSequence-like FinSubsequence-like set
G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
f2 ^ G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
(len j) + 1 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
f2 ^ r1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
f2 ^ (f2 ^ r1) is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
j ^ j1 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*5*> ^ (j ^ j1) is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
f2 ^ G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
j is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
j1 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(j,j1) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*4*> ^ j is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ j) ^ j1 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len j1 is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
len j is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
1 + (len j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len j1) + (1 + (len j)) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len j1) + 1 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
((len j1) + 1) + (len j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len (<*4*> ^ j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len <*4*> is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len <*4*>) + (len j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len (<*4*> ^ j)) + (len j1) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
f2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
f2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(f2,f2) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*4*> ^ f2 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ f2) ^ f2 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len f2 is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
(len f2) + 1 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len f2 is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
((len f2) + 1) + (len f2) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(((len f2) + 1) + (len f2)) + (len r1) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len f2) + (len r1) is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
((len f2) + 1) + ((len f2) + (len r1)) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
j ^ G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
len (<*4*> ^ f2) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len <*4*>) + (len f2) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len (<*4*> ^ f2)) + (len f2) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
f2 ^ f2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (f2 ^ f2) is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (f2 ^ f2)) ^ r1 is Relation-like NAT -defined Function-like non empty V55() FinSequence-like FinSubsequence-like set
(f2 ^ f2) ^ r1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
<*4*> ^ ((f2 ^ f2) ^ r1) is Relation-like NAT -defined Function-like non empty V55() FinSequence-like FinSubsequence-like set
G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
f2 ^ G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
(len j) + 1 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
f2 ^ r1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
f2 ^ (f2 ^ r1) is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
j ^ j1 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (j ^ j1) is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
f2 ^ G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
j is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
j1 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(j,j1) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ j is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*2*> ^ j) ^ j1 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len j1 is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
len j is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
1 + (len j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len j1) + (1 + (len j)) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len j1) + 1 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
((len j1) + 1) + (len j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len (<*2*> ^ j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len <*2*> is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len <*2*>) + (len j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len (<*2*> ^ j)) + (len j1) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
f2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
f2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(f2,f2) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ f2 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*2*> ^ f2) ^ f2 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len f2 is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
(len f2) + 1 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len f2 is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
((len f2) + 1) + (len f2) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(((len f2) + 1) + (len f2)) + (len r1) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len f2) + (len r1) is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
((len f2) + 1) + ((len f2) + (len r1)) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
j ^ G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
len (<*2*> ^ f2) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len <*2*>) + (len f2) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len (<*2*> ^ f2)) + (len f2) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
f2 ^ f2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ (f2 ^ f2) is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*2*> ^ (f2 ^ f2)) ^ r1 is Relation-like NAT -defined Function-like non empty V55() FinSequence-like FinSubsequence-like set
(f2 ^ f2) ^ r1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
<*2*> ^ ((f2 ^ f2) ^ r1) is Relation-like NAT -defined Function-like non empty V55() FinSequence-like FinSubsequence-like set
G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
f2 ^ G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
(len j) + 1 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
f2 ^ r1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
f2 ^ (f2 ^ r1) is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
j ^ j1 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ (j ^ j1) is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
f2 ^ G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
j is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
j1 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(j,j1) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*1*> ^ j is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ j) ^ j1 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len j1 is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
len j is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
1 + (len j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len j1) + (1 + (len j)) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len j1) + 1 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
((len j1) + 1) + (len j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len (<*1*> ^ j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len <*1*> is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len <*1*>) + (len j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len (<*1*> ^ j)) + (len j1) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
f2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
f2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(f2,f2) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*1*> ^ f2 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ f2) ^ f2 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len f2 is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
(len f2) + 1 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
len f2 is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
((len f2) + 1) + (len f2) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(((len f2) + 1) + (len f2)) + (len r1) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len f2) + (len r1) is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
((len f2) + 1) + ((len f2) + (len r1)) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
j ^ G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
len (<*1*> ^ f2) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len <*1*>) + (len f2) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(len (<*1*> ^ f2)) + (len f2) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
f2 ^ f2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ (f2 ^ f2) is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ (f2 ^ f2)) ^ r1 is Relation-like NAT -defined Function-like non empty V55() FinSequence-like FinSubsequence-like set
(f2 ^ f2) ^ r1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
<*1*> ^ ((f2 ^ f2) ^ r1) is Relation-like NAT -defined Function-like non empty V55() FinSequence-like FinSubsequence-like set
G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
f2 ^ G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
(len j) + 1 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
f2 ^ r1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
f2 ^ (f2 ^ r1) is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
j ^ j1 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ (j ^ j1) is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
f2 ^ G1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
len <*3*> is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
j is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(j) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ j is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
j1 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(j1) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ j1 is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len j is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
(len <*3*>) + (len j) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
(<*3*> ^ j1) ^ r1 is Relation-like NAT -defined Function-like non empty V55() FinSequence-like FinSubsequence-like set
j1 ^ r1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
<*3*> ^ (j1 ^ r1) is Relation-like NAT -defined Function-like non empty V55() FinSequence-like FinSubsequence-like set
j is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() set
(j) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
6 + j is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
<*(6 + j)*> is Relation-like NAT -defined NAT -valued Function-like non empty trivial V55() V68(1) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + (len r1) is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
1 + 0 is non empty V24() V25() V26() V30() V31() V34() ext-real positive non negative V55() V66() Element of NAT
u is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() set
nH2 is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
len nH2 is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
k is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
r1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
k ^ r1 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
len H is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
H is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H,r) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*1*> ^ H is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ H) ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
u is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(W,u) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*1*> ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ W) ^ u is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
H ^ r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ (H ^ r) is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
W ^ u is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ (W ^ u) is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
len W is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
len H is V24() V25() V26() V30() V31() V34() ext-real non negative V55() V66() Element of NAT
nH2 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
H ^ nH2 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
W ^ k is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
nH2 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
H ^ nH2 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
nH2 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
W ^ nH2 is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
H ^ k is Relation-like NAT -defined Function-like V55() FinSequence-like FinSubsequence-like set
H is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H,r) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ H is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*2*> ^ H) ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
W is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
u is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
(W,u) is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ W is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*2*> ^ W) ^ u is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
H ^ r is Relation-like NAT -defined NAT -valued Function-like V55() FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ (H ^ r) is Relation-like NAT -defined NAT -valued Function-like non empty V55() FinSequence-like FinSubsequence-like FinSequence of NAT
W ^ u is Relation-like