:: SPRECT_5 semantic presentation

REAL is set
NAT is V6() V7() V8() non empty Element of K27(REAL)
K27(REAL) is set
NAT is V6() V7() V8() non empty set
K27(NAT) is set
K27(NAT) is set
1 is V6() V7() V8() V12() non empty ext-real positive V39() V43() Element of NAT
K28(1,1) is set
K27(K28(1,1)) is set
K28(K28(1,1),1) is set
K27(K28(K28(1,1),1)) is set
K28(K28(1,1),REAL) is set
K27(K28(K28(1,1),REAL)) is set
K28(REAL,REAL) is set
K28(K28(REAL,REAL),REAL) is set
K27(K28(K28(REAL,REAL),REAL)) is set
2 is V6() V7() V8() V12() non empty ext-real positive V39() V43() Element of NAT
K28(2,2) is set
K28(K28(2,2),REAL) is set
K27(K28(K28(2,2),REAL)) is set
COMPLEX is set
RAT is set
INT is set
K27(K28(REAL,REAL)) is set
TOP-REAL 2 is V47() V52() V161() L15()
the U1 of (TOP-REAL 2) is non empty V19() set
K27( the U1 of (TOP-REAL 2)) is set
K28( the U1 of (TOP-REAL 2),REAL) is set
K27(K28( the U1 of (TOP-REAL 2),REAL)) is set
{} is V6() V7() V8() V10() V11() V12() Function-like functional empty ext-real V39() V43() set
Seg 1 is Element of K27(NAT)
4 is V6() V7() V8() V12() non empty ext-real positive V39() V43() Element of NAT
0 is V6() V7() V8() V10() V11() V12() Function-like functional empty ext-real V39() V43() Element of NAT
len {} is V29() set
z is non empty set
g is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
p2 is Element of z
p2 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p3 is Element of z
p3 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
g | (p3 .. g) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
rng (g | (p3 .. g)) is set
p2 .. (g | (p3 .. g)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len (g | (p3 .. g)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is non empty set
g is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
rng g is set
p2 is Element of z
p2 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
g :- p2 is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
p3 is Element of z
p3 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p3 .. (g :- p2) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(p3 .. g) - (p2 .. g) is ext-real V39() V43() set
((p3 .. g) - (p2 .. g)) + 1 is ext-real V39() V43() set
g | (p2 .. g) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
g /^ (p2 .. g) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
(g | (p2 .. g)) ^ (g /^ (p2 .. g)) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
len g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len (g | (p2 .. g)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (g | (p2 .. g)) is set
rng (g /^ (p2 .. g)) is set
(rng (g | (p2 .. g))) \/ (rng (g /^ (p2 .. g))) is set
(rng (g /^ (p2 .. g))) \ (rng (g | (p2 .. g))) is Element of K27((rng (g /^ (p2 .. g))))
K27((rng (g /^ (p2 .. g)))) is set
p3 .. (g /^ (p2 .. g)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(p2 .. g) + (p3 .. (g /^ (p2 .. g))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
{p2} is non empty set
<*p2*> is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
rng <*p2*> is set
(rng (g /^ (p2 .. g))) \ (rng <*p2*>) is Element of K27((rng (g /^ (p2 .. g))))
<*p2*> ^ (g /^ (p2 .. g)) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
len <*p2*> is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(len <*p2*>) + (p3 .. (g /^ (p2 .. g))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is non empty set
g is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
rng g is set
p2 is Element of z
p2 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p3 is Element of z
p3 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
g -: p3 is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
p2 .. (g -: p3) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
g | (p3 .. g) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
rng (g | (p3 .. g)) is set
z is non empty set
g is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
rng g is set
p2 is Element of z
p2 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
Rotate (g,p2) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
p3 is Element of z
p3 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p3 .. (Rotate (g,p2)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(p3 .. g) - (p2 .. g) is ext-real V39() V43() set
((p3 .. g) - (p2 .. g)) + 1 is ext-real V39() V43() set
g :- p2 is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
g -: p2 is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
(g -: p2) /^ 1 is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
(g :- p2) ^ ((g -: p2) /^ 1) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
rng (g :- p2) is set
p3 .. (g :- p2) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is non empty set
g is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
rng g is set
p2 is Element of z
p2 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
Rotate (g,p2) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
p3 is Element of z
p3 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p3 .. (Rotate (g,p2)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
j is Element of z
j .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
j .. (Rotate (g,p2)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(j .. g) - (p2 .. g) is ext-real V39() V43() set
(p3 .. g) - (p2 .. g) is ext-real V39() V43() set
((p3 .. g) - (p2 .. g)) + 1 is ext-real V39() V43() set
((j .. g) - (p2 .. g)) + 1 is ext-real V39() V43() set
z is non empty set
g is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
rng g is set
p2 is Element of z
p2 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
Rotate (g,p2) is V1() V4( NAT ) V5(z) Function-like FinSequence-like FinSequence of z
p3 is Element of z
p3 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p3 .. (Rotate (g,p2)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
j is Element of z
j .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
j .. (Rotate (g,p2)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is non empty set
g is V1() V4( NAT ) V5(z) Function-like FinSequence-like circular FinSequence of z
rng g is set
len g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is Element of z
p2 .. g is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
g /. (len g) is Element of z
g /. 1 is Element of z
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
z /^ 1 is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
g is set
K49((z /^ 1)) is set
p2 is set
(z /^ 1) . g is set
(z /^ 1) . p2 is set
dom (z /^ 1) is Element of K27(NAT)
p3 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p3 + 1 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
dom z is V19() Element of K27(NAT)
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
j is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
j + 1 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. (p3 + 1) is Element of the U1 of (TOP-REAL 2)
(z /^ 1) /. p3 is Element of the U1 of (TOP-REAL 2)
(z /^ 1) . j is set
(z /^ 1) /. j is Element of the U1 of (TOP-REAL 2)
z /. (j + 1) is Element of the U1 of (TOP-REAL 2)
z /. (j + 1) is Element of the U1 of (TOP-REAL 2)
(z /^ 1) /. j is Element of the U1 of (TOP-REAL 2)
(z /^ 1) . p3 is set
(z /^ 1) /. p3 is Element of the U1 of (TOP-REAL 2)
z /. (p3 + 1) is Element of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
rng z is V19() set
z /. 1 is Element of the U1 of (TOP-REAL 2)
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(len z) + 1 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
g is Element of the U1 of (TOP-REAL 2)
g .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
Rotate (z,g) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
(z /. 1) .. (Rotate (z,g)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
((len z) + 1) - (g .. z) is ext-real V39() V43() set
1 + (len z) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(1 + (len z)) -' (g .. z) is V6() V7() V8() V12() ext-real non negative V39() V43() Element of NAT
(g .. z) - 1 is ext-real V39() V43() set
(1 + (len z)) - (g .. z) is ext-real V39() V43() set
((1 + (len z)) -' (g .. z)) + ((g .. z) - 1) is ext-real V39() V43() set
len (Rotate (z,g)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(g .. z) + 0 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. (g .. z) is Element of the U1 of (TOP-REAL 2)
(len z) - (g .. z) is ext-real V39() V43() set
1 + ((len z) - (g .. z)) is ext-real V39() V43() set
1 + 0 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
dom (Rotate (z,g)) is V19() Element of K27(NAT)
(Rotate (z,g)) /. ((1 + (len z)) -' (g .. z)) is Element of the U1 of (TOP-REAL 2)
(Rotate (z,g)) . ((1 + (len z)) -' (g .. z)) is set
p3 is set
(Rotate (z,g)) . p3 is set
j is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(Rotate (z,g)) /. j is Element of the U1 of (TOP-REAL 2)
j is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(Rotate (z,g)) /. j is Element of the U1 of (TOP-REAL 2)
j is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(Rotate (z,g)) <- (z /. 1) is set
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
rng z is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
g is Element of the U1 of (TOP-REAL 2)
g .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(len z) + (g .. z) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is Element of the U1 of (TOP-REAL 2)
p2 .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
Rotate (z,p2) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
g .. (Rotate (z,p2)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
((len z) + (g .. z)) - (p2 .. z) is ext-real V39() V43() set
z -: p2 is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
g .. (z -: p2) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (z -: p2) is set
z :- p2 is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
(z -: p2) /^ 1 is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
(z :- p2) ^ ((z -: p2) /^ 1) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
g .. ((z -: p2) /^ 1) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
1 + (g .. ((z -: p2) /^ 1)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
{p2} is non empty set
<*p2*> is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
rng <*p2*> is set
z /^ 1 is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like one-to-one FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
rng (z /^ 1) is set
(z /^ 1) -| p2 is V1() Function-like FinSequence-like set
((z /^ 1) -| p2) ^ <*p2*> is V1() Function-like FinSequence-like set
p2 .. (z /^ 1) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(z /^ 1) | (p2 .. (z /^ 1)) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
(z /^ 1) -: p2 is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
rng ((z /^ 1) -: p2) is set
rng ((z /^ 1) -| p2) is set
(rng ((z /^ 1) -| p2)) \/ (rng <*p2*>) is set
(z /^ 1) |-- p2 is V1() Function-like FinSequence-like set
rng ((z /^ 1) |-- p2) is set
(z /^ 1) :- p2 is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
<*p2*> ^ ((z /^ 1) |-- p2) is V1() Function-like FinSequence-like set
rng ((z /^ 1) :- p2) is set
(rng <*p2*>) \/ (rng ((z /^ 1) |-- p2)) is set
rng ((z -: p2) /^ 1) is set
rng (z :- p2) is set
(rng ((z -: p2) /^ 1)) \ (rng (z :- p2)) is Element of K27((rng ((z -: p2) /^ 1)))
K27((rng ((z -: p2) /^ 1))) is set
len (z :- p2) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(len (z :- p2)) + (g .. ((z -: p2) /^ 1)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(len z) - (p2 .. z) is ext-real V39() V43() set
((len z) - (p2 .. z)) + 1 is ext-real V39() V43() set
(g .. z) - 1 is ext-real V39() V43() set
(((len z) - (p2 .. z)) + 1) + ((g .. z) - 1) is ext-real V39() V43() set
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
rng z is V19() set
g is Element of the U1 of (TOP-REAL 2)
g .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is Element of the U1 of (TOP-REAL 2)
p2 .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
Rotate (z,p2) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
g .. (Rotate (z,p2)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p3 is Element of the U1 of (TOP-REAL 2)
p3 .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p3 .. (Rotate (z,p2)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,p2)) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(p3 .. z) + 1 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(len z) + (g .. z) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(p3 .. z) - (p2 .. z) is ext-real V39() V43() set
((p3 .. z) - (p2 .. z)) + 1 is ext-real V39() V43() set
((p3 .. z) + 1) - (p2 .. z) is ext-real V39() V43() set
((len z) + (g .. z)) - (p2 .. z) is ext-real V39() V43() set
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
rng z is V19() set
g is Element of the U1 of (TOP-REAL 2)
g .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is Element of the U1 of (TOP-REAL 2)
p2 .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p3 is Element of the U1 of (TOP-REAL 2)
p3 .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
Rotate (z,p3) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
p2 .. (Rotate (z,p3)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
g .. (Rotate (z,p3)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(len z) + (g .. z) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
((len z) + (g .. z)) - (p3 .. z) is ext-real V39() V43() set
(len z) + (p2 .. z) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
((len z) + (p2 .. z)) - (p3 .. z) is ext-real V39() V43() set
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
rng z is V19() set
g is Element of the U1 of (TOP-REAL 2)
g .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is Element of the U1 of (TOP-REAL 2)
p2 .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p3 is Element of the U1 of (TOP-REAL 2)
p3 .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
Rotate (z,p3) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
g .. (Rotate (z,p3)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 .. (Rotate (z,p3)) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng z is V19() set
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng z is V19() set
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng z is V19() set
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng z is V19() set
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng z is V19() set
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng z is V19() set
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng z is V19() set
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng z is V19() set
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng z is V19() set
dom z is V19() Element of K27(NAT)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(N-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
rng (Rotate (z,(N-min (L~ z)))) is V19() set
W-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
N-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(N-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(N-min (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
N-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(N-min (L~ z)))) is V19() set
(N-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
E-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(N-min (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
E-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(N-min (L~ z)))) is V19() set
(E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
S-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(N-min (L~ z)))) is V19() set
S-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng z is V19() set
(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng z is V19() set
dom z is V19() Element of K27(NAT)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
S-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(N-min (L~ z)))) is V19() set
(S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(N-min (L~ z)))),(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
Rotate (z,(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(W-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(W-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(W-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(W-min (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(W-min (L~ z)))),(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(W-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(W-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(W-min (L~ z)))),(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
W-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(W-min (L~ z)))) is V19() set
(W-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(W-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(W-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
N-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(W-min (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(W-min (L~ z)))),(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(W-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(W-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(W-min (L~ z)))),(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
N-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(W-min (L~ z)))) is V19() set
(N-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(W-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(W-min (L~ z)))),(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
E-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(W-min (L~ z)))) is V19() set
E-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng z is V19() set
(Rotate (z,(W-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(E-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng z is V19() set
dom z is V19() Element of K27(NAT)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
E-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(N-min (L~ z)))) is V19() set
(E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(N-min (L~ z)))),(E-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(N-min (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(N-min (L~ z)))),(E-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(S-max (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(S-max (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
E-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(S-max (L~ z)))),(E-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
S-min (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(S-max (L~ z)))) is V19() set
(S-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(S-max (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(S-max (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
W-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(S-max (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(S-max (L~ z)))),(E-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(S-max (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(S-max (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
E-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(S-max (L~ z)))),(E-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
W-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(S-max (L~ z)))) is V19() set
(W-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(S-max (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(S-max (L~ z)))),(E-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
N-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(S-max (L~ z)))) is V19() set
N-min (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng z is V19() set
(Rotate (z,(S-max (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
E-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(N-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(E-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng z is V19() set
dom z is V19() Element of K27(NAT)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(W-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(W-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
N-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(W-min (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(W-min (L~ z)))),(N-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(W-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(W-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(W-min (L~ z)))) is V19() set
E-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(W-min (L~ z)))),(N-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
(S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
S-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(N-min (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(N-min (L~ z)))),(N-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
S-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(N-min (L~ z)))),(N-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(N-min (L~ z)))) is V19() set
(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(S-max (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(S-max (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
W-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(S-max (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(S-max (L~ z)))),(N-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(S-max (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(S-max (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
N-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(S-max (L~ z)))),(N-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
rng (Rotate (z,(S-max (L~ z)))) is V19() set
W-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng z is V19() set
dom z is V19() Element of K27(NAT)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
E-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(N-min (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(N-min (L~ z)))),(E-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(N-min (L~ z)))) is V19() set
S-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(N-min (L~ z)))),(E-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(E-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(E-max (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(E-max (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
E-max (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
W-max (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-min (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(E-max (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(E-max (L~ z)))),(E-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(E-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(E-max (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(E-max (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
E-max (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
W-max (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-min (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(E-max (L~ z)))),(E-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(E-max (L~ z)))) is V19() set
(N-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(W-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(W-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
N-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(W-min (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(W-min (L~ z)))),(E-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(W-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(W-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
E-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(W-min (L~ z)))),(E-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
rng (Rotate (z,(W-min (L~ z)))) is V19() set
N-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng z is V19() set
dom z is V19() Element of K27(NAT)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(E-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(E-max (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(E-max (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
E-max (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
S-min (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-max (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(E-max (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(E-max (L~ z)))),(S-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(E-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(E-max (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(E-max (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
E-max (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(E-max (L~ z)))) is V19() set
W-max (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-min (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(E-max (L~ z)))),(S-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
(N-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(S-max (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(S-max (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
N-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-min (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(S-max (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(S-max (L~ z)))),(S-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(S-max (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(S-max (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
N-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-min (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(S-max (L~ z)))),(S-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
E-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(S-max (L~ z)))) is V19() set
(E-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
E-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(N-min (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(N-min (L~ z)))),(S-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(N-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(N-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(N-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
S-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(N-min (L~ z)))),(S-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
rng (Rotate (z,(N-min (L~ z)))) is V19() set
E-min (L~ (Rotate (z,(N-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(W-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng z is V19() set
dom z is V19() Element of K27(NAT)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(S-max (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(S-max (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
W-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-min (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
N-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(S-max (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(S-max (L~ z)))),(W-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
N-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(N-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(S-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(S-max (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(S-max (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
E-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(S-max (L~ z)))) is V19() set
N-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-max (L~ (Rotate (z,(S-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(S-max (L~ z)))),(W-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
(E-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(W-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(W-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
E-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(W-min (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(W-min (L~ z)))),(W-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
E-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(E-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(W-min (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(W-min (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(W-min (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
W-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
E-min (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(W-min (L~ z)))),(W-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
S-max (L~ (Rotate (z,(W-min (L~ z))))) is Element of the U1 of (TOP-REAL 2)
rng (Rotate (z,(W-min (L~ z)))) is V19() set
(S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ z) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(E-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(E-max (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(E-max (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
E-max (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
S-min (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
S-max (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-max (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-max (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
rng (Rotate (z,(E-max (L~ z)))) is V19() set
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(E-max (L~ z)))),(W-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
z /. 1 is Element of the U1 of (TOP-REAL 2)
L~ z is Element of K27( the U1 of (TOP-REAL 2))
W-max (L~ z) is Element of the U1 of (TOP-REAL 2)
W-min (L~ z) is Element of the U1 of (TOP-REAL 2)
S-min (L~ z) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
(S-min (L~ z)) .. z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
E-max (L~ z) is Element of the U1 of (TOP-REAL 2)
Rotate (z,(E-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (z,(E-max (L~ z)))) is Element of K27( the U1 of (TOP-REAL 2))
rng z is V19() set
(Rotate (z,(E-max (L~ z)))) /. 1 is Element of the U1 of (TOP-REAL 2)
E-max (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
W-max (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-max (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
W-min (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(W-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
len z is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
p2 is V6() V7() V8() V12() ext-real V39() V43() Element of NAT
z /. p2 is Element of the U1 of (TOP-REAL 2)
Rotate ((Rotate (z,(E-max (L~ z)))),(W-max (L~ z))) is V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) Function-like non constant non empty V19() FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)
rng (Rotate (z,(E-max (L~ z)))) is V19() set
S-min (L~ (Rotate (z,(E-max (L~ z))))) is Element of the U1 of (TOP-REAL 2)
(S-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) is V6() V7() V8() V12() ext-real V39() V43() Element of NAT