:: JORDAN1B semantic presentation

REAL is V142() V143() V144() V148() set
NAT is V142() V143() V144() V145() V146() V147() V148() Element of bool REAL
bool REAL is set
COMPLEX is V142() V148() set
NAT is V142() V143() V144() V145() V146() V147() V148() set
bool NAT is set
bool NAT is set
RAT is V142() V143() V144() V145() V148() set
INT is V142() V143() V144() V145() V146() V148() set
[:REAL,REAL:] is V18() set
bool [:REAL,REAL:] is set
K360() is non empty V91() L9()
the U1 of K360() is non empty set
K365() is non empty V91() V113() V114() V115() V117() V164() V165() V166() V167() V168() V169() L9()
K366() is non empty V91() V115() V117() V167() V168() V169() M14(K365())
K367() is non empty V91() V113() V115() V117() V167() V168() V169() V170() M17(K365(),K366())
K369() is non empty V91() V113() V115() V117() L9()
K370() is non empty V91() V113() V115() V117() V170() M14(K369())
1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
[:1,1:] is V18() set
bool [:1,1:] is set
[:[:1,1:],1:] is V18() set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is V18() set
bool [:[:1,1:],REAL:] is set
[:[:REAL,REAL:],REAL:] is V18() set
bool [:[:REAL,REAL:],REAL:] is set
2 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
[:2,2:] is V18() set
[:[:2,2:],REAL:] is V18() set
bool [:[:2,2:],REAL:] is set
TOP-REAL 2 is non empty TopSpace-like V89() V154() V155() V172() V173() V174() V175() V176() V177() V178() strict add-continuous Mult-continuous RLTopStruct
the U1 of (TOP-REAL 2) is non empty set
K331( the U1 of (TOP-REAL 2)) is non empty functional FinSequence-membered M11( the U1 of (TOP-REAL 2))
[: the U1 of (TOP-REAL 2),REAL:] is V18() set
bool [: the U1 of (TOP-REAL 2),REAL:] is set
bool the U1 of (TOP-REAL 2) is set
{} is empty V18() non-empty empty-yielding V21( NAT ) Function-like one-to-one constant functional V31() FinSequence-like FinSubsequence-like FinSequence-membered V142() V143() V144() V145() V146() V147() V148() set
3 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
0 is empty V6() V10() V11() V12() ext-real non positive non negative integer V18() non-empty empty-yielding V21( NAT ) Function-like one-to-one constant functional V31() FinSequence-like FinSubsequence-like FinSequence-membered V76() V142() V143() V144() V145() V146() V147() V148() Element of NAT
4 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
proj2 is V18() Function-like V43( the U1 of (TOP-REAL 2), REAL ) Element of bool [: the U1 of (TOP-REAL 2),REAL:]
C is V18() V21( NAT ) Function-like V31() FinSequence-like FinSubsequence-like set
Rev C is V18() V21( NAT ) Function-like V31() FinSequence-like FinSubsequence-like set
n is empty V18() non-empty empty-yielding V21( NAT ) Function-like one-to-one constant functional V31() FinSequence-like FinSubsequence-like FinSequence-membered V142() V143() V144() V145() V146() V147() V148() set
Rev n is empty V18() non-empty empty-yielding V21( NAT ) Function-like one-to-one constant functional V31() FinSequence-like FinSubsequence-like FinSequence-membered V142() V143() V144() V145() V146() V147() V148() set
C is non empty set
n is V18() V21( NAT ) V22(C) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of C
len n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
j is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
mid (n,i,j) is V18() V21( NAT ) V22(C) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of C
dom n is V142() V143() V144() V145() V146() V147() Element of bool NAT
C is V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
L~ C is Element of bool the U1 of (TOP-REAL 2)
C . 1 is set
n is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
R_Cut (C,n) is V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
(R_Cut (C,n)) . 1 is set
Index (n,C) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
dom C is V142() V143() V144() V145() V146() V147() Element of bool NAT
mid (C,1,(Index (n,C))) is V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
<*n*> is non empty trivial V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like constant V31() V38(1) FinSequence-like FinSubsequence-like special FinSequence of the U1 of (TOP-REAL 2)
(mid (C,1,(Index (n,C)))) ^ <*n*> is non empty V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (mid (C,1,(Index (n,C)))) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(mid (C,1,(Index (n,C)))) . 1 is set
<*n*> is non empty trivial V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like constant V31() V38(1) FinSequence-like FinSubsequence-like special FinSequence of the U1 of (TOP-REAL 2)
C is V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ C is Element of bool the U1 of (TOP-REAL 2)
len C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C . (len C) is set
n is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
L_Cut (C,n) is V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (L_Cut (C,n)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(L_Cut (C,n)) . (len (L_Cut (C,n))) is set
Rev C is V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (Rev C) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
L~ (Rev C) is Element of bool the U1 of (TOP-REAL 2)
Rev (Rev C) is V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L_Cut ((Rev (Rev C)),n) is V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
R_Cut ((Rev C),n) is V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (R_Cut ((Rev C),n)) is V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (R_Cut ((Rev C),n)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Rev (R_Cut ((Rev C),n))) . (len (R_Cut ((Rev C),n))) is set
(R_Cut ((Rev C),n)) . 1 is set
(Rev C) . 1 is set
C is non empty connected bounded being_simple_closed_curve compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
W-max C is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
E-max C is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
E-bound C is V11() V12() ext-real Element of REAL
E-most C is Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (E-most C) is strict SubSpace of TOP-REAL 2
proj2 | (E-most C) is V18() Function-like V43( the U1 of ((TOP-REAL 2) | (E-most C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (E-most C)),REAL:]
the U1 of ((TOP-REAL 2) | (E-most C)) is set
[: the U1 of ((TOP-REAL 2) | (E-most C)),REAL:] is V18() set
bool [: the U1 of ((TOP-REAL 2) | (E-most C)),REAL:] is set
upper_bound (proj2 | (E-most C)) is V11() V12() ext-real Element of REAL
|[(E-bound C),(upper_bound (proj2 | (E-most C)))]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
W-bound C is V11() V12() ext-real Element of REAL
W-most C is Element of bool the U1 of (TOP-REAL 2)
(TOP-REAL 2) | (W-most C) is strict SubSpace of TOP-REAL 2
proj2 | (W-most C) is V18() Function-like V43( the U1 of ((TOP-REAL 2) | (W-most C)), REAL ) Element of bool [: the U1 of ((TOP-REAL 2) | (W-most C)),REAL:]
the U1 of ((TOP-REAL 2) | (W-most C)) is set
[: the U1 of ((TOP-REAL 2) | (W-most C)),REAL:] is V18() set
bool [: the U1 of ((TOP-REAL 2) | (W-most C)),REAL:] is set
upper_bound (proj2 | (W-most C)) is V11() V12() ext-real Element of REAL
|[(W-bound C),(upper_bound (proj2 | (W-most C)))]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is non empty set
i is V18() V21( NAT ) V22(n) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of n
len i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len i) -' 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
mid (i,C,((len i) -' 1)) is V18() V21( NAT ) V22(n) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of n
i /. (len i) is Element of n
<*(i /. (len i))*> is non empty trivial V18() V21( NAT ) V22(n) Function-like constant V31() V38(1) FinSequence-like FinSubsequence-like FinSequence of n
(mid (i,C,((len i) -' 1))) ^ <*(i /. (len i))*> is non empty V18() V21( NAT ) V22(n) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of n
mid (i,C,(len i)) is V18() V21( NAT ) V22(n) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of n
C + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(C + 1) - 1 is V11() V12() ext-real integer Element of REAL
(len i) - 1 is V11() V12() ext-real integer Element of REAL
0 + C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((len i) - 1) - C is V11() V12() ext-real integer Element of REAL
((len i) -' 1) - C is V11() V12() ext-real integer set
(len i) - C is V11() V12() ext-real integer Element of REAL
(len i) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((len i) + 1) - 1 is V11() V12() ext-real integer Element of REAL
len (mid (i,C,((len i) -' 1))) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len (mid (i,C,((len i) -' 1)))) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((len i) -' 1) -' C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(((len i) -' 1) -' C) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((((len i) -' 1) -' C) + 1) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(((len i) -' 1) - C) + 1 is V11() V12() ext-real integer Element of REAL
((((len i) -' 1) - C) + 1) + 1 is V11() V12() ext-real integer Element of REAL
(((len i) - 1) - C) + 1 is V11() V12() ext-real integer Element of REAL
((((len i) - 1) - C) + 1) + 1 is V11() V12() ext-real integer Element of REAL
(len i) -' C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((len i) -' C) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
len (mid (i,C,(len i))) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Seg (len i) is V31() V38( len i) V142() V143() V144() V145() V146() V147() Element of bool NAT
dom i is V142() V143() V144() V145() V146() V147() Element of bool NAT
j is V6() V10() V11() V12() ext-real non negative integer set
Seg (len (mid (i,C,((len i) -' 1)))) is V31() V38( len (mid (i,C,((len i) -' 1)))) V142() V143() V144() V145() V146() V147() Element of bool NAT
dom (mid (i,C,((len i) -' 1))) is V142() V143() V144() V145() V146() V147() Element of bool NAT
Seg (len (mid (i,C,(len i)))) is V31() V38( len (mid (i,C,(len i)))) V142() V143() V144() V145() V146() V147() Element of bool NAT
dom (mid (i,C,(len i))) is V142() V143() V144() V145() V146() V147() Element of bool NAT
((mid (i,C,((len i) -' 1))) ^ <*(i /. (len i))*>) /. j is Element of n
(mid (i,C,((len i) -' 1))) /. j is Element of n
j + C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(j + C) -' 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i /. ((j + C) -' 1) is Element of n
(mid (i,C,(len i))) /. j is Element of n
((mid (i,C,((len i) -' 1))) ^ <*(i /. (len i))*>) /. j is Element of n
(mid (i,C,(len i))) /. j is Element of n
len ((mid (i,C,((len i) -' 1))) ^ <*(i /. (len i))*>) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
n is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
LSeg (C,n) is non empty connected bounded bounded compact compact V250( TOP-REAL 2) Element of bool the U1 of (TOP-REAL 2)
<*C,n*> is non empty non trivial V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() V38(2) FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
C `1 is V11() V12() ext-real Element of REAL
n `1 is V11() V12() ext-real Element of REAL
C is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
n is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
LSeg (C,n) is non empty connected bounded bounded compact compact V250( TOP-REAL 2) Element of bool the U1 of (TOP-REAL 2)
<*C,n*> is non empty non trivial V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() V38(2) FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
C `2 is V11() V12() ext-real Element of REAL
n `2 is V11() V12() ext-real Element of REAL
n is V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
C is V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
i is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
Rotate (C,i) is V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
rng C is set
j is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
dom (Rotate (C,i)) is V142() V143() V144() V145() V146() V147() Element of bool NAT
dom C is V142() V143() V144() V145() V146() V147() Element of bool NAT
len C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Seg (len C) is V31() V38( len C) V142() V143() V144() V145() V146() V147() Element of bool NAT
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
j - 1 is V11() V12() ext-real integer Element of REAL
C :- i is non empty V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (C :- i) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i .. C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len C) - (i .. C) is V11() V12() ext-real integer Element of REAL
((len C) - (i .. C)) + 1 is V11() V12() ext-real integer Element of REAL
(j - 1) + (i .. C) is V11() V12() ext-real integer Element of REAL
j -' 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(j -' 1) + (i .. C) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Rotate (C,i)) /. j is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
C /. ((j -' 1) + (i .. C)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
L~ n is Element of bool the U1 of (TOP-REAL 2)
W-bound (L~ n) is V11() V12() ext-real Element of REAL
((Rotate (C,i)) /. j) `1 is V11() V12() ext-real Element of REAL
E-bound (L~ n) is V11() V12() ext-real Element of REAL
S-bound (L~ n) is V11() V12() ext-real Element of REAL
((Rotate (C,i)) /. j) `2 is V11() V12() ext-real Element of REAL
N-bound (L~ n) is V11() V12() ext-real Element of REAL
C :- i is non empty V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (C :- i) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i .. C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len C) - (i .. C) is V11() V12() ext-real integer Element of REAL
((len C) - (i .. C)) + 1 is V11() V12() ext-real integer Element of REAL
1 + (len C) is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(1 + (len C)) - (i .. C) is V11() V12() ext-real integer Element of REAL
j + (i .. C) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(j + (i .. C)) - (len C) is V11() V12() ext-real integer Element of REAL
(j + (i .. C)) -' (len C) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len C) + (len C) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Rotate (C,i)) /. j is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
C /. ((j + (i .. C)) -' (len C)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
L~ n is Element of bool the U1 of (TOP-REAL 2)
W-bound (L~ n) is V11() V12() ext-real Element of REAL
((Rotate (C,i)) /. j) `1 is V11() V12() ext-real Element of REAL
E-bound (L~ n) is V11() V12() ext-real Element of REAL
S-bound (L~ n) is V11() V12() ext-real Element of REAL
((Rotate (C,i)) /. j) `2 is V11() V12() ext-real Element of REAL
N-bound (L~ n) is V11() V12() ext-real Element of REAL
C :- i is non empty V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (C :- i) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
L~ n is Element of bool the U1 of (TOP-REAL 2)
W-bound (L~ n) is V11() V12() ext-real Element of REAL
E-bound (L~ n) is V11() V12() ext-real Element of REAL
S-bound (L~ n) is V11() V12() ext-real Element of REAL
N-bound (L~ n) is V11() V12() ext-real Element of REAL
L~ n is Element of bool the U1 of (TOP-REAL 2)
W-bound (L~ n) is V11() V12() ext-real Element of REAL
E-bound (L~ n) is V11() V12() ext-real Element of REAL
S-bound (L~ n) is V11() V12() ext-real Element of REAL
N-bound (L~ n) is V11() V12() ext-real Element of REAL
rng C is set
rng C is set
C is non trivial V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
n is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
Rotate (C,n) is V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
C is V18() V21( NAT ) Function-like V31() FinSequence-like FinSubsequence-like set
Center C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
len C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len C) div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((len C) div 2) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C is V18() V21( NAT ) Function-like V31() FinSequence-like FinSubsequence-like set
len C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Center C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len C) + (len C) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
0 + (len C) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len C) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
2 * (len C) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((len C) + 1) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(((len C) + 1) + 1) div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len C) + (1 + 1) is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((len C) + (1 + 1)) div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len C) div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((len C) div 2) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
Center C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
len C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len C) div 2 is V11() V12() ext-real integer set
(len C) div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((len C) div 2) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C is V18() V21( NAT ) Function-like V31() FinSequence-like FinSubsequence-like set
len C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Center C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len C) div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((len C) div 2) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C is V18() V21( NAT ) Function-like V31() FinSequence-like FinSubsequence-like set
len C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Center C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
2 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len C) + (2 + 1) is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len C) + (len C) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len C) + 2 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((len C) + 2) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
2 * (len C) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(((len C) + 2) + 1) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((((len C) + 2) + 1) + 1) div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((len C) + 2) + (1 + 1) is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(((len C) + 2) + (1 + 1)) div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((len C) + 2) div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(((len C) + 2) div 2) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len C) div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((len C) div 2) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C is non empty Element of bool the U1 of (TOP-REAL 2)
Gauge (C,0) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
len (Gauge (C,0)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len (Gauge (C,0))) -' 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
2 |^ 0 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(2 |^ 0) + 3 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((2 |^ 0) + 3) -' 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
1 + 3 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(1 + 3) -' 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C is non empty bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Gauge (C,n) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
Center (Gauge (C,n)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n -' 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
2 |^ (n -' 1) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(2 |^ (n -' 1)) + 2 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
2 * 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(2 * 2) + 0 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
0 - 1 is non empty V11() V12() ext-real non positive negative integer Element of REAL
len (Gauge (C,n)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len (Gauge (C,n))) div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((len (Gauge (C,n))) div 2) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((2 |^ 0) + 3) div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(((2 |^ 0) + 3) div 2) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(1 + 3) div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((1 + 3) div 2) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(1 + 1) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(2 |^ 0) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((2 |^ 0) + 1) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
0 -' 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
2 |^ (0 -' 1) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(2 |^ (0 -' 1)) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((2 |^ (0 -' 1)) + 1) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
2 |^ n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(2 |^ n) div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(2 |^ n) / 2 is V11() V12() ext-real non negative Element of COMPLEX
2 |^ 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(2 |^ n) / (2 |^ 1) is V11() V12() ext-real non negative Element of COMPLEX
2 * 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(2 * 1) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
3 div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(2 |^ n) mod 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
len (Gauge (C,n)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len (Gauge (C,n))) div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((len (Gauge (C,n))) div 2) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(2 |^ n) + 3 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((2 |^ n) + 3) div 2 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(((2 |^ n) + 3) div 2) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((2 |^ n) div 2) + (3 div 2) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(((2 |^ n) div 2) + (3 div 2)) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((2 |^ n) div 2) + (1 + 1) is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C is non empty bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Gauge (C,0) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
cell ((Gauge (C,0)),2,2) is Element of bool the U1 of (TOP-REAL 2)
i is set
len (Gauge (C,0)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
width (Gauge (C,0)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (C,0)) * (1,2) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (C,0)) * (1,2)) `2 is V11() V12() ext-real Element of REAL
S-bound C is V11() V12() ext-real Element of REAL
j is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
j `2 is V11() V12() ext-real Element of REAL
(Gauge (C,0)) * (2,1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (C,0)) * (2,1)) `1 is V11() V12() ext-real Element of REAL
2 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (C,0)) * ((2 + 1),1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (C,0)) * ((2 + 1),1)) `1 is V11() V12() ext-real Element of REAL
(Gauge (C,0)) * (1,(2 + 1)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (C,0)) * (1,(2 + 1))) `2 is V11() V12() ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() V12() ext-real Element of REAL : ( ((Gauge (C,0)) * (2,1)) `1 <= b₁ & b₁ <= ((Gauge (C,0)) * ((2 + 1),1)) `1 & ((Gauge (C,0)) * (1,2)) `2 <= b₂ & b₂ <= ((Gauge (C,0)) * (1,(2 + 1))) `2 ) } is set
W-bound C is V11() V12() ext-real Element of REAL
j `1 is V11() V12() ext-real Element of REAL
(len (Gauge (C,0))) -' 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
E-bound C is V11() V12() ext-real Element of REAL
N-bound C is V11() V12() ext-real Element of REAL
|[(j `1),(j `2)]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
C is non empty bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Gauge (C,0) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
cell ((Gauge (C,0)),2,2) is Element of bool the U1 of (TOP-REAL 2)
BDD C is Element of bool the U1 of (TOP-REAL 2)
the Element of C is Element of C
C is non empty connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Gauge (C,1) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
Center (Gauge (C,1)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (C,1)) * ((Center (Gauge (C,1))),1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
W-bound C is V11() V12() ext-real Element of REAL
E-bound C is V11() V12() ext-real Element of REAL
(W-bound C) + (E-bound C) is V11() V12() ext-real Element of REAL
((W-bound C) + (E-bound C)) / 2 is V11() V12() ext-real Element of COMPLEX
Cage (C,1) is non empty non trivial V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like non constant V31() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (C,1)) is non empty connected bounded being_simple_closed_curve compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
S-bound (L~ (Cage (C,1))) is V11() V12() ext-real Element of REAL
|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
len (Gauge (C,1)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 is V11() V12() ext-real Element of REAL
((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 is V11() V12() ext-real Element of REAL
C is non empty connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Gauge (C,1) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
Center (Gauge (C,1)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
len (Gauge (C,1)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1)))) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
W-bound C is V11() V12() ext-real Element of REAL
E-bound C is V11() V12() ext-real Element of REAL
(W-bound C) + (E-bound C) is V11() V12() ext-real Element of REAL
((W-bound C) + (E-bound C)) / 2 is V11() V12() ext-real Element of COMPLEX
Cage (C,1) is non empty non trivial V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like non constant V31() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (C,1)) is non empty connected bounded being_simple_closed_curve compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (C,1))) is V11() V12() ext-real Element of REAL
|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))) `1 is V11() V12() ext-real Element of REAL
((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))) `2 is V11() V12() ext-real Element of REAL
C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n -' 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
width C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
len C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell (C,(len C),n) is Element of bool the U1 of (TOP-REAL 2)
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
j is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C * (i,j) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (i,j)) `1 is V11() V12() ext-real Element of REAL
n is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
n `1 is V11() V12() ext-real Element of REAL
C * (i,1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (i,1)) `1 is V11() V12() ext-real Element of REAL
C * ((len C),1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * ((len C),1)) `1 is V11() V12() ext-real Element of REAL
C * (1,n) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,n)) `2 is V11() V12() ext-real Element of REAL
n + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C * (1,(n + 1)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,(n + 1))) `2 is V11() V12() ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V11() V12() ext-real Element of REAL : ( (C * ((len C),1)) `1 <= b<sub>1</sub> & (C * (1,n)) `2 <= b₂ & b₂ <= (C * (1,(n + 1))) `2 ) } is set
p is V11() V12() ext-real Element of REAL
r is V11() V12() ext-real Element of REAL
|[p,r]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
C is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
len C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
width C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell (C,n,i) is Element of bool the U1 of (TOP-REAL 2)
j is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
j -' 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C * (j,n) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (j,n)) `1 is V11() V12() ext-real Element of REAL
p is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
p `1 is V11() V12() ext-real Element of REAL
C * (j,1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (j,1)) `1 is V11() V12() ext-real Element of REAL
C * (n,1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (n,1)) `1 is V11() V12() ext-real Element of REAL
n + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C * ((n + 1),1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * ((n + 1),1)) `1 is V11() V12() ext-real Element of REAL
C * (1,i) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,i)) `2 is V11() V12() ext-real Element of REAL
i + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C * (1,(i + 1)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,(i + 1))) `2 is V11() V12() ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V11() V12() ext-real Element of REAL : ( (C * (n,1)) `1 <= b<sub>1</sub> & b<sub>1</sub> <= (C * ((n + 1),1)) `1 & (C * (1,i)) `2 <= b<sub>2</sub> & b<sub>2</sub> <= (C * (1,(i + 1))) `2 ) } is set
r is V11() V12() ext-real Element of REAL
s is V11() V12() ext-real Element of REAL
|[r,s]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
C is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
len C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
width C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell (C,n,(width C)) is Element of bool the U1 of (TOP-REAL 2)
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
j is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C * (i,j) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (i,j)) `2 is V11() V12() ext-real Element of REAL
n is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
n `2 is V11() V12() ext-real Element of REAL
C * (1,j) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,j)) `2 is V11() V12() ext-real Element of REAL
C * (n,1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (n,1)) `1 is V11() V12() ext-real Element of REAL
n + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C * ((n + 1),1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * ((n + 1),1)) `1 is V11() V12() ext-real Element of REAL
C * (1,(width C)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,(width C))) `2 is V11() V12() ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V11() V12() ext-real Element of REAL : ( (C * (n,1)) `1 <= b<sub>1</sub> & b<sub>1</sub> <= (C * ((n + 1),1)) `1 & (C * (1,(width C))) `2 <= b<sub>2</sub> ) } is set
p is V11() V12() ext-real Element of REAL
r is V11() V12() ext-real Element of REAL
|[p,r]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
C is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
len C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
width C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell (C,n,i) is Element of bool the U1 of (TOP-REAL 2)
j is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C * (j,n) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (j,n)) `2 is V11() V12() ext-real Element of REAL
n -' 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
p is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
p `2 is V11() V12() ext-real Element of REAL
C * (1,n) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,n)) `2 is V11() V12() ext-real Element of REAL
C * (n,1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (n,1)) `1 is V11() V12() ext-real Element of REAL
n + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C * ((n + 1),1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * ((n + 1),1)) `1 is V11() V12() ext-real Element of REAL
C * (1,i) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,i)) `2 is V11() V12() ext-real Element of REAL
i + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C * (1,(i + 1)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,(i + 1))) `2 is V11() V12() ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V11() V12() ext-real Element of REAL : ( (C * (n,1)) `1 <= b<sub>1</sub> & b<sub>1</sub> <= (C * ((n + 1),1)) `1 & (C * (1,i)) `2 <= b<sub>2</sub> & b<sub>2</sub> <= (C * (1,(i + 1))) `2 ) } is set
r is V11() V12() ext-real Element of REAL
s is V11() V12() ext-real Element of REAL
|[r,s]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is non empty connected bounded being_simple_closed_curve compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Gauge (n,C) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
len (Gauge (n,C)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Upper_Arc n is non empty Element of bool the U1 of (TOP-REAL 2)
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * (i,1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(Gauge (n,C)) * (i,(len (Gauge (n,C)))) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (n,C)) * (i,1)),((Gauge (n,C)) * (i,(len (Gauge (n,C)))))) is non empty connected bounded bounded compact compact V250( TOP-REAL 2) Element of bool the U1 of (TOP-REAL 2)
(Gauge (n,C)) * (i,2) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (n,C)) * (i,2)) `1 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len (Gauge (n,C))) - 1 is V11() V12() ext-real integer Element of REAL
(len (Gauge (n,C))) -' 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
width (Gauge (n,C)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * (i,((len (Gauge (n,C))) -' 1)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (n,C)) * (i,1)) `1 is V11() V12() ext-real Element of REAL
((Gauge (n,C)) * (i,((len (Gauge (n,C))) -' 1))) `1 is V11() V12() ext-real Element of REAL
(Gauge (n,C)) * (2,2) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (n,C)) * (2,2)) `1 is V11() V12() ext-real Element of REAL
W-bound n is V11() V12() ext-real Element of REAL
i + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * (((len (Gauge (n,C))) -' 1),((len (Gauge (n,C))) -' 1)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (n,C)) * (((len (Gauge (n,C))) -' 1),((len (Gauge (n,C))) -' 1))) `1 is V11() V12() ext-real Element of REAL
E-bound n is V11() V12() ext-real Element of REAL
((Gauge (n,C)) * (i,((len (Gauge (n,C))) -' 1))) `2 is V11() V12() ext-real Element of REAL
|[(((Gauge (n,C)) * (i,((len (Gauge (n,C))) -' 1))) `1),(((Gauge (n,C)) * (i,((len (Gauge (n,C))) -' 1))) `2)]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
N-bound n is V11() V12() ext-real Element of REAL
|[(((Gauge (n,C)) * (i,((len (Gauge (n,C))) -' 1))) `1),(N-bound n)]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (n,C)) * (i,2)) `2 is V11() V12() ext-real Element of REAL
|[(((Gauge (n,C)) * (i,2)) `1),(((Gauge (n,C)) * (i,2)) `2)]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
S-bound n is V11() V12() ext-real Element of REAL
|[(((Gauge (n,C)) * (i,2)) `1),(S-bound n)]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (n,C)) * (i,2)),((Gauge (n,C)) * (i,((len (Gauge (n,C))) -' 1)))) is non empty connected bounded bounded compact compact V250( TOP-REAL 2) Element of bool the U1 of (TOP-REAL 2)
C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is non empty connected bounded being_simple_closed_curve compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Gauge (n,C) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
len (Gauge (n,C)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Lower_Arc n is non empty Element of bool the U1 of (TOP-REAL 2)
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * (i,1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(Gauge (n,C)) * (i,(len (Gauge (n,C)))) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (n,C)) * (i,1)),((Gauge (n,C)) * (i,(len (Gauge (n,C)))))) is non empty connected bounded bounded compact compact V250( TOP-REAL 2) Element of bool the U1 of (TOP-REAL 2)
(Gauge (n,C)) * (i,2) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (n,C)) * (i,2)) `1 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(len (Gauge (n,C))) - 1 is V11() V12() ext-real integer Element of REAL
(len (Gauge (n,C))) -' 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
width (Gauge (n,C)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * (i,((len (Gauge (n,C))) -' 1)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (n,C)) * (i,1)) `1 is V11() V12() ext-real Element of REAL
((Gauge (n,C)) * (i,((len (Gauge (n,C))) -' 1))) `1 is V11() V12() ext-real Element of REAL
(Gauge (n,C)) * (2,2) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (n,C)) * (2,2)) `1 is V11() V12() ext-real Element of REAL
W-bound n is V11() V12() ext-real Element of REAL
i + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * (((len (Gauge (n,C))) -' 1),((len (Gauge (n,C))) -' 1)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (n,C)) * (((len (Gauge (n,C))) -' 1),((len (Gauge (n,C))) -' 1))) `1 is V11() V12() ext-real Element of REAL
E-bound n is V11() V12() ext-real Element of REAL
((Gauge (n,C)) * (i,((len (Gauge (n,C))) -' 1))) `2 is V11() V12() ext-real Element of REAL
|[(((Gauge (n,C)) * (i,((len (Gauge (n,C))) -' 1))) `1),(((Gauge (n,C)) * (i,((len (Gauge (n,C))) -' 1))) `2)]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
N-bound n is V11() V12() ext-real Element of REAL
|[(((Gauge (n,C)) * (i,((len (Gauge (n,C))) -' 1))) `1),(N-bound n)]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (n,C)) * (i,2)) `2 is V11() V12() ext-real Element of REAL
|[(((Gauge (n,C)) * (i,2)) `1),(((Gauge (n,C)) * (i,2)) `2)]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
S-bound n is V11() V12() ext-real Element of REAL
|[(((Gauge (n,C)) * (i,2)) `1),(S-bound n)]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (n,C)) * (i,2)),((Gauge (n,C)) * (i,((len (Gauge (n,C))) -' 1)))) is non empty connected bounded bounded compact compact V250( TOP-REAL 2) Element of bool the U1 of (TOP-REAL 2)
C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is non empty connected bounded being_simple_closed_curve compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Gauge (n,C) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
Center (Gauge (n,C)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * ((Center (Gauge (n,C))),1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
len (Gauge (n,C)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * ((Center (Gauge (n,C))),(len (Gauge (n,C)))) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (n,C)) * ((Center (Gauge (n,C))),1)),((Gauge (n,C)) * ((Center (Gauge (n,C))),(len (Gauge (n,C)))))) is non empty connected bounded bounded compact compact V250( TOP-REAL 2) Element of bool the U1 of (TOP-REAL 2)
Upper_Arc n is non empty Element of bool the U1 of (TOP-REAL 2)
C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is non empty connected bounded being_simple_closed_curve compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Gauge (n,C) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
Center (Gauge (n,C)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * ((Center (Gauge (n,C))),1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
len (Gauge (n,C)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * ((Center (Gauge (n,C))),(len (Gauge (n,C)))) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (n,C)) * ((Center (Gauge (n,C))),1)),((Gauge (n,C)) * ((Center (Gauge (n,C))),(len (Gauge (n,C)))))) is non empty connected bounded bounded compact compact V250( TOP-REAL 2) Element of bool the U1 of (TOP-REAL 2)
Lower_Arc n is non empty Element of bool the U1 of (TOP-REAL 2)
C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is non empty connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Gauge (n,C) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
len (Gauge (n,C)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Cage (n,C) is non empty non trivial V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like non constant V31() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (n,C)) is non empty connected bounded being_simple_closed_curve compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Upper_Arc (L~ (Cage (n,C))) is non empty Element of bool the U1 of (TOP-REAL 2)
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * (i,1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(Gauge (n,C)) * (i,(len (Gauge (n,C)))) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (n,C)) * (i,1)),((Gauge (n,C)) * (i,(len (Gauge (n,C)))))) is non empty connected bounded bounded compact compact V250( TOP-REAL 2) Element of bool the U1 of (TOP-REAL 2)
((Gauge (n,C)) * (i,1)) `1 is V11() V12() ext-real Element of REAL
((Gauge (n,C)) * (i,1)) `2 is V11() V12() ext-real Element of REAL
|[(((Gauge (n,C)) * (i,1)) `1),(((Gauge (n,C)) * (i,1)) `2)]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
S-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL
|[(((Gauge (n,C)) * (i,1)) `1),(S-bound (L~ (Cage (n,C))))]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (n,C)) * (i,(len (Gauge (n,C))))) `1 is V11() V12() ext-real Element of REAL
((Gauge (n,C)) * (i,(len (Gauge (n,C))))) `2 is V11() V12() ext-real Element of REAL
|[(((Gauge (n,C)) * (i,(len (Gauge (n,C))))) `1),(((Gauge (n,C)) * (i,(len (Gauge (n,C))))) `2)]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL
|[(((Gauge (n,C)) * (i,(len (Gauge (n,C))))) `1),(N-bound (L~ (Cage (n,C))))]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
width (Gauge (n,C)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * (1,1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (n,C)) * (1,1)) `1 is V11() V12() ext-real Element of REAL
W-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL
(Gauge (n,C)) * ((len (Gauge (n,C))),1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (n,C)) * ((len (Gauge (n,C))),1)) `1 is V11() V12() ext-real Element of REAL
E-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL
C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is non empty connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Gauge (n,C) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
len (Gauge (n,C)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Cage (n,C) is non empty non trivial V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like non constant V31() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (n,C)) is non empty connected bounded being_simple_closed_curve compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Lower_Arc (L~ (Cage (n,C))) is non empty Element of bool the U1 of (TOP-REAL 2)
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * (i,1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(Gauge (n,C)) * (i,(len (Gauge (n,C)))) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (n,C)) * (i,1)),((Gauge (n,C)) * (i,(len (Gauge (n,C)))))) is non empty connected bounded bounded compact compact V250( TOP-REAL 2) Element of bool the U1 of (TOP-REAL 2)
((Gauge (n,C)) * (i,1)) `1 is V11() V12() ext-real Element of REAL
((Gauge (n,C)) * (i,1)) `2 is V11() V12() ext-real Element of REAL
|[(((Gauge (n,C)) * (i,1)) `1),(((Gauge (n,C)) * (i,1)) `2)]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
S-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL
|[(((Gauge (n,C)) * (i,1)) `1),(S-bound (L~ (Cage (n,C))))]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (n,C)) * (i,(len (Gauge (n,C))))) `1 is V11() V12() ext-real Element of REAL
((Gauge (n,C)) * (i,(len (Gauge (n,C))))) `2 is V11() V12() ext-real Element of REAL
|[(((Gauge (n,C)) * (i,(len (Gauge (n,C))))) `1),(((Gauge (n,C)) * (i,(len (Gauge (n,C))))) `2)]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
N-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL
|[(((Gauge (n,C)) * (i,(len (Gauge (n,C))))) `1),(N-bound (L~ (Cage (n,C))))]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
width (Gauge (n,C)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * (1,1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (n,C)) * (1,1)) `1 is V11() V12() ext-real Element of REAL
W-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL
(Gauge (n,C)) * ((len (Gauge (n,C))),1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
((Gauge (n,C)) * ((len (Gauge (n,C))),1)) `1 is V11() V12() ext-real Element of REAL
E-bound (L~ (Cage (n,C))) is V11() V12() ext-real Element of REAL
C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is non empty connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Gauge (n,C) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
Center (Gauge (n,C)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * ((Center (Gauge (n,C))),1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
len (Gauge (n,C)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * ((Center (Gauge (n,C))),(len (Gauge (n,C)))) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (n,C)) * ((Center (Gauge (n,C))),1)),((Gauge (n,C)) * ((Center (Gauge (n,C))),(len (Gauge (n,C)))))) is non empty connected bounded bounded compact compact V250( TOP-REAL 2) Element of bool the U1 of (TOP-REAL 2)
Cage (n,C) is non empty non trivial V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like non constant V31() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (n,C)) is non empty connected bounded being_simple_closed_curve compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Upper_Arc (L~ (Cage (n,C))) is non empty Element of bool the U1 of (TOP-REAL 2)
C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is non empty connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Gauge (n,C) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
Center (Gauge (n,C)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * ((Center (Gauge (n,C))),1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
len (Gauge (n,C)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (n,C)) * ((Center (Gauge (n,C))),(len (Gauge (n,C)))) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (n,C)) * ((Center (Gauge (n,C))),1)),((Gauge (n,C)) * ((Center (Gauge (n,C))),(len (Gauge (n,C)))))) is non empty connected bounded bounded compact compact V250( TOP-REAL 2) Element of bool the U1 of (TOP-REAL 2)
Cage (n,C) is non empty non trivial V18() V21( NAT ) V22( the U1 of (TOP-REAL 2)) Function-like non constant V31() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Cage (n,C)) is non empty connected bounded being_simple_closed_curve compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
Lower_Arc (L~ (Cage (n,C))) is non empty Element of bool the U1 of (TOP-REAL 2)
C is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
width C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell (C,0,n) is Element of bool the U1 of (TOP-REAL 2)
C * (1,1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,1)) `1 is V11() V12() ext-real Element of REAL
(C * (1,1)) `2 is V11() V12() ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V11() V12() ext-real Element of REAL : ( b₁ <= (C * (1,1)) `1 & b<sub>2</sub> <= (C * (1,1)) `2 ) } is set
i is V11() V12() ext-real Element of REAL
- i is V11() V12() ext-real Element of REAL
min ((- i),((C * (1,1)) `1)) is V11() V12() ext-real Element of REAL
min ((- i),((C * (1,1)) `2)) is V11() V12() ext-real Element of REAL
|[(min ((- i),((C * (1,1)) `1))),(min ((- i),((C * (1,1)) `2)))]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
j is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
|.j.| is V11() V12() ext-real non negative Element of REAL
j `1 is V11() V12() ext-real Element of REAL
abs (j `1) is V11() V12() ext-real Element of REAL
abs (- i) is V11() V12() ext-real Element of REAL
- (- i) is V11() V12() ext-real Element of REAL
C * (1,1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,1)) `1 is V11() V12() ext-real Element of REAL
C * (1,n) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,n)) `2 is V11() V12() ext-real Element of REAL
n + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C * (1,(n + 1)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,(n + 1))) `2 is V11() V12() ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() V12() ext-real Element of REAL : ( b<sub>1</sub> <= (C * (1,1)) `1 & (C * (1,n)) `2 <= b<sub>2</sub> & b<sub>2</sub> <= (C * (1,(n + 1))) `2 ) } is set
len C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i is V11() V12() ext-real Element of REAL
- i is V11() V12() ext-real Element of REAL
min ((- i),((C * (1,1)) `1)) is V11() V12() ext-real Element of REAL
|[(min ((- i),((C * (1,1)) `1))),((C * (1,n)) `2)]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
j is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
|.j.| is V11() V12() ext-real non negative Element of REAL
j `1 is V11() V12() ext-real Element of REAL
abs (j `1) is V11() V12() ext-real Element of REAL
abs (- i) is V11() V12() ext-real Element of REAL
- (- i) is V11() V12() ext-real Element of REAL
C * (1,1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,1)) `1 is V11() V12() ext-real Element of REAL
C * (1,(width C)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,(width C))) `2 is V11() V12() ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V11() V12() ext-real Element of REAL : ( b₁ <= (C * (1,1)) `1 & (C * (1,(width C))) `2 <= b₂ ) } is set
i is V11() V12() ext-real Element of REAL
max (i,((C * (1,(width C))) `2)) is V11() V12() ext-real Element of REAL
|[((C * (1,1)) `1),(max (i,((C * (1,(width C))) `2)))]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
j is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
|.j.| is V11() V12() ext-real non negative Element of REAL
j `2 is V11() V12() ext-real Element of REAL
abs (j `2) is V11() V12() ext-real Element of REAL
C is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
width C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
len C is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell (C,(len C),n) is Element of bool the U1 of (TOP-REAL 2)
cell (C,(len C),0) is Element of bool the U1 of (TOP-REAL 2)
C * ((len C),1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * ((len C),1)) `1 is V11() V12() ext-real Element of REAL
C * (1,1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,1)) `2 is V11() V12() ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() V12() ext-real Element of REAL : ( (C * ((len C),1)) `1 <= b₁ & b₂ <= (C * (1,1)) `2 ) } is set
i is V11() V12() ext-real Element of REAL
- i is V11() V12() ext-real Element of REAL
min ((- i),((C * (1,1)) `2)) is V11() V12() ext-real Element of REAL
|[((C * ((len C),1)) `1),(min ((- i),((C * (1,1)) `2)))]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
j is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
|.j.| is V11() V12() ext-real non negative Element of REAL
j `2 is V11() V12() ext-real Element of REAL
abs (j `2) is V11() V12() ext-real Element of REAL
abs (- i) is V11() V12() ext-real Element of REAL
- (- i) is V11() V12() ext-real Element of REAL
C * ((len C),1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * ((len C),1)) `1 is V11() V12() ext-real Element of REAL
C * (1,n) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,n)) `2 is V11() V12() ext-real Element of REAL
n + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C * (1,(n + 1)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,(n + 1))) `2 is V11() V12() ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() V12() ext-real Element of REAL : ( (C * ((len C),1)) `1 <= b₁ & (C * (1,n)) `2 <= b<sub>2</sub> & b<sub>2</sub> <= (C * (1,(n + 1))) `2 ) } is set
i is V11() V12() ext-real Element of REAL
max (i,((C * ((len C),1)) `1)) is V11() V12() ext-real Element of REAL
|[(max (i,((C * ((len C),1)) `1))),((C * (1,n)) `2)]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
j is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
|.j.| is V11() V12() ext-real non negative Element of REAL
j `1 is V11() V12() ext-real Element of REAL
abs (j `1) is V11() V12() ext-real Element of REAL
cell (C,(len C),(width C)) is Element of bool the U1 of (TOP-REAL 2)
C * ((len C),1) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * ((len C),1)) `1 is V11() V12() ext-real Element of REAL
C * (1,(width C)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
(C * (1,(width C))) `2 is V11() V12() ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() V12() ext-real Element of REAL : ( (C * ((len C),1)) `1 <= b₁ & (C * (1,(width C))) `2 <= b<sub>2</sub> ) } is set
i is V11() V12() ext-real Element of REAL
max (i,((C * (1,(width C))) `2)) is V11() V12() ext-real Element of REAL
|[((C * ((len C),1)) `1),(max (i,((C * (1,(width C))) `2)))]| is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
j is non empty non trivial V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
|.j.| is V11() V12() ext-real non negative Element of REAL
j `2 is V11() V12() ext-real Element of REAL
abs (j `2) is V11() V12() ext-real Element of REAL
C is non empty connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
UBD C is non empty connected Element of bool the U1 of (TOP-REAL 2)
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Gauge (C,i) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
width (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell ((Gauge (C,i)),0,n) is Element of bool the U1 of (TOP-REAL 2)
C ` is Element of bool the U1 of (TOP-REAL 2)
len (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
j is Element of bool the U1 of (TOP-REAL 2)
C is non empty bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
UBD C is non empty connected Element of bool the U1 of (TOP-REAL 2)
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Gauge (C,i) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
len (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell ((Gauge (C,i)),(len (Gauge (C,i))),n) is Element of bool the U1 of (TOP-REAL 2)
C ` is Element of bool the U1 of (TOP-REAL 2)
width (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
j is Element of bool the U1 of (TOP-REAL 2)
C is non empty connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
BDD C is Element of bool the U1 of (TOP-REAL 2)
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Gauge (C,i) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
width (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
j is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell ((Gauge (C,i)),j,n) is Element of bool the U1 of (TOP-REAL 2)
cell ((Gauge (C,i)),0,n) is Element of bool the U1 of (TOP-REAL 2)
UBD C is non empty connected Element of bool the U1 of (TOP-REAL 2)
len (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C is non empty connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
BDD C is Element of bool the U1 of (TOP-REAL 2)
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Gauge (C,i) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
len (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
j is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell ((Gauge (C,i)),n,j) is Element of bool the U1 of (TOP-REAL 2)
cell ((Gauge (C,i)),n,0) is Element of bool the U1 of (TOP-REAL 2)
UBD C is non empty connected Element of bool the U1 of (TOP-REAL 2)
width (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
C is non empty connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
BDD C is Element of bool the U1 of (TOP-REAL 2)
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Gauge (C,i) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
width (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
len (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
j is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell ((Gauge (C,i)),j,n) is Element of bool the U1 of (TOP-REAL 2)
cell ((Gauge (C,i)),(len (Gauge (C,i))),n) is Element of bool the U1 of (TOP-REAL 2)
UBD C is non empty connected Element of bool the U1 of (TOP-REAL 2)
C is non empty connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
BDD C is Element of bool the U1 of (TOP-REAL 2)
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Gauge (C,i) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
len (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
width (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
j is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell ((Gauge (C,i)),n,j) is Element of bool the U1 of (TOP-REAL 2)
cell ((Gauge (C,i)),n,(width (Gauge (C,i)))) is Element of bool the U1 of (TOP-REAL 2)
UBD C is non empty connected Element of bool the U1 of (TOP-REAL 2)
C is non empty connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
BDD C is Element of bool the U1 of (TOP-REAL 2)
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Gauge (C,i) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
len (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
width (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
j is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell ((Gauge (C,i)),n,j) is Element of bool the U1 of (TOP-REAL 2)
C ` is Element of bool the U1 of (TOP-REAL 2)
cell ((Gauge (C,i)),n,1) is Element of bool the U1 of (TOP-REAL 2)
UBD C is non empty connected Element of bool the U1 of (TOP-REAL 2)
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell ((Gauge (C,i)),n,0) is Element of bool the U1 of (TOP-REAL 2)
cell ((Gauge (C,i)),n,(0 + 1)) is Element of bool the U1 of (TOP-REAL 2)
(cell ((Gauge (C,i)),n,0)) /\ (cell ((Gauge (C,i)),n,(0 + 1))) is Element of bool the U1 of (TOP-REAL 2)
(Gauge (C,i)) * (n,(0 + 1)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
n + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (C,i)) * ((n + 1),(0 + 1)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (C,i)) * (n,(0 + 1))),((Gauge (C,i)) * ((n + 1),(0 + 1)))) is non empty connected bounded bounded compact compact V250( TOP-REAL 2) Element of bool the U1 of (TOP-REAL 2)
C is non empty connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
BDD C is Element of bool the U1 of (TOP-REAL 2)
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Gauge (C,i) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
len (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
width (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
j is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell ((Gauge (C,i)),n,j) is Element of bool the U1 of (TOP-REAL 2)
C ` is Element of bool the U1 of (TOP-REAL 2)
cell ((Gauge (C,i)),1,j) is Element of bool the U1 of (TOP-REAL 2)
UBD C is non empty connected Element of bool the U1 of (TOP-REAL 2)
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell ((Gauge (C,i)),0,j) is Element of bool the U1 of (TOP-REAL 2)
cell ((Gauge (C,i)),(0 + 1),j) is Element of bool the U1 of (TOP-REAL 2)
(cell ((Gauge (C,i)),0,j)) /\ (cell ((Gauge (C,i)),(0 + 1),j)) is Element of bool the U1 of (TOP-REAL 2)
(Gauge (C,i)) * ((0 + 1),j) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
j + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (C,i)) * ((0 + 1),(j + 1)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (C,i)) * ((0 + 1),j)),((Gauge (C,i)) * ((0 + 1),(j + 1)))) is non empty connected bounded bounded compact compact V250( TOP-REAL 2) Element of bool the U1 of (TOP-REAL 2)
C is non empty connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
BDD C is Element of bool the U1 of (TOP-REAL 2)
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Gauge (C,i) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
len (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
width (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
j is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell ((Gauge (C,i)),n,j) is Element of bool the U1 of (TOP-REAL 2)
j + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(width (Gauge (C,i))) -' 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell ((Gauge (C,i)),n,((width (Gauge (C,i))) -' 1)) is Element of bool the U1 of (TOP-REAL 2)
C ` is Element of bool the U1 of (TOP-REAL 2)
((width (Gauge (C,i))) -' 1) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell ((Gauge (C,i)),n,(width (Gauge (C,i)))) is Element of bool the U1 of (TOP-REAL 2)
UBD C is non empty connected Element of bool the U1 of (TOP-REAL 2)
(width (Gauge (C,i))) - 1 is V11() V12() ext-real integer Element of REAL
(cell ((Gauge (C,i)),n,(width (Gauge (C,i))))) /\ (cell ((Gauge (C,i)),n,((width (Gauge (C,i))) -' 1))) is Element of bool the U1 of (TOP-REAL 2)
(Gauge (C,i)) * (n,(width (Gauge (C,i)))) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
n + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (C,i)) * ((n + 1),(width (Gauge (C,i)))) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (C,i)) * (n,(width (Gauge (C,i))))),((Gauge (C,i)) * ((n + 1),(width (Gauge (C,i)))))) is non empty connected bounded bounded compact compact V250( TOP-REAL 2) Element of bool the U1 of (TOP-REAL 2)
C is non empty connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
BDD C is Element of bool the U1 of (TOP-REAL 2)
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
n + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Gauge (C,i) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
len (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
width (Gauge (C,i)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
j is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell ((Gauge (C,i)),n,j) is Element of bool the U1 of (TOP-REAL 2)
(len (Gauge (C,i))) -' 1 is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell ((Gauge (C,i)),((len (Gauge (C,i))) -' 1),j) is Element of bool the U1 of (TOP-REAL 2)
C ` is Element of bool the U1 of (TOP-REAL 2)
((len (Gauge (C,i))) -' 1) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
UBD C is non empty connected Element of bool the U1 of (TOP-REAL 2)
cell ((Gauge (C,i)),(len (Gauge (C,i))),j) is Element of bool the U1 of (TOP-REAL 2)
(len (Gauge (C,i))) - 1 is V11() V12() ext-real integer Element of REAL
(cell ((Gauge (C,i)),(len (Gauge (C,i))),j)) /\ (cell ((Gauge (C,i)),((len (Gauge (C,i))) -' 1),j)) is Element of bool the U1 of (TOP-REAL 2)
(Gauge (C,i)) * ((len (Gauge (C,i))),j) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
j + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(Gauge (C,i)) * ((len (Gauge (C,i))),(j + 1)) is V18() V21( NAT ) Function-like V31() V38(2) FinSequence-like FinSubsequence-like V134() Element of the U1 of (TOP-REAL 2)
LSeg (((Gauge (C,i)) * ((len (Gauge (C,i))),j)),((Gauge (C,i)) * ((len (Gauge (C,i))),(j + 1)))) is non empty connected bounded bounded compact compact V250( TOP-REAL 2) Element of bool the U1 of (TOP-REAL 2)
C is non empty connected bounded compact non horizontal non vertical Element of bool the U1 of (TOP-REAL 2)
BDD C is Element of bool the U1 of (TOP-REAL 2)
n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Gauge (C,n) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
len (Gauge (C,n)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
width (Gauge (C,n)) is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
j is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
cell ((Gauge (C,n)),i,j) is Element of bool the U1 of (TOP-REAL 2)
j + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
i + 1 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
2 |^ n is V6() V10() V11() V12() ext-real non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
(2 |^ n) + 3 is non empty V6() V10() V11() V12() ext-real positive non negative integer V76() V142() V143() V144() V145() V146() V147() Element of NAT
Gauge (C,0) is V18() non empty-yielding V21( NAT ) V22(K331( the U1 of (TOP-REAL 2))) Function-like V31() FinSequence-like FinSubsequence-like V180() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K331( the U1 of (TOP-REAL 2))
cell ((Gauge (C,0)),2,2) is Element of bool the U1 of (TOP-REAL 2)