:: FILEREC1 semantic presentation

REAL is set
NAT is non empty V4() V5() V6() V32() V37() V38() Element of K6(REAL)
K6(REAL) is set
NAT is non empty V4() V5() V6() V32() V37() V38() set
K6(NAT) is V32() set
K6(NAT) is V32() set
COMPLEX is set
{} is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() set
1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
2 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
3 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() Element of NAT
Seg 1 is non empty V2() V32() V39(1) Element of K6(NAT)
Seg 2 is non empty V32() V39(2) Element of K6(NAT)
len {} is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() set
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR ^ r1) ^ r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
f is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR ^ r1) ^ r2) ^ f is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 ^ r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ (r1 ^ r2) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR ^ (r1 ^ r2)) ^ f is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 ^ f is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR ^ r1) ^ (r2 ^ f) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
CR | (len CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
Seg (len CR) is V32() V39( len CR) Element of K6(NAT)
CR | (Seg (len CR)) is Relation-like NAT -defined Seg (len CR) -defined NAT -defined D -valued Function-like FinSubsequence-like Element of K6(K7(NAT,D))
K7(NAT,D) is Relation-like set
K6(K7(NAT,D)) is set
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
<*> D is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() FinSequence of D
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
r2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
CR /^ r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (CR /^ r2) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
CR /^ r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (CR /^ r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) -' r2 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
r1 - r1 is V11() ext-real V43() set
r2 - r1 is V11() ext-real V43() set
(len CR) -' r1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((len CR) -' r1) - ((len CR) -' r2) is V11() ext-real V43() set
((len CR) -' r1) - 0 is V11() ext-real non negative V43() set
(len (CR /^ r1)) - (len (CR /^ r2)) is V11() ext-real V43() set
(len CR) -' r1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((len CR) -' r1) - ((len CR) -' r2) is V11() ext-real V43() set
((len CR) -' r1) - 0 is V11() ext-real non negative V43() set
(len (CR /^ r1)) - (len (CR /^ r2)) is V11() ext-real V43() set
(len CR) -' r1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((len CR) -' r1) - ((len CR) -' r2) is V11() ext-real V43() set
(len CR) - r2 is V11() ext-real V43() set
((len CR) -' r1) - ((len CR) - r2) is V11() ext-real V43() set
(len CR) - r1 is V11() ext-real V43() set
((len CR) - r1) - ((len CR) - r2) is V11() ext-real V43() set
(len (CR /^ r1)) - (len (CR /^ r2)) is V11() ext-real V43() set
(len (CR /^ r1)) - (len (CR /^ r2)) is V11() ext-real V43() set
(len (CR /^ r1)) - (len (CR /^ r2)) is V11() ext-real V43() set
(len (CR /^ r1)) - (len (CR /^ r2)) is V11() ext-real V43() set
(len (CR /^ r1)) - (len (CR /^ r2)) is V11() ext-real V43() set
0 + (len (CR /^ r2)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len (CR /^ r1)) - (len (CR /^ r2))) + (len (CR /^ r2)) is V11() ext-real V43() set
D is non empty set
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) + 1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
mid ((CR ^ r1),((len CR) + 1),((len CR) + (len r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
Seg (len r1) is V32() V39( len r1) Element of K6(NAT)
r1 | (Seg (len r1)) is Relation-like NAT -defined Seg (len r1) -defined NAT -defined D -valued Function-like FinSubsequence-like Element of K6(K7(NAT,D))
K7(NAT,D) is Relation-like V32() set
K6(K7(NAT,D)) is V32() set
((len CR) + (len r1)) - (len CR) is V11() ext-real V43() set
(len CR) - (len CR) is V11() ext-real V43() set
((len CR) + (len r1)) -' (len CR) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((len CR) + (len r1)) -' ((len CR) + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(((len CR) + (len r1)) -' ((len CR) + 1)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
((len CR) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(CR ^ r1) /^ (((len CR) + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR ^ r1) /^ (((len CR) + 1) -' 1)) | ((((len CR) + (len r1)) -' ((len CR) + 1)) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR ^ r1) /^ (len CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR ^ r1) /^ (len CR)) | ((((len CR) + (len r1)) -' ((len CR) + 1)) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR ^ r1) /^ (len CR)) | (((len CR) + (len r1)) -' (len CR)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((len CR) + 1) - (len CR) is V11() ext-real V43() set
((len CR) + (len r1)) - (len CR) is V11() ext-real V43() set
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
f is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
mid ((CR ^ r1),r2,f) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
mid (CR,r2,f) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
CR /^ (r2 -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (CR /^ (r2 -' 1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
r2 - 1 is V11() ext-real V43() set
(len (CR /^ (r2 -' 1))) + (r2 - 1) is V11() ext-real V43() set
((len (CR /^ (r2 -' 1))) + (r2 - 1)) - (r2 - 1) is V11() ext-real V43() set
(len CR) - 0 is V11() ext-real V43() set
(len (CR /^ (r2 -' 1))) + (r2 -' 1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) -' (r2 -' 1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((len CR) -' (r2 -' 1)) + (r2 -' 1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(len CR) - (r2 - 1) is V11() ext-real V43() set
(len CR) - r2 is V11() ext-real V43() set
((len CR) - r2) + 1 is V11() ext-real V43() set
f - r2 is V11() ext-real V43() set
(f - r2) + 1 is V11() ext-real V43() set
r2 - r2 is V11() ext-real V43() set
f -' r2 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(f -' r2) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(CR ^ r1) /^ (r2 -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR ^ r1) /^ (r2 -' 1)) | ((f -' r2) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR /^ (r2 -' 1)) ^ r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR /^ (r2 -' 1)) ^ r1) | ((f -' r2) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR /^ (r2 -' 1)) | ((f -' r2) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
r2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
f is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
CR | f is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (CR | f) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
mid (CR,r1,r2) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
mid ((CR | f),r1,r2) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 -' r1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(r2 -' r1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
r2 - r1 is V11() ext-real V43() set
(r2 - r1) + 1 is V11() ext-real V43() set
r1 - 1 is V11() ext-real V43() set
f - 0 is V11() ext-real V43() set
f - r1 is V11() ext-real V43() set
(f - r1) + 1 is V11() ext-real V43() set
r1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
f -' (r1 -' 1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
f - (r1 - 1) is V11() ext-real V43() set
(CR | f) /^ (r1 -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR | f) /^ (r1 -' 1)) | ((r2 -' r1) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR /^ (r1 -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR /^ (r1 -' 1)) | (f -' (r1 -' 1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR /^ (r1 -' 1)) | (f -' (r1 -' 1))) | ((r2 -' r1) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR /^ (r1 -' 1)) | ((r2 -' r1) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is set
<*D*> is non empty V2() Relation-like NAT -defined Function-like constant V32() V39(1) FinSequence-like FinSubsequence-like set
CR is non empty set
r1 is Relation-like NAT -defined CR -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of CR
dom r1 is Element of K6(NAT)
K7((dom r1),CR) is Relation-like set
K6(K7((dom r1),CR)) is set
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
r1 . 1 is set
D is set
CR is set
<*D,CR*> is non empty V2() Relation-like NAT -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set
r1 is non empty set
r2 is Relation-like NAT -defined r1 -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r1
dom r2 is Element of K6(NAT)
K7((dom r2),r1) is Relation-like set
K6(K7((dom r2),r1)) is set
r2 . 1 is set
r2 . 2 is set
D is set
CR is set
r1 is set
<*D,CR,r1*> is non empty Relation-like NAT -defined Function-like V32() V39(3) FinSequence-like FinSubsequence-like set
r2 is non empty set
f is Relation-like NAT -defined r2 -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r2
dom f is Element of K6(NAT)
K7((dom f),r2) is Relation-like set
K6(K7((dom f),r2)) is set
f . 3 is set
f . 1 is set
f . 2 is set
D is set
<*D*> is non empty V2() Relation-like NAT -defined Function-like constant V32() V39(1) FinSequence-like FinSubsequence-like set
CR is non empty set
r1 is Relation-like NAT -defined CR -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of CR
r1 | 1 is Relation-like NAT -defined CR -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of CR
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
D is set
CR is set
<*D,CR*> is non empty V2() Relation-like NAT -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set
<*CR*> is non empty V2() Relation-like NAT -defined Function-like constant V32() V39(1) FinSequence-like FinSubsequence-like set
r1 is non empty set
r2 is Relation-like NAT -defined r1 -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r1
r2 /^ 1 is Relation-like NAT -defined r1 -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r1
dom r2 is Element of K6(NAT)
K7((dom r2),r1) is Relation-like set
K6(K7((dom r2),r1)) is set
r2 . 1 is set
r2 . 2 is set
f is Element of r1
f2 is Element of r1
<*f,f2*> is non empty V2() Relation-like NAT -defined r1 -valued Function-like V32() V39(2) FinSequence-like FinSubsequence-like FinSequence of r1
<*f,f2*> /^ 1 is Relation-like NAT -defined r1 -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r1
<*f2*> is non empty V2() Relation-like NAT -defined r1 -valued Function-like constant V32() V39(1) FinSequence-like FinSubsequence-like FinSequence of r1
D is set
<*D*> is non empty V2() Relation-like NAT -defined Function-like constant V32() V39(1) FinSequence-like FinSubsequence-like set
CR is set
r1 is set
<*D,CR,r1*> is non empty Relation-like NAT -defined Function-like V32() V39(3) FinSequence-like FinSubsequence-like set
r2 is non empty set
f is Relation-like NAT -defined r2 -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r2
f | 1 is Relation-like NAT -defined r2 -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r2
f | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined r2 -valued Function-like FinSubsequence-like Element of K6(K7(NAT,r2))
K7(NAT,r2) is Relation-like V32() set
K6(K7(NAT,r2)) is V32() set
D is set
CR is set
<*D,CR*> is non empty V2() Relation-like NAT -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set
r1 is set
<*D,CR,r1*> is non empty Relation-like NAT -defined Function-like V32() V39(3) FinSequence-like FinSubsequence-like set
r2 is non empty set
f is Relation-like NAT -defined r2 -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r2
f | 2 is Relation-like NAT -defined r2 -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r2
f | (Seg 2) is Relation-like NAT -defined Seg 2 -defined NAT -defined r2 -valued Function-like FinSubsequence-like Element of K6(K7(NAT,r2))
K7(NAT,r2) is Relation-like V32() set
K6(K7(NAT,r2)) is V32() set
D is set
CR is set
r1 is set
<*D,CR,r1*> is non empty Relation-like NAT -defined Function-like V32() V39(3) FinSequence-like FinSubsequence-like set
<*CR,r1*> is non empty V2() Relation-like NAT -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set
r2 is non empty set
f is Relation-like NAT -defined r2 -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r2
f /^ 1 is Relation-like NAT -defined r2 -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r2
f . 3 is set
a2 is Element of r2
f . 1 is set
f2 is Element of r2
f . 2 is set
j is Element of r2
D is set
CR is set
r1 is set
<*D,CR,r1*> is non empty Relation-like NAT -defined Function-like V32() V39(3) FinSequence-like FinSubsequence-like set
<*r1*> is non empty V2() Relation-like NAT -defined Function-like constant V32() V39(1) FinSequence-like FinSubsequence-like set
r2 is non empty set
f is Relation-like NAT -defined r2 -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r2
f /^ 2 is Relation-like NAT -defined r2 -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r2
1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
f2 is Element of r2
<*f2*> is non empty V2() Relation-like NAT -defined r2 -valued Function-like constant V32() V39(1) FinSequence-like FinSubsequence-like FinSequence of r2
j is Element of r2
a2 is Element of r2
<*j,a2*> is non empty V2() Relation-like NAT -defined r2 -valued Function-like V32() V39(2) FinSequence-like FinSubsequence-like FinSequence of r2
<*f2*> ^ <*j,a2*> is non empty Relation-like NAT -defined r2 -valued Function-like V32() V39(1 + 2) FinSequence-like FinSubsequence-like FinSequence of r2
1 + 2 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(<*f2*> ^ <*j,a2*>) /^ (1 + 1) is Relation-like NAT -defined r2 -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r2
len <*f2*> is non empty V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len <*f2*>) + 1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(<*f2*> ^ <*j,a2*>) /^ ((len <*f2*>) + 1) is Relation-like NAT -defined r2 -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r2
<*j,a2*> /^ 1 is Relation-like NAT -defined r2 -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r2
<*a2*> is non empty V2() Relation-like NAT -defined r2 -valued Function-like constant V32() V39(1) FinSequence-like FinSubsequence-like FinSequence of r2
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
Rev CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
<*> D is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() FinSequence of D
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
Rev CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
CR /^ r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
Rev (CR /^ r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(len CR) -' r1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(Rev CR) | ((len CR) -' r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (Rev CR) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len (Rev CR)) -' r1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
len ((Rev CR) | ((len CR) -' r1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(Rev CR) | ((len (Rev CR)) -' r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len ((Rev CR) | ((len (Rev CR)) -' r1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) - r1 is V11() ext-real V43() set
len (Rev (CR /^ r1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
f is V4() V5() V6() V10() V11() ext-real V32() V37() V43() set
(Rev (CR /^ r1)) . f is set
((Rev CR) | ((len CR) -' r1)) . f is set
dom (Rev (CR /^ r1)) is Element of K6(NAT)
len (CR /^ r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len (CR /^ r1)) - f is V11() ext-real V43() set
((len (CR /^ r1)) - f) + 1 is V11() ext-real V43() set
(CR /^ r1) . (((len (CR /^ r1)) - f) + 1) is set
((len CR) - r1) - f is V11() ext-real V43() set
(((len CR) - r1) - f) + 1 is V11() ext-real V43() set
(CR /^ r1) . ((((len CR) - r1) - f) + 1) is set
(len CR) + 0 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) + r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len CR) + r1) - r1 is V11() ext-real V43() set
(len CR) - f is V11() ext-real V43() set
(len CR) -' f is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
f - 1 is V11() ext-real V43() set
(len CR) + (f - 1) is V11() ext-real V43() set
(len CR) - (f - 1) is V11() ext-real V43() set
((len CR) + (f - 1)) - (f - 1) is V11() ext-real V43() set
((len CR) - f) + 1 is V11() ext-real V43() set
((len CR) -' f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
dom CR is Element of K6(NAT)
CR /^ 0 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
dom (Rev CR) is Element of K6(NAT)
((len CR) -' r1) - f is V11() ext-real V43() set
((len CR) -' r1) -' f is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(Rev CR) . f is set
CR . (((len CR) - f) + 1) is set
(((len CR) -' r1) -' f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
r1 + ((((len CR) -' r1) -' f) + 1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
r1 + ((((len CR) - r1) - f) + 1) is V11() ext-real V43() set
((len CR) - r1) + r1 is V11() ext-real V43() set
(((len CR) - r1) + r1) - f is V11() ext-real V43() set
((((len CR) - r1) + r1) - f) + 1 is V11() ext-real V43() set
((len CR) - r1) + 0 is V11() ext-real V43() set
((len CR) - r1) + (f - 1) is V11() ext-real V43() set
((len CR) - r1) - (f - 1) is V11() ext-real V43() set
(((len CR) - r1) + (f - 1)) - (f - 1) is V11() ext-real V43() set
Seg (len (CR /^ r1)) is V32() V39( len (CR /^ r1)) Element of K6(NAT)
dom (CR /^ r1) is Element of K6(NAT)
(CR /^ r1) /. ((((len CR) -' r1) -' f) + 1) is Element of D
(CR /^ 0) /. (r1 + ((((len CR) -' r1) -' f) + 1)) is Element of D
len (CR /^ r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
instr (1,(CR ^ r1),r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) + 1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
((len CR) + 1) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(((len CR) + 1) + (len r1)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
f2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
f2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(CR ^ r1) /^ (f2 -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len ((CR ^ r1) /^ (f2 -' 1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
mid (((CR ^ r1) /^ (f2 -' 1)),1,(len r1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(len r1) + f2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
0 + f2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
f2 + 1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len r1) + f2) - 1 is V11() ext-real V43() set
((len r1) + f2) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(len r1) - 1 is V11() ext-real V43() set
(((len r1) + f2) -' 1) -' f2 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((((len r1) + f2) -' 1) -' f2) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(((len r1) + f2) - 1) - f2 is V11() ext-real V43() set
((((len r1) + f2) - 1) - f2) + 1 is V11() ext-real V43() set
((CR ^ r1) /^ (f2 -' 1)) | (((((len r1) + f2) -' 1) -' f2) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
f2 + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(f2 + (len r1)) - 1 is V11() ext-real V43() set
(f2 + (len r1)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(len CR) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len CR) + (len r1)) + 1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(((len CR) + (len r1)) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(len r1) + (len CR) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len r1) + (len CR)) + 1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(((len r1) + (len CR)) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
mid ((CR ^ r1),((len CR) + 1),((((len CR) + 1) + (len r1)) -' 1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
smid ((CR ^ r1),((len CR) + 1),((((len CR) + 1) + (len r1)) -' 1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(f2 + 1) - 1 is V11() ext-real V43() set
f2 - 1 is V11() ext-real V43() set
(f2 -' 1) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(f2 - 1) + (len r1) is V11() ext-real V43() set
mid ((CR ^ r1),f2,((f2 -' 1) + (len r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
smid ((CR ^ r1),f2,((f2 + (len r1)) -' 1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((len CR) + 1) - f2 is V11() ext-real V43() set
((len CR) + 1) -' f2 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
len (CR ^ r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(((len CR) + 1) - f2) + f2 is V11() ext-real V43() set
((len CR) + 1) - 1 is V11() ext-real V43() set
mid (CR,f2,((f2 -' 1) + (len r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR ^ r1) /^ (len CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((len CR) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(CR ^ r1) /^ (((len CR) + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
r2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(CR ^ r1) /^ (r2 -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (CR ^ r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len (CR ^ r1)) + 1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len (CR ^ r1)) + 1) -' (len r1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len CR) + (len r1)) + 1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(((len CR) + (len r1)) + 1) -' (len r1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(len CR) + 1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len r1) + ((len CR) + 1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len r1) + ((len CR) + 1)) -' (len r1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
instr (1,(CR ^ r1),r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
D is non empty set
D is non empty set
<*> D is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlpart ((<*> D),CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlpart (CR,(<*> D)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(<*> D) ^ CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ (<*> D) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
<*> D is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
addcr ((<*> D),CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlcon ((<*> D),CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlpart ((<*> D),CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (ovlpart ((<*> D),CR)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
CR /^ (len (ovlpart ((<*> D),CR))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(<*> D) ^ (CR /^ (len (ovlpart ((<*> D),CR)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (<*> D) is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() Element of NAT
CR /^ (len (<*> D)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(<*> D) ^ (CR /^ (len (<*> D))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR /^ 0 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(<*> D) ^ (CR /^ 0) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
CR is set
r1 is set
<*r1*> is non empty V2() Relation-like NAT -defined Function-like constant V32() V39(1) FinSequence-like FinSubsequence-like set
<*r1,CR,r1*> is non empty Relation-like NAT -defined Function-like V32() V39(3) FinSequence-like FinSubsequence-like set
<*CR,r1*> is non empty V2() Relation-like NAT -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set
f2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
f is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
f2 . 1 is set
len f2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
<*r1,CR*> is non empty V2() Relation-like NAT -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set
<*r1,CR*> ^ <*r1*> is non empty Relation-like NAT -defined Function-like V32() V39(2 + 1) FinSequence-like FinSubsequence-like set
2 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
r2 | 2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(r2 | 2) ^ f2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlpart (r2,f2) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (ovlpart (r2,f2)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
f2 /^ (len (ovlpart (r2,f2))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 ^ (f2 /^ (len (ovlpart (r2,f2)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlcon (r2,f2) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
f2 ^ f is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len r2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len f is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len f2) + (len f) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len <*CR,r1*> is non empty V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
1 + (len <*CR,r1*>) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
1 + 2 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
addcr (r2,f2) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
mid (r2,1,(len f2)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(1 -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
r2 /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(r2 /^ (1 -' 1)) | ((1 -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
1 + 0 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(r2 /^ (1 -' 1)) | (1 + 0) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 /^ 0 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(r2 /^ 0) | 1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 | 1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
j is Element of D
a2 is Element of D
<*j,a2,j*> is non empty Relation-like NAT -defined D -valued Function-like V32() V39(3) FinSequence-like FinSubsequence-like FinSequence of D
<*j,a2,j*> | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined D -valued Function-like FinSubsequence-like Element of K6(K7(NAT,D))
K7(NAT,D) is Relation-like V32() set
K6(K7(NAT,D)) is V32() set
f /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(0 + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
f /^ ((0 + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
f /^ 0 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (1 -' 1)) . 1 is set
j is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
j -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
f /^ (j -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
f /^ (2 -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(1 + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
f /^ ((1 + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
<*a2,j*> is non empty V2() Relation-like NAT -defined D -valued Function-like V32() V39(2) FinSequence-like FinSubsequence-like FinSequence of D
<*a2,j*> /^ 1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
instr (1,f,f2) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len f) + 1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len f) + 1) -' (len f2) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(len CR) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len (CR ^ r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
mid ((CR ^ r1),1,(len CR)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
addcr (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlcon (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlpart (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (ovlpart (CR,r1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
r1 /^ (len (ovlpart (CR,r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ (r1 /^ (len (ovlpart (CR,r1)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) - (len r1) is V11() ext-real V43() set
(len r1) - (len r1) is V11() ext-real V43() set
D is non empty set
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
addcr (r1,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
Rev r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (Rev r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
Rev CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (Rev CR) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len r1) - (len CR) is V11() ext-real V43() set
0 + (len CR) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len r1) - (len CR)) + (len CR) is V11() ext-real V43() set
mid ((Rev r1),1,(len CR)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
Rev (mid ((Rev r1),1,(len CR))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
Rev (Rev CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
mid ((Rev r1),(len CR),1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(len (Rev r1)) - (len CR) is V11() ext-real V43() set
((len (Rev r1)) - (len CR)) + (len CR) is V11() ext-real V43() set
(len r1) + 1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len r1) + 1) -' (len CR) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
mid (r1,(((len r1) + 1) -' (len CR)),(len r1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(1 + 1) - 1 is V11() ext-real V43() set
(len CR) - 1 is V11() ext-real V43() set
(len CR) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((len CR) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(len (Rev r1)) -' (len CR) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(Rev r1) /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((Rev r1) /^ (1 -' 1)) | (((len CR) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
Rev (((Rev r1) /^ (1 -' 1)) | (((len CR) -' 1) + 1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(Rev r1) /^ 0 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((Rev r1) /^ 0) | (len CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
Rev (((Rev r1) /^ 0) | (len CR)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(Rev r1) | (len CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
Rev ((Rev r1) | (len CR)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
Rev (Rev r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(Rev (Rev r1)) /^ ((len (Rev r1)) -' (len CR)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(len r1) -' (len CR) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
r1 /^ ((len r1) -' (len CR)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlpart (r1,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 | ((len r1) -' (len CR)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(r1 | ((len r1) -' (len CR))) ^ CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlpart (((r1 | ((len r1) -' (len CR))) ^ CR),CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlcon (r1,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (ovlpart (r1,CR)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
CR /^ (len (ovlpart (r1,CR))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 ^ (CR /^ (len (ovlpart (r1,CR)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 ^ {} is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
((len r1) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
mid (r1,(((len r1) + 1) -' 1),(len r1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
mid (r1,(len r1),(len r1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(len r1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
r1 /^ ((len r1) -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 | ((len r1) -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(r1 | ((len r1) -' 1)) ^ CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR /^ (len CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlcon (r1,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlpart (r1,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (ovlpart (r1,CR)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
CR /^ (len (ovlpart (r1,CR))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 ^ (CR /^ (len (ovlpart (r1,CR)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 ^ (CR /^ (len CR)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlpart (r1,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (ovlpart (r1,CR)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
<*> D is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() FinSequence of D
len (<*> D) is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() Element of NAT
ovlcon (r1,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR /^ (len (ovlpart (r1,CR))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 ^ (CR /^ (len (ovlpart (r1,CR)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 ^ CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
addcr (r1,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
Rev CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (Rev CR) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
Rev r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
Rev r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (Rev r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) - 1 is V11() ext-real V43() set
(len CR) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(len r1) + 1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len r1) + 1) - (len CR) is V11() ext-real V43() set
((len r1) + 1) -' (len CR) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(len r1) - (len CR) is V11() ext-real V43() set
(len r1) -' (len CR) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
r1 /^ ((len r1) -' (len CR)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (r1 /^ ((len r1) -' (len CR))) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len r1) -' ((len r1) -' (len CR)) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(len r1) - ((len r1) -' (len CR)) is V11() ext-real V43() set
instr (1,r1,CR) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(((len r1) + 1) -' (len CR)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
r1 /^ ((((len r1) + 1) -' (len CR)) -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
mid ((r1 /^ ((((len r1) + 1) -' (len CR)) -' 1)),1,(len CR)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((len CR) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(r1 /^ ((((len r1) + 1) -' (len CR)) -' 1)) /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((r1 /^ ((((len r1) + 1) -' (len CR)) -' 1)) /^ (1 -' 1)) | (((len CR) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(r1 /^ ((((len r1) + 1) -' (len CR)) -' 1)) /^ 0 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((r1 /^ ((((len r1) + 1) -' (len CR)) -' 1)) /^ 0) | (((len CR) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(len r1) - ((len r1) - (len CR)) is V11() ext-real V43() set
(((len r1) + 1) -' (len CR)) - 1 is V11() ext-real V43() set
(r1 /^ ((len r1) -' (len CR))) | (len CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
mid ((Rev r1),1,(len CR)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(Rev r1) /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((Rev r1) /^ (1 -' 1)) | (((len CR) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(Rev r1) /^ 0 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((Rev r1) /^ 0) | (len CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(Rev r1) | ((len r1) -' ((len r1) -' (len CR))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
Rev (r1 /^ ((len r1) -' (len CR))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
Rev CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (Rev CR) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
mid ((Rev r1),1,(len (Rev CR))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
addcr (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (addcr (CR,r1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
ovlcon (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (ovlcon (CR,r1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
ovlpart (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (ovlpart (CR,r1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len r1) -' (len (ovlpart (CR,r1))) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(len CR) + ((len r1) -' (len (ovlpart (CR,r1)))) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) -' (len (ovlpart (CR,r1))) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
CR | ((len CR) -' (len (ovlpart (CR,r1)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR | ((len CR) -' (len (ovlpart (CR,r1))))) ^ r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (CR | ((len CR) -' (len (ovlpart (CR,r1))))) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len (CR | ((len CR) -' (len (ovlpart (CR,r1)))))) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
D is non empty set
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlpart (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlrdiff (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(ovlpart (CR,r1)) ^ (ovlrdiff (CR,r1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (ovlpart (CR,r1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
smid (r1,1,(len (ovlpart (CR,r1)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 | (len (ovlpart (CR,r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 /^ (len (ovlpart (CR,r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(r1 | (len (ovlpart (CR,r1)))) ^ (r1 /^ (len (ovlpart (CR,r1)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlcon (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlldiff (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(ovlldiff (CR,r1)) ^ r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlpart (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlrdiff (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(ovlpart (CR,r1)) ^ (ovlrdiff (CR,r1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(ovlldiff (CR,r1)) ^ ((ovlpart (CR,r1)) ^ (ovlrdiff (CR,r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
addcr (r1,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlldiff (r1,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(ovlldiff (r1,CR)) ^ CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlcon (r1,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlpart (r1,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlrdiff (r1,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(ovlpart (r1,CR)) ^ (ovlrdiff (r1,CR)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(ovlldiff (r1,CR)) ^ ((ovlpart (r1,CR)) ^ (ovlrdiff (r1,CR))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (CR ^ r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) + 0 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
r1 | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
Seg (len r1) is V32() V39( len r1) Element of K6(NAT)
r1 | (Seg (len r1)) is Relation-like NAT -defined Seg (len r1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((len CR) + (len r1)) -' (len CR) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((len CR) + (len r1)) - (len CR) is V11() ext-real V43() set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(len CR) + 1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
mid ((CR ^ r1),((len CR) + 1),(len (CR ^ r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(len (CR ^ r1)) -' ((len CR) + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((len (CR ^ r1)) -' ((len CR) + 1)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
((len CR) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(CR ^ r1) /^ (((len CR) + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR ^ r1) /^ (((len CR) + 1) -' 1)) | (((len (CR ^ r1)) -' ((len CR) + 1)) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR ^ r1) /^ (len CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR ^ r1) /^ (len CR)) | (((len (CR ^ r1)) -' ((len CR) + 1)) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((len CR) + (len r1)) -' ((len CR) + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(((len CR) + (len r1)) -' ((len CR) + 1)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
((CR ^ r1) /^ (len CR)) | ((((len CR) + (len r1)) -' ((len CR) + 1)) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR ^ r1) /^ (len CR)) | (((len CR) + (len r1)) -' (len CR)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
f is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(((len CR) + 1) -' 1) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
f is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
f -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(f -' 1) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
mid ((CR ^ r1),f,((f -' 1) + (len r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
mid ((CR ^ r1),1,(len CR)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(len CR) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((len CR) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(CR ^ r1) /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR ^ r1) /^ (1 -' 1)) | (((len CR) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR ^ r1) /^ 0 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR ^ r1) /^ 0) | (((len CR) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR ^ r1) /^ 0) | (len CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR ^ r1) | (len CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(1 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
0 + (len CR) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
f is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
f -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(f -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
mid ((CR ^ r1),f,((f -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR ^ r1) ^ r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (CR ^ r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len CR) + (len r1)) -' (len CR) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((len CR) + (len r1)) - (len CR) is V11() ext-real V43() set
(len CR) + 0 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(len CR) + 1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
mid (((CR ^ r1) ^ r2),((len CR) + 1),(len (CR ^ r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(len (CR ^ r1)) -' ((len CR) + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((len (CR ^ r1)) -' ((len CR) + 1)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
((len CR) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((CR ^ r1) ^ r2) /^ (((len CR) + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(((CR ^ r1) ^ r2) /^ (((len CR) + 1) -' 1)) | (((len (CR ^ r1)) -' ((len CR) + 1)) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR ^ r1) ^ r2) /^ (len CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(((CR ^ r1) ^ r2) /^ (len CR)) | (((len (CR ^ r1)) -' ((len CR) + 1)) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((len CR) + (len r1)) -' ((len CR) + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(((len CR) + (len r1)) -' ((len CR) + 1)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(((CR ^ r1) ^ r2) /^ (len CR)) | ((((len CR) + (len r1)) -' ((len CR) + 1)) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(((CR ^ r1) ^ r2) /^ (len CR)) | (((len CR) + (len r1)) -' (len CR)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 ^ r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ (r1 ^ r2) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR ^ (r1 ^ r2)) /^ (len CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR ^ (r1 ^ r2)) /^ (len CR)) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(r1 ^ r2) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((len CR) + 1) + 0 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len CR) + (len r1)) + (len r2) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len ((CR ^ r1) ^ r2) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(((len CR) + 1) -' 1) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
f2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
f2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
f2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(f2 -' 1) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
mid (((CR ^ r1) ^ r2),f2,((f2 -' 1) + (len r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 ^ r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ (r1 ^ r2) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 ^ r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
addcr ((r1 ^ r2),CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
addcr (r2,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlcon (r2,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlpart (r2,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (ovlpart (r2,CR)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
CR /^ (len (ovlpart (r2,CR))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 ^ (CR /^ (len (ovlpart (r2,CR)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
addcr (r1,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlcon (r1,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
ovlpart (r1,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (ovlpart (r1,CR)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len r1) -' (len (ovlpart (r1,CR))) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
r1 | ((len r1) -' (len (ovlpart (r1,CR)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(r1 | ((len r1) -' (len (ovlpart (r1,CR))))) ^ CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((r1 | ((len r1) -' (len (ovlpart (r1,CR))))) ^ CR) ^ (r2 ^ (CR /^ (len (ovlpart (r2,CR))))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlcon ((r1 ^ r2),CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlpart ((r1 ^ r2),CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (ovlpart ((r1 ^ r2),CR)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
CR /^ (len (ovlpart ((r1 ^ r2),CR))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(r1 ^ r2) ^ (CR /^ (len (ovlpart ((r1 ^ r2),CR)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(r1 | ((len r1) -' (len (ovlpart (r1,CR))))) ^ (CR ^ r2) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((r1 | ((len r1) -' (len (ovlpart (r1,CR))))) ^ (CR ^ r2)) ^ (CR /^ (len (ovlpart (r2,CR)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(((r1 | ((len r1) -' (len (ovlpart (r1,CR))))) ^ (CR ^ r2)) ^ (CR /^ (len (ovlpart (r2,CR))))) ^ (CR /^ (len (ovlpart ((r1 ^ r2),CR)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR /^ (len (ovlpart (r2,CR)))) ^ (CR /^ (len (ovlpart ((r1 ^ r2),CR)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((r1 | ((len r1) -' (len (ovlpart (r1,CR))))) ^ (CR ^ r2)) ^ ((CR /^ (len (ovlpart (r2,CR)))) ^ (CR /^ (len (ovlpart ((r1 ^ r2),CR))))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
instr (r2,CR,r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
r2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
CR /^ (r2 -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
instr (r2,CR,r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) + 1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len CR) + 1) - 1 is V11() ext-real V43() set
(instr (r2,CR,r1)) - 1 is V11() ext-real V43() set
(instr (r2,CR,r1)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
CR /^ ((instr (r2,CR,r1)) -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (CR /^ ((instr (r2,CR,r1)) -' 1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlcon (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
ovlpart (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (ovlpart (CR,r1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) -' (len (ovlpart (CR,r1))) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
((len CR) -' (len (ovlpart (CR,r1)))) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
((len CR) -' (len (ovlpart (CR,r1)))) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(((len CR) -' (len (ovlpart (CR,r1)))) + (len r1)) -' (((len CR) -' (len (ovlpart (CR,r1)))) + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((((len CR) -' (len (ovlpart (CR,r1)))) + (len r1)) -' (((len CR) -' (len (ovlpart (CR,r1)))) + 1)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(((len CR) -' (len (ovlpart (CR,r1)))) + (len r1)) - (((len CR) -' (len (ovlpart (CR,r1)))) + 1) is V11() ext-real V43() set
((((len CR) -' (len (ovlpart (CR,r1)))) + (len r1)) - (((len CR) -' (len (ovlpart (CR,r1)))) + 1)) + 1 is V11() ext-real V43() set
1 - (len (ovlpart (CR,r1))) is V11() ext-real V43() set
(len r1) - (len (ovlpart (CR,r1))) is V11() ext-real V43() set
(1 - (len (ovlpart (CR,r1)))) + (len CR) is V11() ext-real V43() set
((len r1) - (len (ovlpart (CR,r1)))) + (len CR) is V11() ext-real V43() set
(len CR) - (len (ovlpart (CR,r1))) is V11() ext-real V43() set
((len CR) - (len (ovlpart (CR,r1)))) + 1 is V11() ext-real V43() set
(len CR) + ((len r1) - (len (ovlpart (CR,r1)))) is V11() ext-real V43() set
CR | ((len CR) -' (len (ovlpart (CR,r1)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (CR | ((len CR) -' (len (ovlpart (CR,r1))))) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(CR | ((len CR) -' (len (ovlpart (CR,r1))))) /^ ((len CR) -' (len (ovlpart (CR,r1)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((len CR) -' (len (ovlpart (CR,r1)))) -' ((len CR) -' (len (ovlpart (CR,r1)))) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
CR /^ ((len CR) -' (len (ovlpart (CR,r1)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR /^ ((len CR) -' (len (ovlpart (CR,r1))))) | (((len CR) -' (len (ovlpart (CR,r1)))) -' ((len CR) -' (len (ovlpart (CR,r1))))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR /^ ((len CR) -' (len (ovlpart (CR,r1))))) | 0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() FinSequence of D
r1 /^ (len (ovlpart (CR,r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (r1 /^ (len (ovlpart (CR,r1)))) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len r1) -' (len (ovlpart (CR,r1))) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
CR ^ (r1 /^ (len (ovlpart (CR,r1)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(len CR) + (len (r1 /^ (len (ovlpart (CR,r1))))) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len (ovlcon (CR,r1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(((len CR) -' (len (ovlpart (CR,r1)))) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((((len CR) -' (len (ovlpart (CR,r1)))) + 1) -' 1) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
mid ((ovlcon (CR,r1)),(((len CR) -' (len (ovlpart (CR,r1)))) + 1),(((((len CR) -' (len (ovlpart (CR,r1)))) + 1) -' 1) + (len r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR | ((len CR) -' (len (ovlpart (CR,r1))))) ^ r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
mid (((CR | ((len CR) -' (len (ovlpart (CR,r1))))) ^ r1),(((len CR) -' (len (ovlpart (CR,r1)))) + 1),(((((len CR) -' (len (ovlpart (CR,r1)))) + 1) -' 1) + (len r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
mid (((CR | ((len CR) -' (len (ovlpart (CR,r1))))) ^ r1),(((len CR) -' (len (ovlpart (CR,r1)))) + 1),(((len CR) -' (len (ovlpart (CR,r1)))) + (len r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR | ((len CR) -' (len (ovlpart (CR,r1))))) ^ r1) /^ ((((len CR) -' (len (ovlpart (CR,r1)))) + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(((CR | ((len CR) -' (len (ovlpart (CR,r1))))) ^ r1) /^ ((((len CR) -' (len (ovlpart (CR,r1)))) + 1) -' 1)) | (((((len CR) -' (len (ovlpart (CR,r1)))) + (len r1)) -' (((len CR) -' (len (ovlpart (CR,r1)))) + 1)) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR | ((len CR) -' (len (ovlpart (CR,r1))))) ^ r1) /^ ((len CR) -' (len (ovlpart (CR,r1)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(((CR | ((len CR) -' (len (ovlpart (CR,r1))))) ^ r1) /^ ((len CR) -' (len (ovlpart (CR,r1))))) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR | ((len CR) -' (len (ovlpart (CR,r1))))) /^ ((len CR) -' (len (ovlpart (CR,r1))))) ^ r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(((CR | ((len CR) -' (len (ovlpart (CR,r1))))) /^ ((len CR) -' (len (ovlpart (CR,r1))))) ^ r1) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
addcr (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlcon (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
r2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
CR | r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (CR | r2) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
f is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
f -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(f -' 1) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
mid ((CR | r2),f,((f -' 1) + (len r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(len r1) - 1 is V11() ext-real V43() set
0 + f is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len r1) - 1) + f is V11() ext-real V43() set
f - 1 is V11() ext-real V43() set
(f - 1) + (len r1) is V11() ext-real V43() set
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((f -' 1) + (len r1)) -' f is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(((f -' 1) + (len r1)) -' f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
((f - 1) + (len r1)) - f is V11() ext-real V43() set
(((f - 1) + (len r1)) - f) + 1 is V11() ext-real V43() set
(CR | r2) /^ (f -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR | r2) /^ (f -' 1)) | ((((f -' 1) + (len r1)) -' f) + 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 -' (f -' 1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
CR /^ (f -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(CR /^ (f -' 1)) | (r2 -' (f -' 1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((CR /^ (f -' 1)) | (r2 -' (f -' 1))) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (CR /^ (f -' 1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len CR) -' (f -' 1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(CR /^ (f -' 1)) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
mid (CR,f,((f -' 1) + (len r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
addcr (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
instr (1,(addcr (CR,r1)),r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(instr (1,(addcr (CR,r1)),r1)) - 1 is V11() ext-real V43() set
(instr (1,(addcr (CR,r1)),r1)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
<*> D is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(instr (1,(addcr (CR,r1)),r1)) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(addcr (CR,r1)) /^ ((instr (1,(addcr (CR,r1)),r1)) -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
<*> D is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() FinSequence of D
ovlpart (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (ovlpart (CR,r1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
r1 /^ (len (ovlpart (CR,r1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ (r1 /^ (len (ovlpart (CR,r1)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlcon (CR,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
mid (CR,1,(len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) | (len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(addcr (CR,r1)) | (len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR | (len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR | (len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(addcr (CR,r1)) | (len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len ((addcr (CR,r1)) /^ ((instr (1,(addcr (CR,r1)),r1)) -' 1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len (addcr (CR,r1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len (addcr (CR,r1))) - ((instr (1,(addcr (CR,r1)),r1)) -' 1) is V11() ext-real V43() set
(len r1) + ((instr (1,(addcr (CR,r1)),r1)) -' 1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
mid (((addcr (CR,r1)) /^ ((instr (1,(addcr (CR,r1)),r1)) -' 1)),1,(len r1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((addcr (CR,r1)) /^ ((instr (1,(addcr (CR,r1)),r1)) -' 1)) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len r1) + 0 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len r1) + ((instr (1,(addcr (CR,r1)),r1)) - 1) is V11() ext-real V43() set
(len r1) + (instr (1,(addcr (CR,r1)),r1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len r1) + (instr (1,(addcr (CR,r1)),r1))) - 1 is V11() ext-real V43() set
len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((instr (1,(addcr (CR,r1)),r1)) + (len r1)) - 1 is V11() ext-real V43() set
(len r1) + (instr (1,(addcr (CR,r1)),r1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len r1) + (instr (1,(addcr (CR,r1)),r1))) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1))) + 1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1))) + 1) -' (len r1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(((len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1))) + 1) -' (len r1)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) /^ ((((len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1))) + 1) -' (len r1)) -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) /^ ((instr (1,(addcr (CR,r1)),r1)) -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) /^ ((instr (1,(addcr (CR,r1)),r1)) -' 1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1))) - ((instr (1,(addcr (CR,r1)),r1)) -' 1) is V11() ext-real V43() set
(((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1) - ((instr (1,(addcr (CR,r1)),r1)) -' 1) is V11() ext-real V43() set
(((instr (1,(addcr (CR,r1)),r1)) + (len r1)) - 1) - ((instr (1,(addcr (CR,r1)),r1)) - 1) is V11() ext-real V43() set
(((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1) -' ((instr (1,(addcr (CR,r1)),r1)) -' 1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) /^ ((instr (1,(addcr (CR,r1)),r1)) -' 1)) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
mid ((((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) /^ ((instr (1,(addcr (CR,r1)),r1)) -' 1)),1,(len r1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(((instr (1,(addcr (CR,r1)),r1)) + (len r1)) - 1) + 1 is V11() ext-real V43() set
((instr (1,(addcr (CR,r1)),r1)) + (len r1)) - (len r1) is V11() ext-real V43() set
((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' (len r1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
j is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
j -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) /^ (j -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) /^ (j -' 1)) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(j -' 1) + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((j -' 1) + (len r1)) -' (j -' 1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) /^ (j -' 1)) | (((j -' 1) + (len r1)) -' (j -' 1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(len r1) + (j -' 1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) | ((len r1) + (j -' 1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) | ((len r1) + (j -' 1))) /^ (j -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
mid ((((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) /^ (j -' 1)),1,(len r1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
j - 1 is V11() ext-real V43() set
(addcr (CR,r1)) /^ (j -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len ((addcr (CR,r1)) /^ (j -' 1)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
j + (len r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(j + (len r1)) - 1 is V11() ext-real V43() set
(j + (len r1)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(len r1) + (j - 1) is V11() ext-real V43() set
((((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1) + 1) -' (len r1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
((addcr (CR,r1)) /^ (j -' 1)) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((addcr (CR,r1)) /^ (j -' 1)) | (((j -' 1) + (len r1)) -' (j -' 1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(addcr (CR,r1)) | ((len r1) + (j -' 1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((addcr (CR,r1)) | ((len r1) + (j -' 1))) /^ (j -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) | ((j + (len r1)) -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) | ((j + (len r1)) -' 1)) /^ (j -' 1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
mid (((addcr (CR,r1)) /^ (j -' 1)),1,(len r1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
((instr (1,(addcr (CR,r1)),r1)) + (len r1)) - (len r1) is V11() ext-real V43() set
((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' (len r1) is V4() V5() V6() V10() V11() ext-real non negative V32() V37() V43() Element of NAT
(((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(((instr (1,(addcr (CR,r1)),r1)) + (len r1)) - 1) + 1 is V11() ext-real V43() set
instr (1,((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)),r1) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
(addcr (CR,r1)) | (len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
mid ((addcr (CR,r1)),1,(len ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 ^ ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 ^ ((addcr (CR,r1)) | (((instr (1,(addcr (CR,r1)),r1)) + (len r1)) -' 1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
D is non empty set
r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
addcr (r2,r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
r1 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
f is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 ^ r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
addcr (f,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
addcr (f,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
1 + 0 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(len r1) + (len r2) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len f is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
addcr (f,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
mid ((addcr (f,CR)),1,(len r1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(addcr (f,CR)) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlcon (f,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(ovlcon (f,CR)) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlpart (f,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (ovlpart (f,CR)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
CR /^ (len (ovlpart (f,CR))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
f ^ (CR /^ (len (ovlpart (f,CR)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(f ^ (CR /^ (len (ovlpart (f,CR))))) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 ^ (CR /^ (len (ovlpart (f,CR)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 ^ (r2 ^ (CR /^ (len (ovlpart (f,CR))))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(r1 ^ (r2 ^ (CR /^ (len (ovlpart (f,CR)))))) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (addcr (f,CR)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
1 + 0 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
(len r1) + (len r2) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len f is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V37() V43() Element of NAT
addcr (f,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
mid ((addcr (f,CR)),1,(len r1)) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(addcr (f,CR)) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlcon (f,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(ovlcon (f,CR)) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
ovlpart (f,CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (ovlpart (f,CR)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
CR /^ (len (ovlpart (f,CR))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
f ^ (CR /^ (len (ovlpart (f,CR)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(f ^ (CR /^ (len (ovlpart (f,CR))))) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r2 ^ (CR /^ (len (ovlpart (f,CR)))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 ^ (r2 ^ (CR /^ (len (ovlpart (f,CR))))) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
(r1 ^ (r2 ^ (CR /^ (len (ovlpart (f,CR)))))) | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
r1 | (len r1) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len (addcr (f,CR)) is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
addcr ((r1 ^ r2),CR) is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
CR ^ r2 is Relation-like NAT -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of D
len r1 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT
len r2 is V4() V5() V6() V10() V11() ext-real V32() V37() V43() Element of NAT