:: 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
is V1() non empty non trivial V30() set
is V1() non empty non trivial V30() set
bool is non empty non trivial V30() set
[:[:2,2:],REAL:] is V1() set
bool [:[:2,2:],REAL:] is set
bool 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 () is non empty set
the U1 of () * is functional non empty FinSequence-membered FinSequenceSet of the U1 of ()
[: the U1 of (),REAL:] is V1() non empty non trivial V30() set
bool [: the U1 of (),REAL:] is non empty non trivial V30() set
bool the U1 of () is set
is V1() non empty non trivial V30() set
bool is non empty non trivial V30() set
is V1() non empty non trivial V30() set
bool is non empty non trivial V30() 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

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

f is non empty set

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

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

(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

(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

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

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

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

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

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

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 .. 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 (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

rng h is V30() set

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

(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

rng z is V30() set

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) /^ 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

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

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

rng h is V30() set
Rotate (h,g) is V1() V4( NAT ) V5(f) Function-like 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

rng z is V30() set

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) 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

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

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

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

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) /^ 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

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

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) /. 1 is Element of f
g /. (len g) is Element 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)*> ^ ((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

rng z is V30() set

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

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

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

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 is non empty TopSpace-like V96() V121() V122() V123() V124() V125() V126() V127() strict RLTopStruct
the U1 of () is non empty set
1.REAL f is f -element FinSequence-like V154() Element of the U1 of ()
Seg f is non empty V30() f -element V163() V164() V165() V166() V167() V168() Element of bool NAT

() . 1 is set

(f |-> 1) . 1 is set

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 () is non empty set
1.REAL f is f -element FinSequence-like V154() Element of the U1 of ()
g is f -element FinSequence-like V154() Element of the U1 of ()
0. () is f -element FinSequence-like zero V154() Element of the U1 of ()
the U2 of () is f -element FinSequence-like V154() Element of the U1 of ()
0.REAL f is f -element FinSequence-like V154() Element of the U1 of ()
f is V1() V4( NAT ) V5( the U1 of ()) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of ()
rng f is V30() set

rng () is V30() set
g is V1() V4( NAT ) V5( the U1 of ()) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of ()
rng g is V30() set

rng () is V30() set
dom () 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 () is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
z is set
() . 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
() . k is set
f /. k is 2 -element FinSequence-like V154() Element of the U1 of ()
(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 ()
() . i2 is set
f is V1() V4( NAT ) V5( the U1 of ()) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of ()
rng f is V30() set

rng () is V30() set
g is V1() V4( NAT ) V5( the U1 of ()) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of ()
rng g is V30() set

rng () is V30() set
f is V1() V4( NAT ) V5( the U1 of ()) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of ()
rng f is V30() set

rng () is V30() set
g is V1() V4( NAT ) V5( the U1 of ()) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of ()
rng g is V30() set

rng () is V30() set
dom () 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 () is V30() V163() V164() V165() V166() V167() V168() Element of bool NAT
z is set
() . 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
() . k is set
f /. k is 2 -element FinSequence-like V154() Element of the U1 of ()
(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 ()
() . i2 is set
f is V1() V4( NAT ) V5( the U1 of ()) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of ()
rng f is V30() set

rng () is V30() set
g is V1() V4( NAT ) V5( the U1 of ()) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of ()
rng g is V30() set

rng () is V30() set
g is V1() V4( NAT ) V5( the U1 of ()) Function-like V30() FinSequence-like FinSubsequence-like circular special FinSequence of the U1 of ()
f is 2 -element FinSequence-like V154() Element of the U1 of ()
Rotate (g,f) is V1() V4( NAT ) V5( the U1 of ()) Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of ()
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 ()
((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 ()
((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 ()) Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the U1 of ()
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 ()
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 ()
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 ()
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()