:: REVROT_1 semantic presentation

REAL is non empty non trivial V30() V163() V164() V165() V169() set
NAT is non empty non trivial V25() V30() cardinal limit_cardinal V163() V164() V165() V166() V167() V168() V169() Element of bool REAL
bool REAL is non empty non trivial V30() set
NAT is non empty non trivial V25() V30() cardinal limit_cardinal V163() V164() V165() V166() V167() V168() V169() set
bool NAT is non empty non trivial V30() set
bool NAT is non empty non trivial V30() set
COMPLEX is non empty non trivial V30() V163() V169() set
2 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
[:2,2:] is V1() V30() set
[:[:2,2:],2:] is V1() V30() set
bool [:[:2,2:],2:] is V30() V34() set
RAT is non empty non trivial V30() V163() V164() V165() V166() V169() set
INT is non empty non trivial V30() V163() V164() V165() V166() V167() V169() set
1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
[:1,1:] is V1() V30() set
bool [:1,1:] is V30() V34() set
[:[:1,1:],1:] is V1() V30() set
bool [:[:1,1:],1:] is V30() V34() set
[:[:1,1:],REAL:] is V1() set
bool [:[:1,1:],REAL:] is set
[:REAL,REAL:] is V1() non empty non trivial V30() set
[:[:REAL,REAL:],REAL:] is V1() non empty non trivial V30() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial V30() set
[:[:2,2:],REAL:] is V1() set
bool [:[:2,2:],REAL:] is set
bool [:REAL,REAL:] is non empty non trivial V30() set
TOP-REAL 2 is non empty TopSpace-like V96() V121() V122() V123() V124() V125() V126() V127() strict RLTopStruct
the U1 of (TOP-REAL 2) is non empty set
the U1 of (TOP-REAL 2) * is functional non empty FinSequence-membered FinSequenceSet of the U1 of (TOP-REAL 2)
[: the U1 of (TOP-REAL 2),REAL:] is V1() non empty non trivial V30() set
bool [: the U1 of (TOP-REAL 2),REAL:] is non empty non trivial V30() set
bool the U1 of (TOP-REAL 2) is set
[:COMPLEX,COMPLEX:] is V1() non empty non trivial V30() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial V30() set
[:COMPLEX,REAL:] is V1() non empty non trivial V30() set
bool [:COMPLEX,REAL:] is non empty non trivial V30() set
{} is V1() non-empty empty-yielding V4( NAT ) Function-like one-to-one constant functional empty trivial V25() V29() V30() V31() V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex V43() ext-real non negative V163() V164() V165() V166() V167() V168() V169() set
the V1() non-empty empty-yielding V4( NAT ) Function-like one-to-one constant functional empty trivial V25() V29() V30() V31() V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex V43() ext-real non negative V163() V164() V165() V166() V167() V168() V169() set is V1() non-empty empty-yielding V4( NAT ) Function-like one-to-one constant functional empty trivial V25() V29() V30() V31() V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex V43() ext-real non negative V163() V164() V165() V166() V167() V168() V169() set
3 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
0 is V1() non-empty empty-yielding V4( NAT ) Function-like one-to-one constant functional empty trivial V25() V29() V30() V31() V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() V169() Element of NAT
4 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
K48({}) is V1() non-empty empty-yielding V4( NAT ) Function-like one-to-one constant functional empty trivial V25() V29() V30() V31() V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex V43() ext-real non negative V163() V164() V165() V166() V167() V168() V169() set
rng {} is V1() non-empty empty-yielding V4( NAT ) Function-like one-to-one constant functional empty trivial V25() V29() V30() V31() V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex V43() ext-real non negative V163() V164() V165() V166() V167() V168() V169() set
f is non empty set
g is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
dom g is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. h is Element of f
g . h is set
g . z is set
g /. z is Element of f
h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g . h is set
z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g . z is set
g /. h is Element of f
g /. z is Element of f
f is non empty set
g is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
len g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. (len g) is Element of f
(g /. (len g)) .. g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((g /. (len g)) .. g) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
h is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
Rev h is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
(Rev h) /. 1 is Element of f
((Rev h) /. 1) .. (Rev h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((g /. (len g)) .. g) + (((Rev h) /. 1) .. (Rev h)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
Rev g is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
(g /. (len g)) .. (Rev g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((g /. (len g)) .. g) + ((g /. (len g)) .. (Rev g)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f is non empty set
g is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
len g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /^ (len g) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
f is non empty set
g is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
len g is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. (len g) is Element of f
rng g is non empty V30() set
dom g is non empty V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
f is non empty set
g is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
h is set
dom g is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
z is set
g . z is set
k is set
g /. k is Element of f
A is set
g . A is set
g /. A is Element of f
z is set
g /. z is Element of f
k is set
g . k is set
g /. k is Element of f
g . z is set
f is non empty set
g is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
len g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. (len g) is Element of f
g -: (g /. (len g)) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
(g /. (len g)) .. g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g | ((g /. (len g)) .. g) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
g | (len g) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
f is non empty set
g is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
len g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. (len g) is Element of f
g :- (g /. (len g)) is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
<*(g /. (len g))*> is V1() V4( NAT ) V5(f) Function-like constant non empty trivial V30() 1 -element FinSequence-like FinSubsequence-like FinSequence of f
(g /. (len g)) .. g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /^ ((g /. (len g)) .. g) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
<*(g /. (len g))*> ^ (g /^ ((g /. (len g)) .. g)) is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
g /^ (len g) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
<*(g /. (len g))*> ^ (g /^ (len g)) is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
<*(g /. (len g))*> ^ {} is V1() V4( NAT ) Function-like non empty V30() FinSequence-like FinSubsequence-like set
f is non empty set
g is Element of f
h is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
h :- g is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
len (h :- g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
<*g*> is V1() V4( NAT ) V5(f) Function-like constant non empty trivial V30() 1 -element FinSequence-like FinSubsequence-like FinSequence of f
g .. h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
h /^ (g .. h) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
<*g*> ^ (h /^ (g .. h)) is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
len (<*g*> ^ (h /^ (g .. h))) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len <*g*> is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len (h /^ (g .. h)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len <*g*>) + (len (h /^ (g .. h))) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
1 + (len (h /^ (g .. h))) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f is non empty set
g is Element of f
h is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
rng h is V30() set
h :- g is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
len (h :- g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g .. h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len h) - (g .. h) is complex V43() ext-real set
(len h) - 1 is complex V43() ext-real set
((len h) - (g .. h)) + 1 is complex V43() ext-real set
(len (h :- g)) - 1 is complex V43() ext-real set
f is non empty set
g is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like circular FinSequence of f
Rev g is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
(Rev g) /. 1 is Element of f
len g is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. (len g) is Element of f
g /. 1 is Element of f
(Rev g) /. (len g) is Element of f
len (Rev g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rev g) /. (len (Rev g)) is Element of f
f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g is non empty set
h is Element of g
z is V1() V4( NAT ) V5(g) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of g
rng z is V30() set
z :- h is V1() V4( NAT ) V5(g) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of g
len (z :- h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
Rotate (z,h) is V1() V4( NAT ) V5(g) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of g
(Rotate (z,h)) /. f is Element of g
h .. z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f -' 1) + (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z /. ((f -' 1) + (h .. z)) is Element of g
dom (z :- h) is non empty V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
(f -' 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z -: h is V1() V4( NAT ) V5(g) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of g
(z -: h) /^ 1 is V1() V4( NAT ) V5(g) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of g
(z :- h) ^ ((z -: h) /^ 1) is V1() V4( NAT ) V5(g) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of g
(z :- h) /. f is Element of g
f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g is non empty set
h is Element of g
z is V1() V4( NAT ) V5(g) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of g
rng z is V30() set
h .. z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z /. f is Element of g
Rotate (z,h) is V1() V4( NAT ) V5(g) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of g
(f + 1) -' (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (z,h)) /. ((f + 1) -' (h .. z)) is Element of g
1 + (h .. z) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len z) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f + 1) - (h .. z) is complex V43() ext-real set
((len z) + 1) - (h .. z) is complex V43() ext-real set
(len z) - (h .. z) is complex V43() ext-real set
((len z) - (h .. z)) + 1 is complex V43() ext-real set
z :- h is V1() V4( NAT ) V5(g) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of g
len (z :- h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((f + 1) -' (h .. z)) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(((f + 1) -' (h .. z)) -' 1) + (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f -' (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f -' (h .. z)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((f -' (h .. z)) + 1) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(((f -' (h .. z)) + 1) -' 1) + (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f -' (h .. z)) + (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f is non empty set
g is Element of f
h is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
rng h is V30() set
Rotate (h,g) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
h :- g is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
len (h :- g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (h,g)) /. (len (h :- g)) is Element of f
len h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
h /. (len h) is Element of f
g .. h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len h) - (g .. h) is complex V43() ext-real set
(len (h :- g)) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len (h :- g)) -' 1) + (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + 1) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z + 1) -' 1) + (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len h) - (g .. h)) + (g .. h) is complex V43() ext-real set
f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g is non empty set
h is Element of g
z is V1() V4( NAT ) V5(g) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of g
rng z is V30() set
z :- h is V1() V4( NAT ) V5(g) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of g
len (z :- h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
Rotate (z,h) is V1() V4( NAT ) V5(g) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of g
(Rotate (z,h)) /. f is Element of g
h .. z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f + (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f + (h .. z)) -' (len z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z /. ((f + (h .. z)) -' (len z)) is Element of g
z -: h is V1() V4( NAT ) V5(g) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of g
len (z -: h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f -' (len (z :- h)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f -' (len (z :- h))) + (len (z :- h)) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z -: h) /^ 1 is V1() V4( NAT ) V5(g) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of g
(z :- h) ^ ((z -: h) /^ 1) is V1() V4( NAT ) V5(g) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of g
len ((z -: h) /^ 1) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len (z -: h)) - 1 is complex V43() ext-real set
(h .. z) + (len z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len z) - (h .. z) is complex V43() ext-real set
(len z) -' (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len z) -' (h .. z)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len z) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
Seg (h .. z) is V30() h .. z -element V163() V164() V165() V166() V167() V168() Element of bool NAT
(h .. z) + ((len z) -' (h .. z)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f -' ((len z) -' (h .. z)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f -' (((len z) -' (h .. z)) + 1) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f -' (((len z) -' (h .. z)) + 1)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(((len z) -' (h .. z)) + 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
dom ((z -: h) /^ 1) is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
((z -: h) /^ 1) /. (f -' (((len z) -' (h .. z)) + 1)) is Element of g
(z -: h) /. ((f -' (((len z) -' (h .. z)) + 1)) + 1) is Element of g
(z -: h) /. (f -' ((len z) -' (h .. z))) is Element of g
f - ((len z) -' (h .. z)) is complex V43() ext-real set
(z -: h) /. (f - ((len z) -' (h .. z))) is Element of g
f - ((len z) - (h .. z)) is complex V43() ext-real set
(z -: h) /. (f - ((len z) - (h .. z))) is Element of g
(f + (h .. z)) - (len z) is complex V43() ext-real set
(z -: h) /. ((f + (h .. z)) - (len z)) is Element of g
(z -: h) /. ((f + (h .. z)) -' (len z)) is Element of g
f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g is non empty set
h is Element of g
z is V1() V4( NAT ) V5(g) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of g
rng z is V30() set
h .. z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z /. f is Element of g
Rotate (z,h) is V1() V4( NAT ) V5(g) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of g
len z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f + (len z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f + (len z)) -' (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (z,h)) /. ((f + (len z)) -' (h .. z)) is Element of g
(len z) -' (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len z) -' f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len z) -' (h .. z)) + f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len z) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f + (len z)) - (h .. z) is complex V43() ext-real set
((len z) + 1) - (h .. z) is complex V43() ext-real set
(len z) - (h .. z) is complex V43() ext-real set
f + ((len z) - (h .. z)) is complex V43() ext-real set
((len z) - (h .. z)) + 1 is complex V43() ext-real set
f + ((len z) -' (h .. z)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z :- h is V1() V4( NAT ) V5(g) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of g
len (z :- h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((f + (len z)) -' (h .. z)) + (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(((f + (len z)) -' (h .. z)) + (h .. z)) -' (len z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f + (len z)) -' (len z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f is non empty set
g is Element of f
h is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
Rotate (h,g) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
len (Rotate (h,g)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
rng h is V30() set
rng h is V30() set
h -: g is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
len (h -: g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
h :- g is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
(h -: g) /^ 1 is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
(h :- g) ^ ((h -: g) /^ 1) is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
len ((h :- g) ^ ((h -: g) /^ 1)) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len (h :- g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len ((h -: g) /^ 1) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len (h :- g)) + (len ((h -: g) /^ 1)) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len (h -: g)) - 1 is complex V43() ext-real set
(len (h :- g)) + ((len (h -: g)) - 1) is complex V43() ext-real set
(len (h :- g)) + (len (h -: g)) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len (h :- g)) + (len (h -: g))) - 1 is complex V43() ext-real set
g .. h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len h) - (g .. h) is complex V43() ext-real set
((len h) - (g .. h)) + 1 is complex V43() ext-real set
(((len h) - (g .. h)) + 1) + (len (h -: g)) is complex V43() ext-real set
((((len h) - (g .. h)) + 1) + (len (h -: g))) - 1 is complex V43() ext-real set
((len h) - (g .. h)) + (len (h -: g)) is complex V43() ext-real set
((len h) - (g .. h)) + (g .. h) is complex V43() ext-real set
rng h is V30() set
f is non empty set
g is Element of f
h is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
Rotate (h,g) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
dom (Rotate (h,g)) is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
dom h is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
len (Rotate (h,g)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f is non empty set
g is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like circular FinSequence of f
len g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. 1 is Element of f
h is Element of f
Rotate (g,h) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
Rotate ((Rotate (g,h)),(g /. 1)) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
rng g is V30() set
Rotate (g,(g /. 1)) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
Rotate (g,(g /. 1)) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
rng g is V30() set
g -: h is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
(g -: h) /. 1 is Element of f
g /. (len g) is Element of f
g :- h is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
len (g :- h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(g :- h) /. (len (g :- h)) is Element of f
rng (g :- h) is non empty V30() set
h .. g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
dom (g :- h) is non empty V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
z is set
(g :- h) /. z is Element of f
k is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
A is V25() V29() V30() cardinal complex V43() ext-real non negative set
A + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) - (h .. g) is complex V43() ext-real set
((len g) - (h .. g)) + 1 is complex V43() ext-real set
i2 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
i2 + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
i2 + (h .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(g :- h) /. (i2 + 1) is Element of f
g /. (i2 + (h .. g)) is Element of f
rng (Rotate (g,h)) is V30() set
(g -: h) /^ 1 is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
(g :- h) ^ ((g -: h) /^ 1) is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
((g :- h) ^ ((g -: h) /^ 1)) :- (g /. 1) is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
((g :- h) ^ ((g -: h) /^ 1)) -: (g /. 1) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
(((g :- h) ^ ((g -: h) /^ 1)) -: (g /. 1)) /^ 1 is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
(((g :- h) ^ ((g -: h) /^ 1)) :- (g /. 1)) ^ ((((g :- h) ^ ((g -: h) /^ 1)) -: (g /. 1)) /^ 1) is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
(g :- h) :- (g /. 1) is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
((g :- h) :- (g /. 1)) ^ ((g -: h) /^ 1) is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
(((g :- h) :- (g /. 1)) ^ ((g -: h) /^ 1)) ^ ((((g :- h) ^ ((g -: h) /^ 1)) -: (g /. 1)) /^ 1) is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
(g :- h) -: (g /. 1) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
((g :- h) -: (g /. 1)) /^ 1 is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
(((g :- h) :- (g /. 1)) ^ ((g -: h) /^ 1)) ^ (((g :- h) -: (g /. 1)) /^ 1) is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
<*(g /. 1)*> is V1() V4( NAT ) V5(f) Function-like constant non empty trivial V30() 1 -element FinSequence-like FinSubsequence-like FinSequence of f
<*(g /. 1)*> ^ ((g -: h) /^ 1) is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
(<*(g /. 1)*> ^ ((g -: h) /^ 1)) ^ (((g :- h) -: (g /. 1)) /^ 1) is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of f
(g -: h) ^ (((g :- h) -: (g /. 1)) /^ 1) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
(g :- h) /^ 1 is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
(g -: h) ^ ((g :- h) /^ 1) is V1() V4( NAT ) V5(f) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of f
rng g is V30() set
f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g is non empty set
h is Element of g
z is V1() V4( NAT ) V5(g) Function-like V30() FinSequence-like FinSubsequence-like circular FinSequence of g
rng z is V30() set
z :- h is V1() V4( NAT ) V5(g) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of g
len (z :- h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
Rotate (z,h) is V1() V4( NAT ) V5(g) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of g
(Rotate (z,h)) /. f is Element of g
h .. z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f + (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f + (h .. z)) -' (len z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z /. ((f + (h .. z)) -' (len z)) is Element of g
(len z) - (h .. z) is complex V43() ext-real set
(len z) -' (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len z) - (h .. z)) + 1 is complex V43() ext-real set
f -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f -' 1) + (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z /. ((f -' 1) + (h .. z)) is Element of g
((len z) -' (h .. z)) + (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z /. (((len z) -' (h .. z)) + (h .. z)) is Element of g
z /. (len z) is Element of g
z /. 1 is Element of g
(len z) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len z) + 1) -' (len z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z /. (((len z) + 1) -' (len z)) is Element of g
f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g is non empty set
h is Element of g
z is V1() V4( NAT ) V5(g) Function-like V30() FinSequence-like FinSubsequence-like circular FinSequence of g
rng z is V30() set
h .. z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z /. f is Element of g
Rotate (z,h) is V1() V4( NAT ) V5(g) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of g
len z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f + (len z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f + (len z)) -' (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (z,h)) /. ((f + (len z)) -' (h .. z)) is Element of g
(len z) -' (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len z) -' f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len z) -' (h .. z)) + f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len z) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len z) + 1) - (h .. z) is complex V43() ext-real set
(f + (len z)) - (h .. z) is complex V43() ext-real set
(len z) - (h .. z) is complex V43() ext-real set
((len z) - (h .. z)) + 1 is complex V43() ext-real set
f + ((len z) - (h .. z)) is complex V43() ext-real set
f + ((len z) -' (h .. z)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z :- h is V1() V4( NAT ) V5(g) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of g
len (z :- h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((f + (len z)) -' (h .. z)) + (h .. z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(((f + (len z)) -' (h .. z)) + (h .. z)) -' (len z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f + (len z)) -' (len z) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f is non empty non trivial set
g is Element of f
h is Element of f
<*g,h,g*> is V1() V4( NAT ) V5(f) Function-like non empty non trivial V30() 3 -element FinSequence-like FinSubsequence-like FinSequence of f
z is V1() V4( NAT ) V5(f) Function-like non empty non trivial V30() 3 -element FinSequence-like FinSubsequence-like FinSequence of f
z . 1 is set
z . 2 is set
dom z is non empty non trivial V30() 3 -element V163() V164() V165() V166() V167() V168() Element of bool NAT
len z is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z /. 1 is Element of f
z /. (len z) is Element of f
f is non empty non trivial set
h is V1() V4( NAT ) V5(f) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular FinSequence of f
g is Element of f
Rotate (h,g) is V1() V4( NAT ) V5(f) Function-like non empty V30() FinSequence-like FinSubsequence-like circular FinSequence of f
rng h is non empty non trivial V30() set
rng h is non empty non trivial V30() set
dom (Rotate (h,g)) is non empty V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
dom h is non empty non trivial V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
h /. z is Element of f
h /. k is Element of f
len h is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g .. h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len h) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + ((len h) -' (g .. h)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + (len h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + (len h)) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k + ((len h) -' (g .. h)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k + (len h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(k + (len h)) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len h) + (g .. h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (h,g)) /. ((z + (len h)) -' (g .. h)) is Element of f
(Rotate (h,g)) /. ((k + (len h)) -' (g .. h)) is Element of f
1 + (g .. h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(k + 1) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len h) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + ((len h) -' (g .. h)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + (len h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + (len h)) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len h) + (g .. h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (h,g)) /. ((z + (len h)) -' (g .. h)) is Element of f
(Rotate (h,g)) /. ((k + 1) -' (g .. h)) is Element of f
1 + (g .. h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + 1) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len h) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k + ((len h) -' (g .. h)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k + (len h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(k + (len h)) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len h) + (g .. h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (h,g)) /. ((k + (len h)) -' (g .. h)) is Element of f
(Rotate (h,g)) /. ((z + 1) -' (g .. h)) is Element of f
1 + (g .. h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(k + 1) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + 1) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len h) + (g .. h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (h,g)) /. ((k + 1) -' (g .. h)) is Element of f
(Rotate (h,g)) /. ((z + 1) -' (g .. h)) is Element of f
rng h is non empty non trivial V30() set
f is non empty V25() V29() V30() cardinal complex V43() ext-real non negative set
0.REAL f is f -element FinSequence-like V154() Element of the U1 of (TOP-REAL f)
TOP-REAL f is non empty TopSpace-like V96() V121() V122() V123() V124() V125() V126() V127() strict RLTopStruct
the U1 of (TOP-REAL f) is non empty set
1.REAL f is f -element FinSequence-like V154() Element of the U1 of (TOP-REAL f)
Seg f is non empty V30() f -element V163() V164() V165() V166() V167() V168() Element of bool NAT
f |-> {} is V1() V4( NAT ) Function-like V30() FinSequence-like FinSubsequence-like set
(f |-> {}) . 1 is set
f |-> 1 is V1() V4( NAT ) V5( NAT ) Function-like V30() FinSequence-like FinSubsequence-like Element of f -tuples_on NAT
f -tuples_on NAT is functional FinSequence-membered FinSequenceSet of NAT
(f |-> 1) . 1 is set
1* f is V1() V4( NAT ) V5( REAL ) Function-like V30() f -element FinSequence-like FinSubsequence-like Element of REAL f
REAL f is functional non empty FinSequence-membered FinSequenceSet of REAL
f is non empty V25() V29() V30() cardinal complex V43() ext-real non negative set
TOP-REAL f is non empty TopSpace-like V96() V121() V122() V123() V124() V125() V126() V127() strict RLTopStruct
the U1 of (TOP-REAL f) is non empty set
1.REAL f is f -element FinSequence-like V154() Element of the U1 of (TOP-REAL f)
g is f -element FinSequence-like V154() Element of the U1 of (TOP-REAL f)
0. (TOP-REAL f) is f -element FinSequence-like zero V154() Element of the U1 of (TOP-REAL f)
the U2 of (TOP-REAL f) is f -element FinSequence-like V154() Element of the U1 of (TOP-REAL f)
0.REAL f is f -element FinSequence-like V154() Element of the U1 of (TOP-REAL f)
f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
rng f is V30() set
X_axis f is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (X_axis f) is V30() set
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
rng g is V30() set
X_axis g is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (X_axis g) is V30() set
dom (X_axis g) is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
dom g is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
h is set
dom (X_axis f) is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
z is set
(X_axis f) . z is set
k is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(X_axis f) . k is set
f /. k is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(f /. k) `1 is complex V43() ext-real Element of REAL
dom f is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
A is set
g . A is set
i2 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. i2 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(X_axis g) . i2 is set
f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
rng f is V30() set
X_axis f is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (X_axis f) is V30() set
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
rng g is V30() set
X_axis g is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (X_axis g) is V30() set
f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
rng f is V30() set
Y_axis f is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (Y_axis f) is V30() set
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
rng g is V30() set
Y_axis g is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (Y_axis g) is V30() set
dom (Y_axis g) is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
dom g is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
h is set
dom (Y_axis f) is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
z is set
(Y_axis f) . z is set
k is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Y_axis f) . k is set
f /. k is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(f /. k) `2 is complex V43() ext-real Element of REAL
dom f is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
A is set
g . A is set
i2 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. i2 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(Y_axis g) . i2 is set
f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
rng f is V30() set
Y_axis f is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (Y_axis f) is V30() set
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
rng g is V30() set
Y_axis g is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (Y_axis g) is V30() set
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like circular special FinSequence of the U1 of (TOP-REAL 2)
f is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
Rotate (g,f) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
rng g is V30() set
rng g is V30() set
len (Rotate (g,f)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
h is V25() V29() V30() cardinal complex V43() ext-real non negative set
h + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (g,f)) /. h is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
((Rotate (g,f)) /. h) `1 is complex V43() ext-real Element of REAL
(Rotate (g,f)) /. (h + 1) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
((Rotate (g,f)) /. (h + 1)) `1 is complex V43() ext-real Element of REAL
((Rotate (g,f)) /. h) `2 is complex V43() ext-real Element of REAL
((Rotate (g,f)) /. (h + 1)) `2 is complex V43() ext-real Element of REAL
g :- f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (g :- f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f .. g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) - (f .. g) is complex V43() ext-real set
((len g) - (f .. g)) + 1 is complex V43() ext-real set
(h + 1) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h + 1) -' 1) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
h + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
h -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(h -' 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h -' 1) + 1) + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(h -' 1) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h -' 1) + (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. (((h -' 1) + (f .. g)) + 1) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
1 + {} is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len g) + 1) - (f .. g) is complex V43() ext-real set
g /. ((h -' 1) + (f .. g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
h + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(h + (f .. g)) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. ((h + (f .. g)) -' (len g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
h - ((len g) - (f .. g)) is complex V43() ext-real set
(h + (f .. g)) - (len g) is complex V43() ext-real set
(h + 1) + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h + 1) + (f .. g)) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(h + (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h + (f .. g)) + 1) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h + (f .. g)) -' (len g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. (((h + (f .. g)) -' (len g)) + 1) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(len g) + (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h + (f .. g)) + 1) - (len g) is complex V43() ext-real set
((h + (f .. g)) - (len g)) + 1 is complex V43() ext-real set
rng g is V30() set
f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
h is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
rng h is V30() set
h :- g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (h :- g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
Rotate (h,g) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
LSeg ((Rotate (h,g)),f) is Element of bool the U1 of (TOP-REAL 2)
g .. h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f -' 1) + (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg (h,((f -' 1) + (g .. h))) is Element of bool the U1 of (TOP-REAL 2)
f + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len h) - (g .. h) is complex V43() ext-real set
((len h) - (g .. h)) + 1 is complex V43() ext-real set
f - 1 is complex V43() ext-real set
((f -' 1) + (g .. h)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(g .. h) - 1 is complex V43() ext-real set
(len h) - ((g .. h) - 1) is complex V43() ext-real set
{} + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f -' 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((f -' 1) + 1) + (g .. h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f + (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f + 1) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((f + 1) -' 1) + (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (h,g)) /. (f + 1) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
h /. (((f -' 1) + (g .. h)) + 1) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
len (Rotate (h,g)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (h,g)) /. f is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
h /. ((f -' 1) + (g .. h)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
LSeg ((h /. ((f -' 1) + (g .. h))),(h /. (((f -' 1) + (g .. h)) + 1))) is Element of bool the U1 of (TOP-REAL 2)
f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
h is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
rng h is V30() set
g .. h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg (h,f) is Element of bool the U1 of (TOP-REAL 2)
Rotate (h,g) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
f -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f -' (g .. h)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg ((Rotate (h,g)),((f -' (g .. h)) + 1)) is Element of bool the U1 of (TOP-REAL 2)
(len h) - (g .. h) is complex V43() ext-real set
f - (g .. h) is complex V43() ext-real set
((len h) - (g .. h)) + 1 is complex V43() ext-real set
h :- g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (h :- g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
1 + (g .. h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f + 1) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((f -' (g .. h)) + 1) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(((f -' (g .. h)) + 1) -' 1) + (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f -' (g .. h)) + (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like circular FinSequence of the U1 of (TOP-REAL 2)
X_axis g is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (X_axis g) is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like V156() FinSequence of REAL
Rotate (g,f) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
X_axis (Rotate (g,f)) is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (X_axis (Rotate (g,f))) is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like V156() FinSequence of REAL
rng g is V30() set
rng g is V30() set
rng (Rotate (g,f)) is V30() set
rng (X_axis (Rotate (g,f))) is V30() set
rng (X_axis g) is V30() set
rng (Incr (X_axis (Rotate (g,f)))) is V30() set
len (Incr (X_axis (Rotate (g,f)))) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
card (rng (X_axis g)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
rng g is V30() set
f is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like circular FinSequence of the U1 of (TOP-REAL 2)
Y_axis g is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (Y_axis g) is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like V156() FinSequence of REAL
Rotate (g,f) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Y_axis (Rotate (g,f)) is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (Y_axis (Rotate (g,f))) is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like V156() FinSequence of REAL
rng g is V30() set
rng g is V30() set
rng (Rotate (g,f)) is V30() set
rng (Y_axis (Rotate (g,f))) is V30() set
rng (Y_axis g) is V30() set
rng (Incr (Y_axis (Rotate (g,f)))) is V30() set
len (Incr (Y_axis (Rotate (g,f)))) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
card (rng (Y_axis g)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
rng g is V30() set
f is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like circular FinSequence of the U1 of (TOP-REAL 2)
Rotate (g,f) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like circular FinSequence of the U1 of (TOP-REAL 2)
GoB (Rotate (g,f)) is V1() non empty-yielding V4( NAT ) V5( the U1 of (TOP-REAL 2) * ) Function-like V30() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the U1 of (TOP-REAL 2) *
GoB g is V1() non empty-yielding V4( NAT ) V5( the U1 of (TOP-REAL 2) * ) Function-like V30() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the U1 of (TOP-REAL 2) *
X_axis g is V1() V4( NAT ) V5( REAL ) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (X_axis g) is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like V156() FinSequence of REAL
X_axis (Rotate (g,f)) is V1() V4( NAT ) V5( REAL ) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (X_axis (Rotate (g,f))) is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like V156() FinSequence of REAL
Y_axis g is V1() V4( NAT ) V5( REAL ) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (Y_axis g) is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like V156() FinSequence of REAL
Y_axis (Rotate (g,f)) is V1() V4( NAT ) V5( REAL ) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (Y_axis (Rotate (g,f))) is V1() V4( NAT ) V5( REAL ) Function-like V30() FinSequence-like FinSubsequence-like V156() FinSequence of REAL
GoB ((Incr (X_axis g)),(Incr (Y_axis g))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2) * ) Function-like V30() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of (TOP-REAL 2) *
f is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
Rotate (g,f) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special FinSequence of the U1 of (TOP-REAL 2)
Rev (Rotate (g,f)) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
Rotate ((Rev g),f) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special FinSequence of the U1 of (TOP-REAL 2)
rng g is non empty non trivial V30() set
rng (Rev g) is non empty non trivial V30() set
g /. 1 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
len g is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rev g) /. (len g) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
len (Rev g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rev g) /. (len (Rev g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(Rev g) /. 1 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
rng g is non empty non trivial V30() set
g /. 1 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
f .. g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
dom g is non empty non trivial V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
g /. (f .. g) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g . (f .. g) is set
h is set
g /. h is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len g is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len g is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
rng g is non empty non trivial V30() set
g /. 1 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like circular s.c.c. FinSequence of the U1 of (TOP-REAL 2)
len f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len f) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg (f,((len f) -' 1)) is Element of bool the U1 of (TOP-REAL 2)
LSeg (f,1) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) is Element of bool the U1 of (TOP-REAL 2)
f /. 1 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
{(f /. 1)} is non empty trivial V30() 1 -element compact Element of bool the U1 of (TOP-REAL 2)
((len f) -' 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
1 + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(1 + 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
f /. ((len f) -' 1) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
f /. (len f) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
LSeg ((f /. ((len f) -' 1)),(f /. (len f))) is Element of bool the U1 of (TOP-REAL 2)
f /. (1 + 1) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
LSeg ((f /. 1),(f /. (1 + 1))) is Element of bool the U1 of (TOP-REAL 2)
LSeg (f,(1 + 1)) is Element of bool the U1 of (TOP-REAL 2)
3 + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len f) - 1 is complex V43() ext-real set
(len f) -' 2 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len f) -' 2) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len f) -' 1) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(((len f) -' 1) -' 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
2 + 2 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len f) - 2 is complex V43() ext-real set
LSeg (f,((len f) -' 2)) is Element of bool the U1 of (TOP-REAL 2)
g is set
f /. (len f) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
h is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like circular FinSequence of the U1 of (TOP-REAL 2)
rng h is V30() set
h :- g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (h :- g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
Rotate (h,g) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
LSeg ((Rotate (h,g)),f) is Element of bool the U1 of (TOP-REAL 2)
g .. h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f + (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f + (g .. h)) -' (len h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg (h,((f + (g .. h)) -' (len h))) is Element of bool the U1 of (TOP-REAL 2)
(len h) - (g .. h) is complex V43() ext-real set
((len h) - (g .. h)) + 1 is complex V43() ext-real set
(len h) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len h) -' (g .. h)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len h) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len h) + 1) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{} + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{} + f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len (Rotate (h,g)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f + 1) + (g .. h) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len h) + (len h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f + (g .. h)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((f + (g .. h)) + 1) -' (len h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((f + (g .. h)) -' (len h)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((f + 1) + (g .. h)) -' (len h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (h,g)) /. (f + 1) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
h /. (((f + (g .. h)) -' (len h)) + 1) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(Rotate (h,g)) /. f is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
h /. ((f + (g .. h)) -' (len h)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
LSeg ((h /. ((f + (g .. h)) -' (len h))),(h /. (((f + (g .. h)) -' (len h)) + 1))) is Element of bool the U1 of (TOP-REAL 2)
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like circular s.c.c. FinSequence of the U1 of (TOP-REAL 2)
f is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
Rotate (g,f) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
rng g is V30() set
rng g is V30() set
f .. g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. 1 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
rng g is V30() set
f .. g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. (len g) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g /. 1 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
rng g is V30() set
f .. g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g :- f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (g :- f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) - (f .. g) is complex V43() ext-real set
((len g) - (f .. g)) + 1 is complex V43() ext-real set
z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len (Rotate (g,f)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg ((Rotate (g,f)),z) is Element of bool the U1 of (TOP-REAL 2)
k is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg ((Rotate (g,f)),k) is Element of bool the U1 of (TOP-REAL 2)
z -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z -' 1) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{} + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg (g,((z -' 1) + (f .. g))) is Element of bool the U1 of (TOP-REAL 2)
k -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(k -' 1) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + 1) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z -' 1) + (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z -' 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z -' 1) + 1) + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z + 1) -' 1) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg (g,((k -' 1) + (f .. g))) is Element of bool the U1 of (TOP-REAL 2)
1 + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z -' 1) + (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{} + (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z -' 1) + (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z -' 1) + (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z -' 1) + (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z -' 1) + (len g)) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(k + 1) + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z -' 1) + (f .. g)) + (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(k + (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len g) -' (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((k + (f .. g)) + 1) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(k + (f .. g)) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((k + (f .. g)) -' (len g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg (g,((z -' 1) + (f .. g))) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g,((k + (f .. g)) -' (len g))) is Element of bool the U1 of (TOP-REAL 2)
k - ((len g) - (f .. g)) is complex V43() ext-real set
(k + (f .. g)) - (len g) is complex V43() ext-real set
z + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z -' 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z -' 1) + 1) + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z -' 1) + (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(k + (f .. g)) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg (g,((k + (f .. g)) -' (len g))) is Element of bool the U1 of (TOP-REAL 2)
z + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(k + 1) + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
1 + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k + (1 + (f .. g)) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(k + (1 + (f .. g))) - (len g) is complex V43() ext-real set
(k + (f .. g)) - (len g) is complex V43() ext-real set
((k + (f .. g)) - (len g)) + 1 is complex V43() ext-real set
((k + (f .. g)) -' (len g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + 1) + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + (f .. g)) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z + (f .. g)) -' (len g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z + (f .. g)) + 1) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z + 1) + (f .. g)) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg (g,((z + (f .. g)) -' (len g))) is Element of bool the U1 of (TOP-REAL 2)
rng g is V30() set
f .. g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
f is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
Rotate (g,f) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special s.c.c. FinSequence of the U1 of (TOP-REAL 2)
rng g is non empty non trivial V30() set
rng g is non empty non trivial V30() set
h is V25() V29() V30() cardinal complex V43() ext-real non negative set
h + 2 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len (Rotate (g,f)) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg ((Rotate (g,f)),h) is Element of bool the U1 of (TOP-REAL 2)
h + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg ((Rotate (g,f)),(h + 1)) is Element of bool the U1 of (TOP-REAL 2)
(LSeg ((Rotate (g,f)),h)) /\ (LSeg ((Rotate (g,f)),(h + 1))) is Element of bool the U1 of (TOP-REAL 2)
(Rotate (g,f)) /. (h + 1) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
{((Rotate (g,f)) /. (h + 1))} is non empty trivial V30() 1 -element set
len g is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{((Rotate (g,f)) /. (h + 1))} is non empty trivial V30() 1 -element compact Element of bool the U1 of (TOP-REAL 2)
(h + 1) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f .. g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h + 1) -' 1) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
h + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
h -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(h -' 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h -' 1) + 1) + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(h -' 1) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h -' 1) + (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g :- f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (g :- f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) - (f .. g) is complex V43() ext-real set
((len g) - (f .. g)) + 1 is complex V43() ext-real set
(len (g :- f)) + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len (g :- f)) + (f .. g)) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len g) + 1) - (len g) is complex V43() ext-real set
LSeg ((Rotate (g,f)),(len (g :- f))) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g,1) is Element of bool the U1 of (TOP-REAL 2)
(((len g) - (f .. g)) + 1) - 1 is complex V43() ext-real set
((((len g) - (f .. g)) + 1) - 1) - 1 is complex V43() ext-real set
(((((len g) - (f .. g)) + 1) - 1) - 1) + (f .. g) is complex V43() ext-real set
((len g) - (f .. g)) + (f .. g) is complex V43() ext-real set
(((len g) - (f .. g)) + (f .. g)) - 1 is complex V43() ext-real set
(len g) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg (g,((len g) -' 1)) is Element of bool the U1 of (TOP-REAL 2)
g /. 1 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
{(g /. 1)} is non empty trivial V30() 1 -element compact Element of bool the U1 of (TOP-REAL 2)
g /. (len g) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
{(g /. (len g))} is non empty trivial V30() 1 -element compact Element of bool the U1 of (TOP-REAL 2)
(((h -' 1) + (f .. g)) + 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
1 + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h -' 1) + (f .. g)) + (1 + 1) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
h + {} is V25() V29() V30() cardinal complex V43() ext-real non negative set
LSeg (g,((h -' 1) + (f .. g))) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g,(((h + 1) -' 1) + (f .. g))) is Element of bool the U1 of (TOP-REAL 2)
g /. (((h + 1) -' 1) + (f .. g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
{(g /. (((h + 1) -' 1) + (f .. g)))} is non empty trivial V30() 1 -element compact Element of bool the U1 of (TOP-REAL 2)
(h + 2) + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + (len g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(h + (f .. g)) + 2 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h + (f .. g)) + 2) - (len g) is complex V43() ext-real set
(h + (f .. g)) - (len g) is complex V43() ext-real set
((h + (f .. g)) - (len g)) + 2 is complex V43() ext-real set
(h + 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(h + (f .. g)) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{} + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(h + 1) + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h + 1) + (f .. g)) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(h + (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h + (f .. g)) + 1) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h + (f .. g)) -' (len g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
h + {} is V25() V29() V30() cardinal complex V43() ext-real non negative set
LSeg (g,((h + (f .. g)) -' (len g))) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g,(((h + 1) + (f .. g)) -' (len g))) is Element of bool the U1 of (TOP-REAL 2)
g /. (((h + 1) + (f .. g)) -' (len g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
{(g /. (((h + 1) + (f .. g)) -' (len g)))} is non empty trivial V30() 1 -element compact Element of bool the U1 of (TOP-REAL 2)
rng g is non empty non trivial V30() set
f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
h is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like circular FinSequence of the U1 of (TOP-REAL 2)
rng h is V30() set
g .. h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg (h,f) is Element of bool the U1 of (TOP-REAL 2)
Rotate (h,g) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f + (len h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f + (len h)) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg ((Rotate (h,g)),((f + (len h)) -' (g .. h))) is Element of bool the U1 of (TOP-REAL 2)
(len h) + (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len h) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len h) + 1) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len h) -' (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len h) -' (g .. h)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len h) - (g .. h) is complex V43() ext-real set
((len h) - (g .. h)) + 1 is complex V43() ext-real set
h :- g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (h :- g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((f + (len h)) -' (g .. h)) + (g .. h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(((f + (len h)) -' (g .. h)) + (g .. h)) -' (len h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f + (len h)) -' (len h) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like circular FinSequence of the U1 of (TOP-REAL 2)
Rotate (g,f) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (g,f)) is compact Element of bool the U1 of (TOP-REAL 2)
len (Rotate (g,f)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{ (LSeg ((Rotate (g,f)),b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Rotate (g,f)) ) } is set
union { (LSeg ((Rotate (g,f)),b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Rotate (g,f)) ) } is set
L~ g is compact Element of bool the U1 of (TOP-REAL 2)
len g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{ (LSeg (g,b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g ) } is set
union { (LSeg (g,b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g ) } is set
rng g is V30() set
rng g is V30() set
{ (LSeg (g,b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g ) } is set
{ (LSeg ((Rotate (g,f)),b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g ) } is set
f .. g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k is set
A is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg ((Rotate (g,f)),A) is Element of bool the U1 of (TOP-REAL 2)
A + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g :- f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (g :- f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) - (f .. g) is complex V43() ext-real set
((len g) - (f .. g)) + 1 is complex V43() ext-real set
(len g) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len g) -' (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
A -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(A -' 1) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((A -' 1) + (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
1 + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
A + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(A + (f .. g)) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg (g,((A -' 1) + (f .. g))) is Element of bool the U1 of (TOP-REAL 2)
g :- f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (g :- f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) - (f .. g) is complex V43() ext-real set
((len g) - (f .. g)) + 1 is complex V43() ext-real set
(len g) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len g) -' (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
1 + (len g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(1 + (len g)) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
A + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(A + (f .. g)) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(A + 1) + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(A + (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((A + (f .. g)) + 1) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((A + (f .. g)) -' (len g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg (g,((A + (f .. g)) -' (len g))) is Element of bool the U1 of (TOP-REAL 2)
g :- f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (g :- f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k is set
A is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg (g,A) is Element of bool the U1 of (TOP-REAL 2)
A + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(A + 1) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
A -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(A -' (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((A -' (f .. g)) + 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
1 + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg ((Rotate (g,f)),((A -' (f .. g)) + 1)) is Element of bool the U1 of (TOP-REAL 2)
(A + 1) + (len g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
A + (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(A + (len g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((A + (len g)) + 1) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(A + (len g)) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((A + (len g)) -' (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
1 + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
LSeg ((Rotate (g,f)),((A + (len g)) -' (f .. g))) is Element of bool the U1 of (TOP-REAL 2)
rng g is V30() set
f is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like circular FinSequence of the U1 of (TOP-REAL 2)
Rotate (g,f) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
h is V1() non empty-yielding V4( NAT ) V5( the U1 of (TOP-REAL 2) * ) Function-like V30() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the U1 of (TOP-REAL 2) *
dom g is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
dom (Rotate (g,f)) is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
len g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len (Rotate (g,f)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
rng g is V30() set
rng g is V30() set
f .. g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
Indices h is set
z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (g,f)) /. z is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g :- f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (g :- f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) - (f .. g) is complex V43() ext-real set
((len g) - (f .. g)) + 1 is complex V43() ext-real set
(len g) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len g) -' (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len g) + 1) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + (f .. g)) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. ((z + (f .. g)) -' (len g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
k is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
A is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
[k,A] is non empty Element of [:NAT,NAT:]
[:NAT,NAT:] is V1() non empty non trivial V30() set
{k,A} is non empty V30() V34() V163() V164() V165() V166() V167() V168() set
{k} is non empty trivial V30() V34() 1 -element V163() V164() V165() V166() V167() V168() set
{{k,A},{k}} is non empty V30() V34() set
h * (k,A) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g :- f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (g :- f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) - (f .. g) is complex V43() ext-real set
((len g) - (f .. g)) + 1 is complex V43() ext-real set
(len g) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len g) -' (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z -' 1) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
1 + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + (f .. g)) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. ((z -' 1) + (f .. g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
k is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
A is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
[k,A] is non empty Element of [:NAT,NAT:]
[:NAT,NAT:] is V1() non empty non trivial V30() set
{k,A} is non empty V30() V34() V163() V164() V165() V166() V167() V168() set
{k} is non empty trivial V30() V34() 1 -element V163() V164() V165() V166() V167() V168() set
{{k,A},{k}} is non empty V30() V34() set
h * (k,A) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g :- f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (g :- f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (g,f)) /. z is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(Rotate (g,f)) /. (z + 1) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
k is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
A is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
[k,A] is non empty set
{k,A} is non empty V30() V34() V163() V164() V165() V166() V167() V168() set
{k} is non empty trivial V30() V34() 1 -element V163() V164() V165() V166() V167() V168() set
{{k,A},{k}} is non empty V30() V34() set
h * (k,A) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
i2 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k - i2 is complex V43() ext-real set
abs (k - i2) is complex V43() ext-real Element of REAL
j2 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
[i2,j2] is non empty set
{i2,j2} is non empty V30() V34() V163() V164() V165() V166() V167() V168() set
{i2} is non empty trivial V30() V34() 1 -element V163() V164() V165() V166() V167() V168() set
{{i2,j2},{i2}} is non empty V30() V34() set
h * (i2,j2) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
A - j2 is complex V43() ext-real set
abs (A - j2) is complex V43() ext-real Element of REAL
(abs (k - i2)) + (abs (A - j2)) is complex V43() ext-real set
[k,A] is non empty Element of [:NAT,NAT:]
[:NAT,NAT:] is V1() non empty non trivial V30() set
[i2,j2] is non empty Element of [:NAT,NAT:]
g :- f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (g :- f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) - (f .. g) is complex V43() ext-real set
((len g) - (f .. g)) + 1 is complex V43() ext-real set
(len g) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len g) -' (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len g) + 1) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + (f .. g)) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + 1) + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z + 1) + (f .. g)) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. (((z + 1) + (f .. g)) -' (len g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(z + (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z + (f .. g)) + 1) -' (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z + (f .. g)) -' (len g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. ((z + (f .. g)) -' (len g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g :- f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (g :- f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) - (f .. g) is complex V43() ext-real set
((len g) - (f .. g)) + 1 is complex V43() ext-real set
(len g) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len g) -' (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z -' 1) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
1 + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + (f .. g)) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + 1) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z + 1) -' 1) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z -' 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z -' 1) + 1) + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z -' 1) + (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. (((z + 1) -' 1) + (f .. g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(z + 1) + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z + 1) + (f .. g)) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. ((z -' 1) + (f .. g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g :- f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (g :- f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
Indices h is set
z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. z is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(len g) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + ((len g) -' (f .. g)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + (len g)) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (g,f)) /. ((z + (len g)) -' (f .. g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
k is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
A is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
[k,A] is non empty Element of [:NAT,NAT:]
[:NAT,NAT:] is V1() non empty non trivial V30() set
{k,A} is non empty V30() V34() V163() V164() V165() V166() V167() V168() set
{k} is non empty trivial V30() V34() 1 -element V163() V164() V165() V166() V167() V168() set
{{k,A},{k}} is non empty V30() V34() set
h * (k,A) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
1 + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + 1) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (g,f)) /. ((z + 1) -' (f .. g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
k is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
A is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
[k,A] is non empty Element of [:NAT,NAT:]
[:NAT,NAT:] is V1() non empty non trivial V30() set
{k,A} is non empty V30() V34() V163() V164() V165() V166() V167() V168() set
{k} is non empty trivial V30() V34() 1 -element V163() V164() V165() V166() V167() V168() set
{{k,A},{k}} is non empty V30() V34() set
h * (k,A) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. z is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g /. (z + 1) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
k is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
A is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
[k,A] is non empty set
{k,A} is non empty V30() V34() V163() V164() V165() V166() V167() V168() set
{k} is non empty trivial V30() V34() 1 -element V163() V164() V165() V166() V167() V168() set
{{k,A},{k}} is non empty V30() V34() set
h * (k,A) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
i2 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k - i2 is complex V43() ext-real set
abs (k - i2) is complex V43() ext-real Element of REAL
j2 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
[i2,j2] is non empty set
{i2,j2} is non empty V30() V34() V163() V164() V165() V166() V167() V168() set
{i2} is non empty trivial V30() V34() 1 -element V163() V164() V165() V166() V167() V168() set
{{i2,j2},{i2}} is non empty V30() V34() set
h * (i2,j2) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
A - j2 is complex V43() ext-real set
abs (A - j2) is complex V43() ext-real Element of REAL
(abs (k - i2)) + (abs (A - j2)) is complex V43() ext-real set
[k,A] is non empty Element of [:NAT,NAT:]
[:NAT,NAT:] is V1() non empty non trivial V30() set
[i2,j2] is non empty Element of [:NAT,NAT:]
(len g) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + ((len g) -' (f .. g)) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z + (len g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + (len g)) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + 1) + (len g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z + 1) + (len g)) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len g) -' (f .. g)) + (z + 1) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((len g) -' (f .. g)) + z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(((len g) -' (f .. g)) + z) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z + (len g)) -' (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + 1) + ((len g) -' (f .. g)) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (g,f)) /. (((z + 1) + (len g)) -' (f .. g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(Rotate (g,f)) /. ((z + (len g)) -' (f .. g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
1 + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(z + 1) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (g,f)) /. ((z + 1) -' (f .. g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(z + 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z + 1) + 1) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((z + 1) -' (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rotate (g,f)) /. (((z + 1) + 1) -' (f .. g)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
rng g is V30() set
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like circular standard FinSequence of the U1 of (TOP-REAL 2)
f is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
Rotate (g,f) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non empty V30() FinSequence-like FinSubsequence-like circular FinSequence of the U1 of (TOP-REAL 2)
GoB (Rotate (g,f)) is V1() non empty-yielding V4( NAT ) V5( the U1 of (TOP-REAL 2) * ) Function-like V30() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the U1 of (TOP-REAL 2) *
GoB g is V1() non empty-yielding V4( NAT ) V5( the U1 of (TOP-REAL 2) * ) Function-like V30() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the U1 of (TOP-REAL 2) *
f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
rng f is non empty non trivial V30() set
len f is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g .. f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
Rotate (f,g) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
left_cell (f,h) is Element of bool the U1 of (TOP-REAL 2)
h + (len f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(h + (len f)) -' (g .. f) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
left_cell ((Rotate (f,g)),((h + (len f)) -' (g .. f))) is Element of bool the U1 of (TOP-REAL 2)
h + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{} + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h + (len f)) -' (g .. f)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(h + (len f)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h + (len f)) + 1) -' (g .. f) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(h + 1) + (len f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len f) + (g .. f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
len (Rotate (f,g)) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((h + 1) + (len f)) -' (g .. f) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
GoB (Rotate (f,g)) is V1() non empty-yielding V4( NAT ) V5( the U1 of (TOP-REAL 2) * ) Function-like V30() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the U1 of (TOP-REAL 2) *
Indices (GoB (Rotate (f,g))) is set
(Rotate (f,g)) /. ((h + (len f)) -' (g .. f)) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(Rotate (f,g)) /. (((h + (len f)) -' (g .. f)) + 1) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
k is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
A is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
[k,A] is non empty Element of [:NAT,NAT:]
[:NAT,NAT:] is V1() non empty non trivial V30() set
{k,A} is non empty V30() V34() V163() V164() V165() V166() V167() V168() set
{k} is non empty trivial V30() V34() 1 -element V163() V164() V165() V166() V167() V168() set
{{k,A},{k}} is non empty V30() V34() set
i2 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
j2 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
[i2,j2] is non empty Element of [:NAT,NAT:]
{i2,j2} is non empty V30() V34() V163() V164() V165() V166() V167() V168() set
{i2} is non empty trivial V30() V34() 1 -element V163() V164() V165() V166() V167() V168() set
{{i2,j2},{i2}} is non empty V30() V34() set
(GoB (Rotate (f,g))) * (k,A) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(GoB (Rotate (f,g))) * (i2,j2) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
A + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
cell ((GoB (Rotate (f,g))),(k -' 1),A) is Element of bool the U1 of (TOP-REAL 2)
v_strip ((GoB (Rotate (f,g))),(k -' 1)) is Element of bool the U1 of (TOP-REAL 2)
h_strip ((GoB (Rotate (f,g))),A) is Element of bool the U1 of (TOP-REAL 2)
(v_strip ((GoB (Rotate (f,g))),(k -' 1))) /\ (h_strip ((GoB (Rotate (f,g))),A)) is Element of bool the U1 of (TOP-REAL 2)
k + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
cell ((GoB (Rotate (f,g))),k,A) is Element of bool the U1 of (TOP-REAL 2)
v_strip ((GoB (Rotate (f,g))),k) is Element of bool the U1 of (TOP-REAL 2)
(v_strip ((GoB (Rotate (f,g))),k)) /\ (h_strip ((GoB (Rotate (f,g))),A)) is Element of bool the U1 of (TOP-REAL 2)
i2 + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
j2 -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
cell ((GoB (Rotate (f,g))),i2,(j2 -' 1)) is Element of bool the U1 of (TOP-REAL 2)
v_strip ((GoB (Rotate (f,g))),i2) is Element of bool the U1 of (TOP-REAL 2)
h_strip ((GoB (Rotate (f,g))),(j2 -' 1)) is Element of bool the U1 of (TOP-REAL 2)
(v_strip ((GoB (Rotate (f,g))),i2)) /\ (h_strip ((GoB (Rotate (f,g))),(j2 -' 1))) is Element of bool the U1 of (TOP-REAL 2)
j2 + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
cell ((GoB (Rotate (f,g))),k,j2) is Element of bool the U1 of (TOP-REAL 2)
h_strip ((GoB (Rotate (f,g))),j2) is Element of bool the U1 of (TOP-REAL 2)
(v_strip ((GoB (Rotate (f,g))),k)) /\ (h_strip ((GoB (Rotate (f,g))),j2)) is Element of bool the U1 of (TOP-REAL 2)
GoB f is V1() non empty-yielding V4( NAT ) V5( the U1 of (TOP-REAL 2) * ) Function-like V30() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the U1 of (TOP-REAL 2) *
f /. h is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(GoB f) * (k,A) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
f /. (h + 1) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(GoB f) * (i2,j2) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
cell ((GoB f),(k -' 1),A) is Element of bool the U1 of (TOP-REAL 2)
v_strip ((GoB f),(k -' 1)) is Element of bool the U1 of (TOP-REAL 2)
h_strip ((GoB f),A) is Element of bool the U1 of (TOP-REAL 2)
(v_strip ((GoB f),(k -' 1))) /\ (h_strip ((GoB f),A)) is Element of bool the U1 of (TOP-REAL 2)
cell ((GoB f),k,A) is Element of bool the U1 of (TOP-REAL 2)
v_strip ((GoB f),k) is Element of bool the U1 of (TOP-REAL 2)
(v_strip ((GoB f),k)) /\ (h_strip ((GoB f),A)) is Element of bool the U1 of (TOP-REAL 2)
cell ((GoB f),i2,(j2 -' 1)) is Element of bool the U1 of (TOP-REAL 2)
v_strip ((GoB f),i2) is Element of bool the U1 of (TOP-REAL 2)
h_strip ((GoB f),(j2 -' 1)) is Element of bool the U1 of (TOP-REAL 2)
(v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),(j2 -' 1))) is Element of bool the U1 of (TOP-REAL 2)
cell ((GoB f),k,j2) is Element of bool the U1 of (TOP-REAL 2)
h_strip ((GoB f),j2) is Element of bool the U1 of (TOP-REAL 2)
(v_strip ((GoB f),k)) /\ (h_strip ((GoB f),j2)) is Element of bool the U1 of (TOP-REAL 2)
1 + (g .. f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
Rotate (g,f) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
LeftComp (Rotate (g,f)) is non empty Element of bool the U1 of (TOP-REAL 2)
LeftComp g is non empty Element of bool the U1 of (TOP-REAL 2)
rng g is non empty non trivial V30() set
f .. g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
L~ (Rotate (g,f)) is non empty compact Element of bool the U1 of (TOP-REAL 2)
len (Rotate (g,f)) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{ (LSeg ((Rotate (g,f)),b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Rotate (g,f)) ) } is set
union { (LSeg ((Rotate (g,f)),b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Rotate (g,f)) ) } is set
(L~ (Rotate (g,f))) ` is Element of bool the U1 of (TOP-REAL 2)
L~ g is non empty compact Element of bool the U1 of (TOP-REAL 2)
len g is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{ (LSeg (g,b<sub>1</sub>)) where b<sub>1</sub> is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len g ) } is set
union { (LSeg (g,b<sub>1</sub>)) where b<sub>1</sub> is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len g ) } is set
(L~ g) ` is Element of bool the U1 of (TOP-REAL 2)
dom g is non empty non trivial V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
g . 1 is set
g /. 1 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
1 + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
1 + (len g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
1 + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(1 + 1) + (len g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + (f .. g) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len g) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(1 + (len g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((1 + (len g)) + 1) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(1 + (len g)) -' (f .. g) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
((1 + (len g)) -' (f .. g)) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
left_cell (g,1) is Element of bool the U1 of (TOP-REAL 2)
left_cell ((Rotate (g,f)),((1 + (len g)) -' (f .. g))) is Element of bool the U1 of (TOP-REAL 2)
Int (left_cell (g,1)) is Element of bool the U1 of (TOP-REAL 2)
f is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
Rotate (g,f) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
RightComp (Rotate (g,f)) is non empty Element of bool the U1 of (TOP-REAL 2)
RightComp g is non empty Element of bool the U1 of (TOP-REAL 2)
Rev g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
LeftComp (Rev g) is non empty Element of bool the U1 of (TOP-REAL 2)
Rev (Rotate (g,f)) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
LeftComp (Rev (Rotate (g,f))) is non empty Element of bool the U1 of (TOP-REAL 2)
Rotate ((Rev g),f) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
LeftComp (Rotate ((Rev g),f)) is non empty Element of bool the U1 of (TOP-REAL 2)
f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
f /. 1 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
L~ f is non empty compact Element of bool the U1 of (TOP-REAL 2)
len f is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{ (LSeg (f,b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
union { (LSeg (f,b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
N-min (L~ f) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
Rev f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
1 + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(1 + 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len f) -' 1 is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
GoB f is V1() non empty-yielding V4( NAT ) V5( the U1 of (TOP-REAL 2) * ) Function-like V30() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the U1 of (TOP-REAL 2) *
width (GoB f) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
i_w_n f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
[(i_w_n f),(width (GoB f))] is non empty Element of [:NAT,NAT:]
[:NAT,NAT:] is V1() non empty non trivial V30() set
{(i_w_n f),(width (GoB f))} is non empty V30() V34() V163() V164() V165() V166() V167() V168() set
{(i_w_n f)} is non empty trivial V30() V34() 1 -element V163() V164() V165() V166() V167() V168() set
{{(i_w_n f),(width (GoB f))},{(i_w_n f)}} is non empty V30() V34() set
Indices (GoB f) is set
len (GoB f) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(GoB f) * ((i_w_n f),(width (GoB f))) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
dom f is non empty non trivial V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
f /. 2 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
[g,h] is non empty Element of [:NAT,NAT:]
{g,h} is non empty V30() V34() V163() V164() V165() V166() V167() V168() set
{g} is non empty trivial V30() V34() 1 -element V163() V164() V165() V166() V167() V168() set
{{g,h},{g}} is non empty V30() V34() set
(GoB f) * (g,h) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(GoB f) * (1,h) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
((GoB f) * (1,h)) `2 is complex V43() ext-real Element of REAL
N-bound (L~ f) is complex V43() ext-real Element of REAL
((GoB f) * (g,h)) `2 is complex V43() ext-real Element of REAL
N-most (L~ f) is Element of bool the U1 of (TOP-REAL 2)
(N-min (L~ f)) `1 is complex V43() ext-real Element of REAL
((GoB f) * (g,h)) `1 is complex V43() ext-real Element of REAL
(i_w_n f) - g is complex V43() ext-real set
abs ((i_w_n f) - g) is complex V43() ext-real Element of REAL
(width (GoB f)) - h is complex V43() ext-real set
abs ((width (GoB f)) - h) is complex V43() ext-real Element of REAL
(abs ((i_w_n f) - g)) + (abs ((width (GoB f)) - h)) is complex V43() ext-real set
(i_w_n f) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
h + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
i_e_n f is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f /. ((len f) -' 1) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
[z,k] is non empty Element of [:NAT,NAT:]
{z,k} is non empty V30() V34() V163() V164() V165() V166() V167() V168() set
{z} is non empty trivial V30() V34() 1 -element V163() V164() V165() V166() V167() V168() set
{{z,k},{z}} is non empty V30() V34() set
(GoB f) * (z,k) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(GoB f) * (1,k) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
((GoB f) * (1,k)) `2 is complex V43() ext-real Element of REAL
((GoB f) * (z,k)) `2 is complex V43() ext-real Element of REAL
((GoB f) * (z,k)) `1 is complex V43() ext-real Element of REAL
((len f) -' 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f /. (((len f) -' 1) + 1) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
z - (i_w_n f) is complex V43() ext-real set
abs (z - (i_w_n f)) is complex V43() ext-real Element of REAL
k - (width (GoB f)) is complex V43() ext-real set
abs (k - (width (GoB f))) is complex V43() ext-real Element of REAL
(abs (z - (i_w_n f))) + (abs (k - (width (GoB f)))) is complex V43() ext-real set
k + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(f /. 2) `2 is complex V43() ext-real Element of REAL
(GoB f) * (1,(width (GoB f))) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
((GoB f) * (1,(width (GoB f)))) `2 is complex V43() ext-real Element of REAL
(f /. ((len f) -' 1)) `2 is complex V43() ext-real Element of REAL
L~ (Rev f) is non empty compact Element of bool the U1 of (TOP-REAL 2)
len (Rev f) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{ (LSeg ((Rev f),b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Rev f) ) } is set
union { (LSeg ((Rev f),b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Rev f) ) } is set
A is non empty compact Element of bool the U1 of (TOP-REAL 2)
((len f) -' 1) + (1 + 1) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(((len f) -' 1) + 1) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(len f) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
(Rev f) /. 2 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(Rev f) /. 1 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
f /. (len f) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
N-min A is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
g is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
f is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
Rotate (g,f) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len g is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. 1 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g /. h is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
L~ (Rotate (g,f)) is non empty compact Element of bool the U1 of (TOP-REAL 2)
len (Rotate (g,f)) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{ (LSeg ((Rotate (g,f)),b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Rotate (g,f)) ) } is set
union { (LSeg ((Rotate (g,f)),b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Rotate (g,f)) ) } is set
L~ g is non empty compact Element of bool the U1 of (TOP-REAL 2)
{ (LSeg (g,b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g ) } is set
union { (LSeg (g,b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g ) } is set
N-min (L~ g) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (g,f)),(N-min (L~ g))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (g,f))) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (g,f)),(N-min (L~ (Rotate (g,f))))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
(Rotate ((Rotate (g,f)),(N-min (L~ (Rotate (g,f)))))) /. 2 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
N-most (L~ (Rotate (g,f))) is Element of bool the U1 of (TOP-REAL 2)
N-min (L~ g) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
n_w_n g is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
dom g is non empty non trivial V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
g /. (n_w_n g) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
(n_w_n g) + 1 is non empty V25() V29() V30() cardinal complex V43() V44() ext-real positive non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
g . (n_w_n g) is set
h is set
g /. h is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
z is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
Rotate (g,(N-min (L~ g))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
(Rotate (g,(N-min (L~ g)))) /. 2 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
N-most (L~ g) is Element of bool the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (g,f))) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (g,f)),(N-min (L~ (Rotate (g,f))))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
(Rotate ((Rotate (g,f)),(N-min (L~ (Rotate (g,f)))))) /. 2 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
N-most (L~ (Rotate (g,f))) is Element of bool the U1 of (TOP-REAL 2)
N-min (L~ g) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
Rev f is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
L~ f is non empty compact Element of bool the U1 of (TOP-REAL 2)
len f is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{ (LSeg (f,b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
union { (LSeg (f,b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
N-min (L~ f) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
f /. 1 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
L~ f is non empty compact Element of bool the U1 of (TOP-REAL 2)
len f is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{ (LSeg (f,b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
union { (LSeg (f,b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
N-min (L~ f) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
f /. 1 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
Rotate (f,(N-min (L~ f))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
h is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
f /. h is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
rng f is non empty non trivial V30() set
L~ (Rotate (f,(N-min (L~ f)))) is non empty compact Element of bool the U1 of (TOP-REAL 2)
len (Rotate (f,(N-min (L~ f)))) is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{ (LSeg ((Rotate (f,(N-min (L~ f)))),b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Rotate (f,(N-min (L~ f)))) ) } is set
union { (LSeg ((Rotate (f,(N-min (L~ f)))),b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (Rotate (f,(N-min (L~ f)))) ) } is set
(Rotate (f,(N-min (L~ f)))) /. 1 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (f,(N-min (L~ f))))) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
h is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
Rotate (h,(f /. 1)) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
Rev (Rotate (f,(N-min (L~ f)))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
(f /. 1) .. (Rotate (f,(N-min (L~ f)))) is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
dom (Rotate (f,(N-min (L~ f)))) is non empty non trivial V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
(Rotate (f,(N-min (L~ f)))) /. ((f /. 1) .. (Rotate (f,(N-min (L~ f))))) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
rng (Rotate (f,(N-min (L~ f)))) is non empty non trivial V30() set
(Rotate (f,(N-min (L~ f)))) . ((f /. 1) .. (Rotate (f,(N-min (L~ f))))) is set
z is set
(Rotate (f,(N-min (L~ f)))) /. z is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
k is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
k is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
Rotate ((Rotate (f,(N-min (L~ f)))),(f /. 1)) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
Rev (Rotate ((Rotate (f,(N-min (L~ f)))),(f /. 1))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
h is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
Rotate (h,(f /. 1)) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
Rev (Rotate (f,(N-min (L~ f)))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty non trivial V30() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
L~ f is non empty compact Element of bool the U1 of (TOP-REAL 2)
len f is non empty V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT
{ (LSeg (f,b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
union { (LSeg (f,b₁)) where b₁ is V25() V29() V30() cardinal complex V43() V44() ext-real non negative V162() V163() V164() V165() V166() V167() V168() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
N-min (L~ f) is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)
f /. 1 is 2 -element FinSequence-like V154() Element of the U1 of (TOP-REAL 2)