REAL is set
NAT is non empty V4() V5() V6() V26() V31() V32() Element of K6(REAL)
K6(REAL) is non empty set
NAT is non empty V4() V5() V6() V26() V31() V32() set
K6(NAT) is non empty V26() set
K6(NAT) is non empty V26() set
COMPLEX is set
RAT is set
INT is set
1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
K7(1,1) is non empty V13() set
K6(K7(1,1)) is non empty set
K7(K7(1,1),1) is non empty V13() set
K6(K7(K7(1,1),1)) is non empty set
K7(K7(1,1),REAL) is V13() set
K6(K7(K7(1,1),REAL)) is non empty set
K7(REAL,REAL) is V13() set
K7(K7(REAL,REAL),REAL) is V13() set
K6(K7(K7(REAL,REAL),REAL)) is non empty set
2 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
K7(2,2) is non empty V13() set
K7(K7(2,2),REAL) is V13() set
K6(K7(K7(2,2),REAL)) is non empty set
K6(K7(REAL,REAL)) is non empty set
TOP-REAL 2 is non empty V74() TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict RLTopStruct
the U1 of (TOP-REAL 2) is non empty V2() set
K304( the U1 of (TOP-REAL 2)) is non empty functional FinSequence-membered M13( the U1 of (TOP-REAL 2))
K6( the U1 of (TOP-REAL 2)) is non empty set
{} is set
the empty V2() V4() V5() V6() V8() V9() V10() V11() V12() V13() non-empty empty-yielding V16( NAT ) Function-like one-to-one constant functional V26() V31() V33( {} ) FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative set is empty V2() V4() V5() V6() V8() V9() V10() V11() V12() V13() non-empty empty-yielding V16( NAT ) Function-like one-to-one constant functional V26() V31() V33( {} ) FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative set
3 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
K7(NAT, the U1 of (TOP-REAL 2)) is non empty V13() V26() set
0 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Seg 1 is non empty V2() V26() V33(1) Element of K6(NAT)
{1} is non empty V2() V33(1) set
Seg 2 is non empty V26() V33(2) Element of K6(NAT)
{1,2} is set
4 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (L_Cut (n,C)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
0 + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
R_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (R_Cut (n,C)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
0 + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
p is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
B_Cut (n,C,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L_Cut (n,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
R_Cut ((L_Cut (n,p)),C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
R_Cut ((L_Cut (n,C)),p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
Rev (R_Cut ((L_Cut (n,p)),C)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n is set
<*n*> is non empty V2() V13() V16( NAT ) Function-like constant V26() V33(1) FinSequence-like FinSubsequence-like set
n is set
C is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
dom C is Element of K6(NAT)
len C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
p is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
q is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C /. p is Element of n
C /. q is Element of n
C . p is set
C . q is set
p is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
q is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C . p is set
C . q is set
C /. p is Element of n
C /. q is Element of n
n is set
C is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
len C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
p is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C /. p is Element of n
p + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C /. (p + 1) is Element of n
C . (p + 1) is set
C . p is set
p is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
p + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C . (p + 1) is set
C /. (p + 1) is Element of n
C . p is set
C /. p is Element of n
n is set
C is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
len C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
p is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C /. p is Element of n
p + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C /. (p + 1) is Element of n
C . (p + 1) is set
C . p is set
p is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
p + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C . (p + 1) is set
C /. (p + 1) is Element of n
C . p is set
C /. p is Element of n
n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom n is Element of K6(NAT)
p is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . C is set
n . p is set
n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom n is Element of K6(NAT)
n . C is set
n . (C + 1) is set
C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . C is set
C + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . (C + 1) is set
C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . C is set
C + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . (C + 1) is set
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . C is set
C + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . (C + 1) is set
C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . C is set
C + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . (C + 1) is set
n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . C is set
C + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . (C + 1) is set
n is set
<*n*> is non empty V2() V13() V16( NAT ) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like () () set
C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len <*n*> is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
<*n*> . C is set
C + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
<*n*> . (C + 1) is set
n is set
C is set
<*n,C*> is non empty V13() V16( NAT ) Function-like V26() V33(2) FinSequence-like FinSubsequence-like set
len <*n,C*> is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
the set is set
<* the set *> is non empty V2() V13() V16( NAT ) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like () () () set
len <* the set *> is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n is non empty set
the Element of n is Element of n
<* the Element of n*> is non empty V2() V13() V16( NAT ) V17(n) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like () () () FinSequence of n
<* the Element of n*> /. 1 is Element of n
len <* the Element of n*> is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
<* the Element of n*> /. (len <* the Element of n*>) is Element of n
n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
Rev n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom (Rev n) is Element of K6(NAT)
p is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len (Rev n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Rev n) . C is set
(Rev n) . p is set
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len n) - C is V11() V12() ext-real Element of REAL
((len n) - C) + 1 is V11() V12() ext-real Element of REAL
(len n) - p is V11() V12() ext-real Element of REAL
((len n) - p) + 1 is V11() V12() ext-real Element of REAL
dom n is Element of K6(NAT)
Seg (len n) is V26() V33( len n) Element of K6(NAT)
n . (((len n) - p) + 1) is set
n . (((len n) - C) + 1) is set
n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
Rev n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len (Rev n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Rev n) . C is set
C + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Rev n) . (C + 1) is set
Seg (len (Rev n)) is V26() V33( len (Rev n)) Element of K6(NAT)
dom (Rev n) is Element of K6(NAT)
(len n) - (C + 1) is V11() V12() ext-real Element of REAL
((len n) - (C + 1)) + 1 is V11() V12() ext-real Element of REAL
n . (((len n) - (C + 1)) + 1) is set
(len n) - C is V11() V12() ext-real Element of REAL
((len n) - C) + 1 is V11() V12() ext-real Element of REAL
n . (((len n) - C) + 1) is set
Seg (len n) is V26() V33( len n) Element of K6(NAT)
p is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
p + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
Rev n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len (Rev n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
the set is set
<* the set *> is non empty V2() V13() V16( NAT ) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like () () () set
n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like () () set
Rev n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like () set
Rev n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like () set
Rev n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
n is non empty set
C is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
p is Element of n
Rotate (C,p) is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
rng C is set
0 + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
p .. C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(p .. C) - 1 is V11() V12() ext-real Element of REAL
C :- p is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
len (C :- p) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len C) - (p .. C) is V11() V12() ext-real Element of REAL
((len C) - (p .. C)) + 1 is V11() V12() ext-real Element of REAL
q is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom (Rotate (C,p)) is Element of K6(NAT)
f is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len (Rotate (C,p)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Rotate (C,p)) . q is set
(Rotate (C,p)) . f is set
dom C is Element of K6(NAT)
q - (len C) is V11() V12() ext-real Element of REAL
(len C) - (len C) is V11() V12() ext-real Element of REAL
f - (len C) is V11() V12() ext-real Element of REAL
f - 1 is V11() V12() ext-real Element of REAL
q -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
(q -' 1) + (p .. C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
f -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
(f -' 1) + (p .. C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(f -' 1) + ((p .. C) - 1) is V11() V12() ext-real Element of REAL
q - 1 is V11() V12() ext-real Element of REAL
(q -' 1) + ((p .. C) - 1) is V11() V12() ext-real Element of REAL
dom (C :- p) is Element of K6(NAT)
(q -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
(Rotate (C,p)) /. q is Element of n
C /. ((q -' 1) + (p .. C)) is Element of n
(f -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
(Rotate (C,p)) /. f is Element of n
C /. ((f -' 1) + (p .. C)) is Element of n
C . ((q -' 1) + (p .. C)) is set
C . ((f -' 1) + (p .. C)) is set
(Rotate (C,p)) /. f is Element of n
f + (p .. C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(f + (p .. C)) -' (len C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
C /. ((f + (p .. C)) -' (len C)) is Element of n
f - ((len C) - (p .. C)) is V11() V12() ext-real Element of REAL
(f + (p .. C)) - (len C) is V11() V12() ext-real Element of REAL
(len C) + (len C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C . ((q -' 1) + (p .. C)) is set
C . ((f + (p .. C)) -' (len C)) is set
q - ((len C) - (p .. C)) is V11() V12() ext-real Element of REAL
q + (p .. C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len C) + (len C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(q + (p .. C)) - (len C) is V11() V12() ext-real Element of REAL
(q + (p .. C)) -' (len C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
(Rotate (C,p)) /. q is Element of n
C /. ((q + (p .. C)) -' (len C)) is Element of n
(Rotate (C,p)) /. f is Element of n
C /. ((f -' 1) + (p .. C)) is Element of n
dom (C :- p) is Element of K6(NAT)
(f -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
C . ((f -' 1) + (p .. C)) is set
C . ((q + (p .. C)) -' (len C)) is set
(Rotate (C,p)) /. f is Element of n
f + (p .. C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(f + (p .. C)) -' (len C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
C /. ((f + (p .. C)) -' (len C)) is Element of n
f - ((len C) - (p .. C)) is V11() V12() ext-real Element of REAL
(f + (p .. C)) - (len C) is V11() V12() ext-real Element of REAL
C . ((q + (p .. C)) -' (len C)) is set
C . ((f + (p .. C)) -' (len C)) is set
rng C is set
rng C is set
n is non empty set
C is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
p is Element of n
Rotate (C,p) is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
rng C is set
p .. C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C :- p is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
len (C :- p) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len C) - (p .. C) is V11() V12() ext-real Element of REAL
((len C) - (p .. C)) + 1 is V11() V12() ext-real Element of REAL
q is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len (Rotate (C,p)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Rotate (C,p)) . q is set
q + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Rotate (C,p)) . (q + 1) is set
0 + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
q -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
(q -' 1) + (p .. C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
((q -' 1) + (p .. C)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
q - 1 is V11() V12() ext-real Element of REAL
(q - 1) + 1 is V11() V12() ext-real Element of REAL
1 - 1 is V11() V12() ext-real Element of REAL
(q + 1) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
((q + 1) -' 1) + (p .. C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(q + 1) - 1 is V11() V12() ext-real Element of REAL
((q + 1) - 1) + (p .. C) is V11() V12() ext-real Element of REAL
(q - 1) + (p .. C) is V11() V12() ext-real Element of REAL
((q - 1) + (p .. C)) + 1 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
(Rotate (C,p)) /. q is Element of n
C /. ((q -' 1) + (p .. C)) is Element of n
C . ((q -' 1) + (p .. C)) is set
(Rotate (C,p)) /. (q + 1) is Element of n
C /. (((q + 1) -' 1) + (p .. C)) is Element of n
C . (((q + 1) -' 1) + (p .. C)) is set
(Rotate (C,p)) /. q is Element of n
C /. (len C) is Element of n
C /. 1 is Element of n
C . 1 is set
(q + 1) + (p .. C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
((q + 1) + (p .. C)) -' (len C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
(len C) + (1 + 1) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
((len C) + (1 + 1)) - (len C) is V11() V12() ext-real Element of REAL
(Rotate (C,p)) /. (q + 1) is Element of n
C /. (((q + 1) + (p .. C)) -' (len C)) is Element of n
C . (((q + 1) + (p .. C)) -' (len C)) is set
C . (1 + 1) is set
q - ((len C) - (p .. C)) is V11() V12() ext-real Element of REAL
q + (p .. C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(q + (p .. C)) - (len C) is V11() V12() ext-real Element of REAL
((q + (p .. C)) - (len C)) + 1 is V11() V12() ext-real Element of REAL
(q + 1) + (p .. C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
((q + 1) + (p .. C)) -' (len C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
((q + 1) + (p .. C)) - (len C) is V11() V12() ext-real Element of REAL
(q + (p .. C)) -' (len C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
((q + (p .. C)) -' (len C)) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
(len C) + (len C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Rotate (C,p)) /. (q + 1) is Element of n
C /. (((q + 1) + (p .. C)) -' (len C)) is Element of n
C . (((q + 1) + (p .. C)) -' (len C)) is set
(Rotate (C,p)) /. q is Element of n
C /. ((q + (p .. C)) -' (len C)) is Element of n
C . ((q + (p .. C)) -' (len C)) is set
rng C is set
rng C is set
n is non empty set
C is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
p is Element of n
Rotate (C,p) is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
len (Rotate (C,p)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n is non empty set
the Element of n is Element of n
<* the Element of n*> is non empty V2() V13() V16( NAT ) V17(n) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like () () () FinSequence of n
<* the Element of n*> /. 1 is Element of n
len <* the Element of n*> is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
<* the Element of n*> /. (len <* the Element of n*>) is Element of n
n is non empty set
C is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like () () FinSequence of n
p is Element of n
Rotate (C,p) is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
n is non empty set
C is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like circular () FinSequence of n
p is Element of n
Rotate (C,p) is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
n is non empty set
C is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like circular () FinSequence of n
p is Element of n
Rotate (C,p) is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
n is non empty set
C is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
C /^ 1 is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
len C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len C) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
C | ((len C) -' 1) is V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
len (C /^ 1) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
p is set
K74((C /^ 1)) is set
q is set
(C /^ 1) . p is set
(C /^ 1) . q is set
dom (C /^ 1) is Element of K6(NAT)
f is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Seg (len (C /^ 1)) is V26() V33( len (C /^ 1)) Element of K6(NAT)
(len C) - 1 is V11() V12() ext-real Element of REAL
f + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(C /^ 1) . f is set
C . (f + 1) is set
Lf is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Lf + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(C /^ 1) . Lf is set
C . (Lf + 1) is set
dom C is Element of K6(NAT)
len (C | ((len C) -' 1)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
p is set
K74((C | ((len C) -' 1))) is set
q is set
(C | ((len C) -' 1)) . p is set
(C | ((len C) -' 1)) . q is set
dom (C | ((len C) -' 1)) is Element of K6(NAT)
f is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Seg (len (C | ((len C) -' 1))) is V26() V33( len (C | ((len C) -' 1))) Element of K6(NAT)
Lf is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(C | ((len C) -' 1)) . Lf is set
C . Lf is set
(C | ((len C) -' 1)) . f is set
C . f is set
(len C) - 1 is V11() V12() ext-real Element of REAL
Lf + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom C is Element of K6(NAT)
f + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
p is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom C is Element of K6(NAT)
q is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C . p is set
C . q is set
0 + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
p - 1 is V11() V12() ext-real Element of REAL
(len C) - 1 is V11() V12() ext-real Element of REAL
p -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
((len C) -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
len (C | ((len C) -' 1)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
q - 1 is V11() V12() ext-real Element of REAL
q -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
C /. 1 is Element of n
<*(C /. 1)*> is non empty V2() V13() V16( NAT ) V17(n) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like () () () FinSequence of n
<*(C /. 1)*> ^ (C /^ 1) is non empty V13() V16( NAT ) V17(n) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
(p -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
(q -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
dom (C /^ 1) is Element of K6(NAT)
(C /^ 1) . (q -' 1) is set
(C /^ 1) . (p -' 1) is set
q + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(C | ((len C) -' 1)) . q is set
dom (C | ((len C) -' 1)) is Element of K6(NAT)
(C | ((len C) -' 1)) . p is set
p + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(C | ((len C) -' 1)) . p is set
dom (C | ((len C) -' 1)) is Element of K6(NAT)
(C | ((len C) -' 1)) . q is set
n is non empty compact non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))
C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Cage (n,C) is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard V192() FinSequence of the U1 of (TOP-REAL 2)
len (Cage (n,C)) is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
0 + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len (Cage (n,C))) - 1 is V11() V12() ext-real Element of REAL
(len (Cage (n,C))) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
(len (Cage (n,C))) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Cage (n,C)) | ((len (Cage (n,C))) -' 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special unfolded FinSequence of the U1 of (TOP-REAL 2)
(Cage (n,C)) /^ 1 is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one V26() FinSequence-like FinSubsequence-like special unfolded () () FinSequence of the U1 of (TOP-REAL 2)
n is non empty compact non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))
C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Cage (n,C) is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard V192() () () FinSequence of the U1 of (TOP-REAL 2)
len (Cage (n,C)) is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
B_Cut (n,C,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
L_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
(L_Cut (n,C)) . 1 is set
R_Cut ((L_Cut (n,C)),C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom n is Element of K6(NAT)
n . (Index (C,n)) is set
n . ((Index (C,n)) + 1) is set
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg (n,(Index (C,n))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((n /. (Index (C,n))),(n /. ((Index (C,n)) + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. (Index (C,n)))) + (b1 * (n /. ((Index (C,n)) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . C is set
C + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . (C + 1) is set
dom n is Element of K6(NAT)
n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
p is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
B_Cut (n,C,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
B_Cut (n,p,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (B_Cut (n,p,C)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n /. (Index (p,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (p,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (p,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
R_Cut ((L_Cut (n,C)),p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (R_Cut ((L_Cut (n,C)),p)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (Rev (R_Cut ((L_Cut (n,C)),p))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
LSeg (n,(Index (C,n))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((n /. (Index (C,n))),(n /. ((Index (C,n)) + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. (Index (C,n)))) + (b1 * (n /. ((Index (C,n)) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
dom n is Element of K6(NAT)
n . (Index (C,n)) is set
n . ((Index (C,n)) + 1) is set
n /. (Index (p,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (p,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (p,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut (n,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
R_Cut ((L_Cut (n,p)),C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (R_Cut ((L_Cut (n,p)),C)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
p is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . p is set
q is V4() V5() V6() V10() V11() V12() V26() V31() ext-real set
q + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
1 + 0 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
f is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom n is Element of K6(NAT)
n /. p is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg (n,f) is Element of K6( the U1 of (TOP-REAL 2))
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
LSeg (n,(Index (C,n))) is Element of K6( the U1 of (TOP-REAL 2))
1 + 2 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
(Index (C,n)) + 2 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
2 + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
(Index (C,n)) + (1 + 1) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(LSeg (n,(Index (C,n)))) /\ (LSeg (n,f)) is Element of K6( the U1 of (TOP-REAL 2))
n /. f is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
{(n /. f)} is non empty V2() V33(1) set
n . f is set
(LSeg (n,(Index (C,n)))) /\ (LSeg (n,f)) is Element of K6( the U1 of (TOP-REAL 2))
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
p is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
B_Cut (n,C,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
(B_Cut (n,C,p)) /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom n is Element of K6(NAT)
L_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (L_Cut (n,C)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
L~ (L_Cut (n,C)) is compact Element of K6( the U1 of (TOP-REAL 2))
R_Cut ((L_Cut (n,C)),p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
(R_Cut ((L_Cut (n,C)),p)) /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(L_Cut (n,C)) /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(L_Cut (n,C)) . 1 is set
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L~ (L_Cut (n,C)) is compact Element of K6( the U1 of (TOP-REAL 2))
R_Cut ((L_Cut (n,C)),p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
(R_Cut ((L_Cut (n,C)),p)) /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(L_Cut (n,C)) /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(L_Cut (n,C)) . 1 is set
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut (n,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
R_Cut ((L_Cut (n,p)),C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (R_Cut ((L_Cut (n,p)),C)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (L_Cut (n,p)) is compact Element of K6( the U1 of (TOP-REAL 2))
len (R_Cut ((L_Cut (n,p)),C)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(R_Cut ((L_Cut (n,p)),C)) /. (len (R_Cut ((L_Cut (n,p)),C))) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg ((n /. (Index (C,n))),(n /. ((Index (C,n)) + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. (Index (C,n)))) + (b1 * (n /. ((Index (C,n)) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
n . (Index (C,n)) is set
n . ((Index (C,n)) + 1) is set
L~ (L_Cut (n,p)) is compact Element of K6( the U1 of (TOP-REAL 2))
len (R_Cut ((L_Cut (n,p)),C)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(R_Cut ((L_Cut (n,p)),C)) /. (len (R_Cut ((L_Cut (n,p)),C))) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
p is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
B_Cut (n,C,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (B_Cut (n,C,p)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(B_Cut (n,C,p)) /. (len (B_Cut (n,C,p))) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
B_Cut (n,p,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (B_Cut (n,p,C)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (B_Cut (n,p,C)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Rev (B_Cut (n,p,C))) /. (len (B_Cut (n,p,C))) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(B_Cut (n,p,C)) /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (L_Cut (n,C)) is compact Element of K6( the U1 of (TOP-REAL 2))
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
0 + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom n is Element of K6(NAT)
n . ((Index (C,n)) + 1) is set
mid (n,((Index (C,n)) + 1),(len n)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n . ((Index (C,n)) + 1) is set
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
mid (n,((Index (C,n)) + 1),(len n)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*C*> ^ (mid (n,((Index (C,n)) + 1),(len n))) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg ((n /. (Index (C,n))),(n /. ((Index (C,n)) + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. (Index (C,n)))) + (b1 * (n /. ((Index (C,n)) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (n,(Index (C,n))) is Element of K6( the U1 of (TOP-REAL 2))
(mid (n,((Index (C,n)) + 1),(len n))) /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg (C,((mid (n,((Index (C,n)) + 1),(len n))) /. 1)) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * C) + (b1 * ((mid (n,((Index (C,n)) + 1),(len n))) /. 1))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
len (mid (n,((Index (C,n)) + 1),(len n))) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
L~ (<*C*> ^ (mid (n,((Index (C,n)) + 1),(len n)))) is compact Element of K6( the U1 of (TOP-REAL 2))
L~ (mid (n,((Index (C,n)) + 1),(len n))) is compact Element of K6( the U1 of (TOP-REAL 2))
(LSeg (C,((mid (n,((Index (C,n)) + 1),(len n))) /. 1))) \/ (L~ (mid (n,((Index (C,n)) + 1),(len n)))) is Element of K6( the U1 of (TOP-REAL 2))
n . ((Index (C,n)) + 1) is set
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
p is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
B_Cut (n,C,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (B_Cut (n,C,p)) is compact Element of K6( the U1 of (TOP-REAL 2))
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
len (B_Cut (n,C,p)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom n is Element of K6(NAT)
LSeg (n,(Index (C,n))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((n /. (Index (C,n))),(n /. ((Index (C,n)) + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. (Index (C,n)))) + (b1 * (n /. ((Index (C,n)) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
n . (Index (C,n)) is set
n . ((Index (C,n)) + 1) is set
n /. (Index (p,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (p,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (p,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
B_Cut (n,p,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (B_Cut (n,p,C)) is compact Element of K6( the U1 of (TOP-REAL 2))
L_Cut (n,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
R_Cut ((L_Cut (n,p)),C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (R_Cut ((L_Cut (n,p)),C)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (B_Cut (n,p,C)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
dom n is Element of K6(NAT)
C is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
n ^' C is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
dom (n ^' C) is Element of K6(NAT)
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len (n ^' C) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n is non empty V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
C is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
dom C is Element of K6(NAT)
n ^' C is non empty V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
dom (n ^' C) is non empty Element of K6(NAT)
len C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len (n ^' C) is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
C is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
n ^' C is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
rng n is set
p is V13() V16( NAT ) Function-like constant V26() FinSequence-like FinSubsequence-like set
rng p is V2() set
n is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
C is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
n ^' C is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . (len n) is set
C . 1 is set
p is V13() V16( NAT ) Function-like constant V26() FinSequence-like FinSubsequence-like set
rng p is V2() set
rng n is set
rng C is set
(rng n) \/ (rng C) is set
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special FinSequence of the U1 of (TOP-REAL 2)
C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
p is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
mid (n,C,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
p -' C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
(p -' C) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
C -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
n /^ (C -' 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special FinSequence of the U1 of (TOP-REAL 2)
(n /^ (C -' 1)) | ((p -' C) + 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special FinSequence of the U1 of (TOP-REAL 2)
mid (n,p,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
C -' p is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
(C -' p) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
p -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
n /^ (p -' 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special FinSequence of the U1 of (TOP-REAL 2)
(n /^ (p -' 1)) | ((C -' p) + 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special FinSequence of the U1 of (TOP-REAL 2)
Rev (mid (n,C,p)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (Rev (mid (n,C,p))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like unfolded FinSequence of the U1 of (TOP-REAL 2)
C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
p is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
mid (n,C,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
p -' C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
(p -' C) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
C -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
n /^ (C -' 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like unfolded FinSequence of the U1 of (TOP-REAL 2)
(n /^ (C -' 1)) | ((p -' C) + 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like unfolded FinSequence of the U1 of (TOP-REAL 2)
mid (n,p,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
C -' p is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
(C -' p) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
p -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
n /^ (p -' 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like unfolded FinSequence of the U1 of (TOP-REAL 2)
(n /^ (p -' 1)) | ((C -' p) + 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like unfolded FinSequence of the U1 of (TOP-REAL 2)
Rev (mid (n,C,p)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (Rev (mid (n,C,p))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
mid (n,((Index (C,n)) + 1),(len n)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
<*C*> /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg (n,(Index (C,n))) is Element of K6( the U1 of (TOP-REAL 2))
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg ((n /. (Index (C,n))),(n /. ((Index (C,n)) + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. (Index (C,n)))) + (b1 * (n /. ((Index (C,n)) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
C `1 is V11() V12() ext-real Element of REAL
(n /. ((Index (C,n)) + 1)) `1 is V11() V12() ext-real Element of REAL
C `2 is V11() V12() ext-real Element of REAL
(n /. ((Index (C,n)) + 1)) `2 is V11() V12() ext-real Element of REAL
C `1 is V11() V12() ext-real Element of REAL
(n /. ((Index (C,n)) + 1)) `1 is V11() V12() ext-real Element of REAL
C `2 is V11() V12() ext-real Element of REAL
(n /. ((Index (C,n)) + 1)) `2 is V11() V12() ext-real Element of REAL
C `1 is V11() V12() ext-real Element of REAL
(n /. ((Index (C,n)) + 1)) `1 is V11() V12() ext-real Element of REAL
C `2 is V11() V12() ext-real Element of REAL
(n /. ((Index (C,n)) + 1)) `2 is V11() V12() ext-real Element of REAL
len <*C*> is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
0 + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom n is Element of K6(NAT)
(mid (n,((Index (C,n)) + 1),(len n))) /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n . ((Index (C,n)) + 1) is set
<*C*> ^ (mid (n,((Index (C,n)) + 1),(len n))) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n . ((Index (C,n)) + 1) is set
n . ((Index (C,n)) + 1) is set
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
R_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
mid (n,1,(Index (C,n))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
0 + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom n is Element of K6(NAT)
len (mid (n,1,(Index (C,n)))) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(mid (n,1,(Index (C,n)))) /. (len (mid (n,1,(Index (C,n))))) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
LSeg (n,(Index (C,n))) is Element of K6( the U1 of (TOP-REAL 2))
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg ((n /. (Index (C,n))),(n /. ((Index (C,n)) + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. (Index (C,n)))) + (b1 * (n /. ((Index (C,n)) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
C `1 is V11() V12() ext-real Element of REAL
(n /. (Index (C,n))) `1 is V11() V12() ext-real Element of REAL
C `2 is V11() V12() ext-real Element of REAL
(n /. (Index (C,n))) `2 is V11() V12() ext-real Element of REAL
C `1 is V11() V12() ext-real Element of REAL
(n /. (Index (C,n))) `1 is V11() V12() ext-real Element of REAL
C `2 is V11() V12() ext-real Element of REAL
(n /. (Index (C,n))) `2 is V11() V12() ext-real Element of REAL
C `1 is V11() V12() ext-real Element of REAL
(n /. (Index (C,n))) `1 is V11() V12() ext-real Element of REAL
C `2 is V11() V12() ext-real Element of REAL
(n /. (Index (C,n))) `2 is V11() V12() ext-real Element of REAL
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
<*C*> /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n . 1 is set
(mid (n,1,(Index (C,n)))) ^ <*C*> is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n . 1 is set
n . 1 is set
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
p is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
B_Cut (n,C,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom n is Element of K6(NAT)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
L_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (L_Cut (n,C)) is compact Element of K6( the U1 of (TOP-REAL 2))
R_Cut ((L_Cut (n,C)),p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (L_Cut (n,C)) is compact Element of K6( the U1 of (TOP-REAL 2))
R_Cut ((L_Cut (n,C)),p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut (n,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (L_Cut (n,p)) is compact Element of K6( the U1 of (TOP-REAL 2))
LSeg ((n /. (Index (C,n))),(n /. ((Index (C,n)) + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. (Index (C,n)))) + (b1 * (n /. ((Index (C,n)) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
n . (Index (C,n)) is set
n . ((Index (C,n)) + 1) is set
L_Cut (n,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (L_Cut (n,p)) is compact Element of K6( the U1 of (TOP-REAL 2))
L_Cut (n,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (L_Cut (n,p)) is compact Element of K6( the U1 of (TOP-REAL 2))
L_Cut (n,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (L_Cut (n,p)) is compact Element of K6( the U1 of (TOP-REAL 2))
R_Cut ((L_Cut (n,p)),C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (R_Cut ((L_Cut (n,p)),C)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
mid (n,((Index (C,n)) + 1),(len n)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg ((n /. (Index (C,n))),(n /. ((Index (C,n)) + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. (Index (C,n)))) + (b1 * (n /. ((Index (C,n)) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
((Index (C,n)) + 1) + 0 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
0 + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom n is Element of K6(NAT)
LSeg (n,(Index (C,n))) is Element of K6( the U1 of (TOP-REAL 2))
(mid (n,((Index (C,n)) + 1),(len n))) /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
((Index (C,n)) + 1) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
LSeg (n,((Index (C,n)) + 1)) is Element of K6( the U1 of (TOP-REAL 2))
1 + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
(Index (C,n)) + (1 + 1) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + (1 + 1)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg ((n /. ((Index (C,n)) + 1)),(n /. ((Index (C,n)) + (1 + 1)))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. ((Index (C,n)) + 1))) + (b1 * (n /. ((Index (C,n)) + (1 + 1))))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((n /. (Index (C,n))),(n /. ((Index (C,n)) + 1)))) /\ (LSeg ((n /. ((Index (C,n)) + 1)),(n /. ((Index (C,n)) + (1 + 1))))) is Element of K6( the U1 of (TOP-REAL 2))
{(n /. ((Index (C,n)) + 1))} is non empty V2() V33(1) set
(len n) - ((Index (C,n)) + 1) is V11() V12() ext-real Element of REAL
(len n) - (Index (C,n)) is V11() V12() ext-real Element of REAL
LSeg (C,(n /. ((Index (C,n)) + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * C) + (b1 * (n /. ((Index (C,n)) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg (C,(n /. ((Index (C,n)) + 1)))) /\ (LSeg ((n /. ((Index (C,n)) + 1)),(n /. ((Index (C,n)) + (1 + 1))))) is Element of K6( the U1 of (TOP-REAL 2))
2 + ((Index (C,n)) + 1) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(2 + ((Index (C,n)) + 1)) - 1 is V11() V12() ext-real Element of REAL
len (mid (n,((Index (C,n)) + 1),(len n))) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len n) -' ((Index (C,n)) + 1) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
((len n) -' ((Index (C,n)) + 1)) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
((len n) - ((Index (C,n)) + 1)) + 1 is V11() V12() ext-real Element of REAL
dom (mid (n,((Index (C,n)) + 1),(len n))) is Element of K6(NAT)
(mid (n,((Index (C,n)) + 1),(len n))) /. 2 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(2 + ((Index (C,n)) + 1)) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
n /. ((2 + ((Index (C,n)) + 1)) -' 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg ((mid (n,((Index (C,n)) + 1),(len n))),1) is Element of K6( the U1 of (TOP-REAL 2))
n . ((Index (C,n)) + 1) is set
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
<*C*> ^ (mid (n,((Index (C,n)) + 1),(len n))) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n . ((Index (C,n)) + 1) is set
n . ((Index (C,n)) + 1) is set
((Index (C,n)) + 1) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . ((Index (C,n)) + 1) is set
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
mid (n,(len n),(len n)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*C*> ^ (mid (n,(len n),(len n))) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n /. (len n) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
<*(n /. (len n))*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
<*C*> ^ <*(n /. (len n))*> is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() V33(1 + 1) FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
1 + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
<*C,(n /. (len n))*> is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() V33(2) FinSequence-like FinSubsequence-like () FinSequence of the U1 of (TOP-REAL 2)
len (L_Cut (n,C)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . ((Index (C,n)) + 1) is set
mid (n,(len n),(len n)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n /. (len n) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
<*(n /. (len n))*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
len (L_Cut (n,C)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . ((Index (C,n)) + 1) is set
((Index (C,n)) + 1) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
R_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
0 + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Seg (len n) is V26() V33( len n) Element of K6(NAT)
dom n is Element of K6(NAT)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
((Index (C,n)) + 1) + 0 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
LSeg (n,(Index (C,n))) is Element of K6( the U1 of (TOP-REAL 2))
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg ((n /. (Index (C,n))),(n /. ((Index (C,n)) + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. (Index (C,n)))) + (b1 * (n /. ((Index (C,n)) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
mid (n,1,(Index (C,n))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (mid (n,1,(Index (C,n)))) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(mid (n,1,(Index (C,n)))) /. (len (mid (n,1,(Index (C,n))))) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
((Index (C,n)) -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
LSeg ((n /. (Index (C,n))),C) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. (Index (C,n)))) + (b1 * C)) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
n /. ((Index (C,n)) -' 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg ((n /. ((Index (C,n)) -' 1)),(n /. (Index (C,n)))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. ((Index (C,n)) -' 1))) + (b1 * (n /. (Index (C,n))))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((n /. ((Index (C,n)) -' 1)),(n /. (Index (C,n))))) /\ (LSeg ((n /. (Index (C,n))),C)) is Element of K6( the U1 of (TOP-REAL 2))
{(n /. (Index (C,n)))} is non empty V2() V33(1) set
1 + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
((Index (C,n)) -' 1) + (1 + 1) is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
(Index (C,n)) - 1 is V11() V12() ext-real Element of REAL
LSeg (n,((Index (C,n)) -' 1)) is Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((n /. ((Index (C,n)) -' 1)),(n /. (Index (C,n))))) /\ (LSeg ((n /. (Index (C,n))),(n /. ((Index (C,n)) + 1)))) is Element of K6( the U1 of (TOP-REAL 2))
(len (mid (n,1,(Index (C,n))))) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
((len (mid (n,1,(Index (C,n))))) -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
Seg (len (mid (n,1,(Index (C,n))))) is V26() V33( len (mid (n,1,(Index (C,n))))) Element of K6(NAT)
dom (mid (n,1,(Index (C,n)))) is Element of K6(NAT)
(mid (n,1,(Index (C,n)))) /. ((len (mid (n,1,(Index (C,n))))) -' 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(((len (mid (n,1,(Index (C,n))))) -' 1) + 1) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
n /. ((((len (mid (n,1,(Index (C,n))))) -' 1) + 1) -' 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n /. ((len (mid (n,1,(Index (C,n))))) -' 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(((Index (C,n)) -' 1) + 1) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
n /. ((((Index (C,n)) -' 1) + 1) -' 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg ((mid (n,1,(Index (C,n)))),((len (mid (n,1,(Index (C,n))))) -' 1)) is Element of K6( the U1 of (TOP-REAL 2))
n . 1 is set
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
(mid (n,1,(Index (C,n)))) ^ <*C*> is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n . 1 is set
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
len (R_Cut (n,C)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . 1 is set
n . 1 is set
mid (n,1,1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
(mid (n,1,1)) ^ <*C*> is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
<*(n /. 1)*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
<*(n /. 1)*> ^ <*C*> is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() V33(1 + 1) FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
1 + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
<*(n /. 1),C*> is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() V33(2) FinSequence-like FinSubsequence-like () FinSequence of the U1 of (TOP-REAL 2)
len (R_Cut (n,C)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . 1 is set
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
len (R_Cut (n,C)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . 1 is set
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
p is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
B_Cut (n,C,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Seg (len n) is V26() V33( len n) Element of K6(NAT)
dom n is Element of K6(NAT)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
L_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (L_Cut (n,C)) is compact Element of K6( the U1 of (TOP-REAL 2))
R_Cut ((L_Cut (n,C)),p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (L_Cut (n,C)) is compact Element of K6( the U1 of (TOP-REAL 2))
R_Cut ((L_Cut (n,C)),p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut (n,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (L_Cut (n,p)) is compact Element of K6( the U1 of (TOP-REAL 2))
LSeg ((n /. (Index (C,n))),(n /. ((Index (C,n)) + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. (Index (C,n)))) + (b1 * (n /. ((Index (C,n)) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
n . (Index (C,n)) is set
n . ((Index (C,n)) + 1) is set
L_Cut (n,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (L_Cut (n,p)) is compact Element of K6( the U1 of (TOP-REAL 2))
L_Cut (n,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (L_Cut (n,p)) is compact Element of K6( the U1 of (TOP-REAL 2))
L_Cut (n,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (L_Cut (n,p)) is compact Element of K6( the U1 of (TOP-REAL 2))
R_Cut ((L_Cut (n,p)),C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (R_Cut ((L_Cut (n,p)),C)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
len (B_Cut (n,C,p)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
n . 1 is set
C is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
p is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
mid (n,1,(Index (p,n))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*p*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
(mid (n,1,(Index (p,n)))) ^ <*p*> is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
f is V4() V5() V6() V10() V11() V12() V26() V31() ext-real set
q is V4() V5() V6() V10() V11() V12() V26() V31() ext-real set
q + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
LSeg (C,q) is Element of K6( the U1 of (TOP-REAL 2))
LSeg (C,f) is Element of K6( the U1 of (TOP-REAL 2))
0 + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(LSeg (C,q)) /\ (LSeg (C,f)) is Element of K6( the U1 of (TOP-REAL 2))
f + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
LSeg (n,q) is Element of K6( the U1 of (TOP-REAL 2))
1 + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
LSeg (n,f) is Element of K6( the U1 of (TOP-REAL 2))
(LSeg (n,q)) /\ (LSeg (n,f)) is Element of K6( the U1 of (TOP-REAL 2))
(LSeg (C,q)) /\ (LSeg (C,f)) is Element of K6( the U1 of (TOP-REAL 2))
f + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(LSeg (C,q)) /\ (LSeg (C,f)) is Element of K6( the U1 of (TOP-REAL 2))
f + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
f + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len C is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len (mid (n,1,(Index (p,n)))) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len <*p*> is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len (mid (n,1,(Index (p,n))))) + (len <*p*>) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len (mid (n,1,(Index (p,n))))) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
q is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
q + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
LSeg (n,q) is Element of K6( the U1 of (TOP-REAL 2))
1 + q is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Index (p,n)) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
((Index (p,n)) -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
C . 1 is set
(mid (n,1,(Index (p,n)))) . 1 is set
f is V4() V5() V6() V10() V11() V12() V26() V31() ext-real set
f + 2 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
LSeg (C,f) is Element of K6( the U1 of (TOP-REAL 2))
f + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
LSeg (C,(f + 1)) is Element of K6( the U1 of (TOP-REAL 2))
(LSeg (C,f)) /\ (LSeg (C,(f + 1))) is Element of K6( the U1 of (TOP-REAL 2))
C /. (f + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
{(C /. (f + 1))} is non empty V2() V33(1) set
C /. f is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg ((C /. f),(C /. (f + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (C /. f)) + (b1 * (C /. (f + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(f + 1) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C /. ((f + 1) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg ((C /. (f + 1)),(C /. ((f + 1) + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (C /. (f + 1))) + (b1 * (C /. ((f + 1) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (n,f) is Element of K6( the U1 of (TOP-REAL 2))
LSeg (n,(f + 1)) is Element of K6( the U1 of (TOP-REAL 2))
(LSeg (n,f)) /\ (LSeg (n,(f + 1))) is Element of K6( the U1 of (TOP-REAL 2))
C . (f + 1) is set
(len n) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (f + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
{(n /. (f + 1))} is non empty V2() V33(1) set
n . (f + 1) is set
(mid (n,1,(Index (p,n)))) . (f + 1) is set
f is V4() V5() V6() V10() V11() V12() V26() V31() ext-real set
f + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C /. f is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(C /. f) `1 is V11() V12() ext-real Element of REAL
C /. (f + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(C /. (f + 1)) `1 is V11() V12() ext-real Element of REAL
(C /. f) `2 is V11() V12() ext-real Element of REAL
(C /. (f + 1)) `2 is V11() V12() ext-real Element of REAL
LSeg (C,f) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((C /. f),(C /. (f + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (C /. f)) + (b1 * (C /. (f + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(Index (p,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
LSeg (n,f) is Element of K6( the U1 of (TOP-REAL 2))
n /. f is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n /. (f + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg ((n /. f),(n /. (f + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. f)) + (b1 * (n /. (f + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(n /. f) `1 is V11() V12() ext-real Element of REAL
(n /. (f + 1)) `1 is V11() V12() ext-real Element of REAL
(n /. f) `2 is V11() V12() ext-real Element of REAL
(n /. (f + 1)) `2 is V11() V12() ext-real Element of REAL
dom <*p*> is non empty V2() V33(1) Element of K6(NAT)
dom C is Element of K6(NAT)
f is set
Lf is set
C . f is set
C . Lf is set
a is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
b is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C . (len C) is set
<*p*> . 1 is set
C . b is set
(mid (n,1,(Index (p,n)))) . b is set
b + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(b + 1) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
n . ((b + 1) -' 1) is set
n . b is set
(Index (p,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C . a is set
(mid (n,1,(Index (p,n)))) . a is set
a + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(a + 1) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
n . ((a + 1) -' 1) is set
n . a is set
(Index (p,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C . b is set
(mid (n,1,(Index (p,n)))) . b is set
n . b is set
Seg (len n) is V26() V33( len n) Element of K6(NAT)
dom n is Element of K6(NAT)
C . a is set
(mid (n,1,(Index (p,n)))) . a is set
n . a is set
1 + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
C . (len C) is set
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
len n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . (len n) is set
Rev n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . ((Index (C,n)) + 1) is set
Index (C,(Rev n)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Index (C,(Rev n))) + (Index (C,n)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
((Index (C,(Rev n))) + (Index (C,n))) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len (Rev n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len n) + (Index (C,n)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len n) - (Index (C,n)) is V11() V12() ext-real Element of REAL
(len n) -' (Index (C,n)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
dom n is Element of K6(NAT)
dom (Rev n) is Element of K6(NAT)
Rev (Rev n) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
(Rev (Rev n)) . ((Index (C,n)) + 1) is set
(len (Rev n)) - ((Index (C,n)) + 1) is V11() V12() ext-real Element of REAL
((len (Rev n)) - ((Index (C,n)) + 1)) + 1 is V11() V12() ext-real Element of REAL
(Rev n) . (((len (Rev n)) - ((Index (C,n)) + 1)) + 1) is set
(len (Rev n)) - (Index (C,n)) is V11() V12() ext-real Element of REAL
(Rev n) . ((len (Rev n)) - (Index (C,n))) is set
(Rev n) . ((len n) - (Index (C,n))) is set
(Index (C,(Rev n))) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len n is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut (n,(n /. 1)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index ((n /. 1),n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom n is non empty Element of K6(NAT)
n . 1 is set
1 + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
n . (1 + 1) is set
<*(n /. 1)*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
(Index ((n /. 1),n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
mid (n,((Index ((n /. 1),n)) + 1),(len n)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*(n /. 1)*> ^ (mid (n,((Index ((n /. 1),n)) + 1),(len n))) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
mid (n,1,(len n)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
len n is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . (len n) is set
Rev n is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut ((Rev n),C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
R_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (R_Cut (n,C)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
L~ (Rev n) is compact Element of K6( the U1 of (TOP-REAL 2))
dom (Rev n) is non empty Element of K6(NAT)
dom n is non empty Element of K6(NAT)
len (Rev n) is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,(Rev n)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Index (C,(Rev n))) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . 1 is set
(len (Rev n)) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
((len (Rev n)) -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
(Rev n) /^ ((len (Rev n)) -' 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
((Rev n) /^ ((len (Rev n)) -' 1)) . 1 is set
(Rev n) . (len (Rev n)) is set
len ((Rev n) /^ ((len (Rev n)) -' 1)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len (Rev n)) -' ((len (Rev n)) -' 1) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
(len (Rev n)) - ((len (Rev n)) -' 1) is V11() V12() ext-real Element of REAL
(len (Rev n)) -' (len (Rev n)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
((len (Rev n)) -' (len (Rev n))) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
(len (Rev n)) - (len (Rev n)) is V11() V12() ext-real Element of REAL
((len (Rev n)) - (len (Rev n))) + 1 is V11() V12() ext-real Element of REAL
mid ((Rev n),(len (Rev n)),(len (Rev n))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
((Rev n) /^ ((len (Rev n)) -' 1)) | 1 is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
((Rev n) /^ ((len (Rev n)) -' 1)) /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
<*(((Rev n) /^ ((len (Rev n)) -' 1)) /. 1)*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
<*((Rev n) . (len (Rev n)))*> is non empty V2() V13() V16( NAT ) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like () () () set
(Rev n) . (len n) is set
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
Rev <*C*> is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like () () () FinSequence of the U1 of (TOP-REAL 2)
n . 1 is set
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . ((Index (C,n)) + 1) is set
(Index (C,(Rev n))) + (Index (C,n)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
((Index (C,(Rev n))) + (Index (C,n))) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Index (C,n)) + ((Index (C,(Rev n))) + 1) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Index (C,(Rev n))) + ((Index (C,n)) + 1) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len n) - ((Index (C,(Rev n))) + 1) is V11() V12() ext-real Element of REAL
((len n) - ((Index (C,(Rev n))) + 1)) + 1 is V11() V12() ext-real Element of REAL
n . (((len n) - ((Index (C,(Rev n))) + 1)) + 1) is set
(Rev n) . ((Index (C,(Rev n))) + 1) is set
(len n) -' (Index (C,n)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
(len n) - (Index (C,n)) is V11() V12() ext-real Element of REAL
(Rev n) . (len n) is set
mid ((Rev n),((Index (C,(Rev n))) + 1),(len n)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
((len n) -' (Index (C,n))) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
mid ((Rev n),(((len n) -' (Index (C,n))) + 1),(len n)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*C*> ^ (mid ((Rev n),(((len n) -' (Index (C,n))) + 1),(len n))) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
(len n) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
((len n) -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
mid ((Rev n),(((len n) -' (Index (C,n))) + 1),(((len n) -' 1) + 1)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*C*> ^ (mid ((Rev n),(((len n) -' (Index (C,n))) + 1),(((len n) -' 1) + 1))) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
mid (n,1,(Index (C,n))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (mid (n,1,(Index (C,n)))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*C*> ^ (Rev (mid (n,1,(Index (C,n))))) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
(mid (n,1,(Index (C,n)))) ^ <*C*> is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev ((mid (n,1,(Index (C,n)))) ^ <*C*>) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n . 1 is set
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . ((Index (C,n)) + 1) is set
(Rev n) . (len n) is set
(Rev n) . ((Index (C,(Rev n))) + 1) is set
Rev (Rev n) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (C,(Rev (Rev n))) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Index (C,(Rev (Rev n)))) + (Index (C,(Rev n))) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
((Index (C,(Rev (Rev n)))) + (Index (C,(Rev n)))) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
((Index (C,n)) + 1) + (Index (C,(Rev n))) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len n) - ((Index (C,(Rev n))) + 1) is V11() V12() ext-real Element of REAL
((len n) - ((Index (C,(Rev n))) + 1)) + 1 is V11() V12() ext-real Element of REAL
n . (((len n) - ((Index (C,(Rev n))) + 1)) + 1) is set
(Index (C,(Rev n))) + (Index (C,n)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len n) - (Index (C,n)) is V11() V12() ext-real Element of REAL
(len n) -' (Index (C,n)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
((len n) -' (Index (C,n))) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
mid ((Rev n),(((len n) -' (Index (C,n))) + 1),(len n)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*C*> ^ (mid ((Rev n),(((len n) -' (Index (C,n))) + 1),(len n))) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
(len n) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
((len n) -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
mid ((Rev n),(((len n) -' (Index (C,n))) + 1),(((len n) -' 1) + 1)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*C*> ^ (mid ((Rev n),(((len n) -' (Index (C,n))) + 1),(((len n) -' 1) + 1))) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
mid (n,1,(Index (C,n))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (mid (n,1,(Index (C,n)))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*C*> ^ (Rev (mid (n,1,(Index (C,n))))) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
(mid (n,1,(Index (C,n)))) ^ <*C*> is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev ((mid (n,1,(Index (C,n)))) ^ <*C*>) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n . 1 is set
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . ((Index (C,n)) + 1) is set
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
n . 1 is set
n /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
R_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
mid (n,1,(Index (C,n))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*C*> is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one constant V26() V33(1) FinSequence-like FinSubsequence-like special () () () FinSequence of the U1 of (TOP-REAL 2)
(mid (n,1,(Index (C,n)))) ^ <*C*> is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
len n is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . (len n) is set
n . 1 is set
n /. (len n) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev n is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (Rev n) is compact Element of K6( the U1 of (TOP-REAL 2))
(Rev n) . (len n) is set
len (Rev n) is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Rev n) . (len (Rev n)) is set
(Rev n) . 1 is set
Rev (Rev n) is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L_Cut ((Rev (Rev n)),C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
R_Cut ((Rev n),C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (R_Cut ((Rev n),C)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
(Rev n) /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
n . 1 is set
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
R_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
len n is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n . (len n) is set
n . 1 is set
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n /. (len n) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
n . 1 is set
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
p is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
B_Cut (n,C,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len n is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
L_Cut (n,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
R_Cut ((L_Cut (n,C)),p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n . (len n) is set
LSeg ((n /. (Index (C,n))),(n /. ((Index (C,n)) + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. (Index (C,n)))) + (b1 * (n /. ((Index (C,n)) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
q is V11() V12() ext-real Element of REAL
1 - q is V11() V12() ext-real Element of REAL
(1 - q) * (n /. (Index (C,n))) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
q * (n /. ((Index (C,n)) + 1)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
((1 - q) * (n /. (Index (C,n)))) + (q * (n /. ((Index (C,n)) + 1))) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
1 * C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
0. (TOP-REAL 2) is V33(2) FinSequence-like V48() V76( TOP-REAL 2) Element of the U1 of (TOP-REAL 2)
(0. (TOP-REAL 2)) + (1 * C) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
1 - 1 is V11() V12() ext-real Element of REAL
(1 - 1) * (n /. (Index (C,n))) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
((1 - 1) * (n /. (Index (C,n)))) + (1 * C) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n . ((Index (C,n)) + 1) is set
n . (len n) is set
n . (len n) is set
n . (len n) is set
n /. (len n) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(L_Cut (n,C)) . 1 is set
L~ (L_Cut (n,C)) is compact Element of K6( the U1 of (TOP-REAL 2))
len (L_Cut (n,C)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
L~ (L_Cut (n,C)) is compact Element of K6( the U1 of (TOP-REAL 2))
len (L_Cut (n,C)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len (L_Cut (n,C)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len (L_Cut (n,C)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
L~ (L_Cut (n,C)) is compact Element of K6( the U1 of (TOP-REAL 2))
q is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
q + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
LSeg ((L_Cut (n,C)),q) is Element of K6( the U1 of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
f + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
LSeg ((L_Cut (n,C)),f) is Element of K6( the U1 of (TOP-REAL 2))
Index (p,(L_Cut (n,C))) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(L_Cut (n,C)) /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len n is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
n . 1 is set
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
p is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
B_Cut (n,C,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
dom n is non empty Element of K6(NAT)
n . (Index (C,n)) is set
n . ((Index (C,n)) + 1) is set
LSeg (n,(Index (C,n))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((n /. (Index (C,n))),(n /. ((Index (C,n)) + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (n /. (Index (C,n)))) + (b1 * (n /. ((Index (C,n)) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
n /. (Index (p,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (p,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (p,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L_Cut (n,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
R_Cut ((L_Cut (n,p)),C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (R_Cut ((L_Cut (n,p)),C)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
B_Cut (n,p,C) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (B_Cut (n,p,C)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Index (p,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
Index (C,n) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. (Index (C,n)) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Index (C,n)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
n /. ((Index (C,n)) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
n is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len n is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
L~ n is compact Element of K6( the U1 of (TOP-REAL 2))
n . 1 is set
C is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
p is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
B_Cut (n,C,p) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
C is non empty compact non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))
Cage (C,n) is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard V192() () () () FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (C,n)) is non empty compact Element of K6( the U1 of (TOP-REAL 2))
BDD (L~ (Cage (C,n))) is Element of K6( the U1 of (TOP-REAL 2))
p is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
South-Bound (p,(L~ (Cage (C,n)))) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))) is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard V192() () () () FinSequence of the U1 of (TOP-REAL 2)
len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
(Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like special unfolded FinSequence of the U1 of (TOP-REAL 2)
North-Bound (p,(L~ (Cage (C,n)))) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
B_Cut (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() V33(2) FinSequence-like FinSubsequence-like () FinSequence of the U1 of (TOP-REAL 2)
L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> is compact Element of K6( the U1 of (TOP-REAL 2))
L~ (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) is non empty compact Element of K6( the U1 of (TOP-REAL 2))
LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1))) /\ (LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1)) is Element of K6( the U1 of (TOP-REAL 2))
(Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
{((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)} is non empty V2() V33(1) set
(Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2)) + (b1 * ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
1 + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
(Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)) + (b1 * ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(South-Bound (p,(L~ (Cage (C,n))))) `1 is V11() V12() ext-real Element of REAL
p `1 is V11() V12() ext-real Element of REAL
len (Cage (C,n)) is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len (Cage (C,n))) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
((len (Cage (C,n))) -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
(Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1))) + (b1 * ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
rf is V4() V5() V6() V10() V11() V12() V26() V31() ext-real set
(Cage (C,n)) /. rf is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
dom (Cage (C,n)) is non empty V2() Element of K6(NAT)
((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n)) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
0 + (((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n))) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len (Cage (C,n))) - (((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n))) is V11() V12() ext-real Element of REAL
1 - 1 is V11() V12() ext-real Element of REAL
rng (Cage (C,n)) is non empty V2() set
(Cage (C,n)) :- ((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len ((Cage (C,n)) :- ((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
((len (Cage (C,n))) - (((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n)))) + 1 is V11() V12() ext-real Element of REAL
1 -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
(1 -' 1) + (((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n))) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
LSeg ((Cage (C,n)),((1 -' 1) + (((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n))))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((Cage (C,n)),(0 + (((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n))))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((Cage (C,n)),(Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) is Element of K6( the U1 of (TOP-REAL 2))
(len (Cage (C,n))) - 1 is V11() V12() ext-real Element of REAL
(North-Bound (p,(L~ (Cage (C,n))))) `1 is V11() V12() ext-real Element of REAL
LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (North-Bound (p,(L~ (Cage (C,n)))))) + (b1 * (South-Bound (p,(L~ (Cage (C,n))))))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(North-Bound (p,(L~ (Cage (C,n))))) `2 is V11() V12() ext-real Element of REAL
p `2 is V11() V12() ext-real Element of REAL
(South-Bound (p,(L~ (Cage (C,n))))) `2 is V11() V12() ext-real Element of REAL
rf is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one V26() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq () () () FinSequence of the U1 of (TOP-REAL 2)
L~ rf is non empty compact Element of K6( the U1 of (TOP-REAL 2))
(L~ rf) \/ (LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1))) is Element of K6( the U1 of (TOP-REAL 2))
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1 is V11() V12() ext-real Element of REAL
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `1 is V11() V12() ext-real Element of REAL
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `1 is V11() V12() ext-real Element of REAL
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `1 is V11() V12() ext-real Element of REAL
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 is V11() V12() ext-real Element of REAL
((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2) is V11() V12() ext-real Element of REAL
(((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2 is V11() V12() ext-real Element of REAL
|[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| is non empty V13() V16( NAT ) Function-like V26() V33(2) FinSequence-like FinSubsequence-like V48() () Element of the U1 of (TOP-REAL 2)
|[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `1 is V11() V12() ext-real Element of REAL
|[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `2 is V11() V12() ext-real Element of REAL
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 is V11() V12() ext-real Element of REAL
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `2 is V11() V12() ext-real Element of REAL
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 is V11() V12() ext-real Element of REAL
LSeg ((South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (South-Bound (p,(L~ (Cage (C,n)))))) + (b1 * (North-Bound (p,(L~ (Cage (C,n))))))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) is Element of K6( the U1 of (TOP-REAL 2))
{(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} is set
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 is V11() V12() ext-real Element of REAL
((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2) is V11() V12() ext-real Element of REAL
(((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2 is V11() V12() ext-real Element of REAL
|[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| is non empty V13() V16( NAT ) Function-like V26() V33(2) FinSequence-like FinSubsequence-like V48() () Element of the U1 of (TOP-REAL 2)
|[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `1 is V11() V12() ext-real Element of REAL
|[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `2 is V11() V12() ext-real Element of REAL
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 is V11() V12() ext-real Element of REAL
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `2 is V11() V12() ext-real Element of REAL
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 is V11() V12() ext-real Element of REAL
LSeg ((South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (South-Bound (p,(L~ (Cage (C,n)))))) + (b1 * (North-Bound (p,(L~ (Cage (C,n))))))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) is Element of K6( the U1 of (TOP-REAL 2))
{(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} is set
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 is V11() V12() ext-real Element of REAL
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `2 is V11() V12() ext-real Element of REAL
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `1 is V11() V12() ext-real Element of REAL
LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2)) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)) + (b1 * ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) is Element of K6( the U1 of (TOP-REAL 2))
{(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} is set
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 is V11() V12() ext-real Element of REAL
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1 is V11() V12() ext-real Element of REAL
(LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) is Element of K6( the U1 of (TOP-REAL 2))
{(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} is set
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 is V11() V12() ext-real Element of REAL
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 is V11() V12() ext-real Element of REAL
len rf is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
LSeg (rf,1) is Element of K6( the U1 of (TOP-REAL 2))
B_Cut (rf,(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
BCut is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one V26() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq () () () FinSequence of the U1 of (TOP-REAL 2)
len BCut is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len BCut) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) is V13() non empty-yielding V16( NAT ) V17(K304( the U1 of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K304( the U1 of (TOP-REAL 2))
BCut1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom BCut is non empty V2() Element of K6(NAT)
dom (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) is non empty Element of K6(NAT)
Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) is set
(BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) /. BCut1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
BCut1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
pion1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
[BCut1,pion1] is non empty set
{BCut1,pion1} is set
{BCut1} is non empty V2() V33(1) set
{{BCut1,pion1},{BCut1}} is set
(GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (BCut1,pion1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
pion1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
g is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
[pion1,g] is non empty set
{pion1,g} is set
{pion1} is non empty V2() V33(1) set
{{pion1,g},{pion1}} is set
BCut /. BCut1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (pion1,g) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
L~ BCut is non empty compact Element of K6( the U1 of (TOP-REAL 2))
BCut /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
BCut /. (len BCut) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
BCut1 is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ BCut1 is compact Element of K6( the U1 of (TOP-REAL 2))
BCut1 /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
len BCut1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
BCut1 /. (len BCut1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
BCut1 is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one V26() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq () () () FinSequence of the U1 of (TOP-REAL 2)
L~ BCut1 is non empty compact Element of K6( the U1 of (TOP-REAL 2))
len BCut1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom BCut1 is non empty V2() Element of K6(NAT)
BCut1 /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
BCut1 /. (len BCut1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(len BCut1) -' 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real non negative Element of NAT
BCut1 /. ((len BCut1) -' 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg ((BCut1 /. ((len BCut1) -' 1)),(BCut1 /. (len BCut1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (BCut1 /. ((len BCut1) -' 1))) + (b1 * (BCut1 /. (len BCut1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(len BCut1) - 1 is V11() V12() ext-real Element of REAL
(LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) is Element of K6( the U1 of (TOP-REAL 2))
{(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} is set
0 + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) /. (len BCut) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
<*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
len <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
len (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
(len BCut) + (1 + 1) is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
((len BCut) + 1) + 1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
pion1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
dom <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> is non empty V33(2) Element of K6(NAT)
Seg (len (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) is non empty V26() V33( len (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) Element of K6(NAT)
pion1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
g is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
[pion1,g] is non empty set
{pion1,g} is set
{pion1} is non empty V2() V33(1) set
{{pion1,g},{pion1}} is set
(GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (pion1,g) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
g is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
c21 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
[g,c21] is non empty set
{g,c21} is set
{g} is non empty V2() V33(1) set
{{g,c21},{g}} is set
<*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. pion1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (g,c21) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) /. ((len BCut) + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
pion1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
g is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
[pion1,g] is non empty set
{pion1,g} is set
{pion1} is non empty V2() V33(1) set
{{pion1,g},{pion1}} is set
(GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (pion1,g) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
g is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
c21 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
[g,c21] is non empty set
{g,c21} is set
{g} is non empty V2() V33(1) set
{{g,c21},{g}} is set
<*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. pion1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (g,c21) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
<*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. (len <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
pion1 is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ pion1 is compact Element of K6( the U1 of (TOP-REAL 2))
pion1 /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
len pion1 is V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
pion1 /. (len pion1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
pion1 is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one V26() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq () () () FinSequence of the U1 of (TOP-REAL 2)
len pion1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real Element of NAT
pion1 /. (len pion1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
(L~ BCut1) /\ (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) is Element of K6( the U1 of (TOP-REAL 2))
L~ pion1 is non empty compact Element of K6( the U1 of (TOP-REAL 2))
(L~ BCut1) /\ (L~ pion1) is Element of K6( the U1 of (TOP-REAL 2))
{(North-Bound (p,(L~ (Cage (C,n))))),(BCut1 /. 1)} is set
pion1 /. 1 is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
{(BCut1 /. 1),(pion1 /. 1)} is set
((len BCut1) -' 1) + 1 is non empty V4() V5() V6() V10() V11() V12() V26() V31() ext-real positive non negative Element of NAT
BCut1 ^' pion1 is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
LSeg (BCut1,((len BCut1) -' 1)) is Element of K6( the U1 of (TOP-REAL 2))
LSeg (pion1,1) is Element of K6( the U1 of (TOP-REAL 2))
(LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) is Element of K6( the U1 of (TOP-REAL 2))
{(BCut1 /. (len BCut1))} is non empty V2() V33(1) set
g is set
g is set
pion1 /. (1 + 1) is V33(2) FinSequence-like V48() Element of the U1 of (TOP-REAL 2)
LSeg ((pion1 /. 1),(pion1 /. (1 + 1))) is compact Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (pion1 /. 1)) + (b1 * (pion1 /. (1 + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
g is set
g is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)