let f be V8() standard special_circular_sequence; ( not f /. 1 = N-min (L~ f) or f is clockwise_oriented or Rev f is clockwise_oriented )
assume A1:
f /. 1 = N-min (L~ f)
; ( f is clockwise_oriented or Rev f is clockwise_oriented )
(1 + 1) + 1 < len f
by GOBOARD7:34, XXREAL_0:2;
then A2:
2 < (len f) -' 1
by NAT_D:52;
A3:
[(i_w_n f),(width (GoB f))] in Indices (GoB f)
by JORDAN5D:def 7;
then A4:
i_w_n f <= len (GoB f)
by MATRIX_0:32;
A5:
1 <= width (GoB f)
by A3, MATRIX_0:32;
A6:
(GoB f) * ((i_w_n f),(width (GoB f))) = N-min (L~ f)
by JORDAN5D:def 7;
A7:
len f > 1 + 1
by GOBOARD7:34, XXREAL_0:2;
then A8:
1 + 1 in dom f
by FINSEQ_3:25;
then consider i1, j1 being Nat such that
A9:
[i1,j1] in Indices (GoB f)
and
A10:
f /. 2 = (GoB f) * (i1,j1)
by GOBOARD5:11;
A11:
j1 <= width (GoB f)
by A9, MATRIX_0:32;
A12:
1 <= j1
by A9, MATRIX_0:32;
then A13:
1 <= width (GoB f)
by A11, XXREAL_0:2;
A14:
1 <= i1
by A9, MATRIX_0:32;
A15:
i1 <= len (GoB f)
by A9, MATRIX_0:32;
A16:
now ( width (GoB f) = j1 implies i_w_n f <= i1 )assume A17:
width (GoB f) = j1
;
i_w_n f <= i1then
((GoB f) * (1,j1)) `2 = N-bound (L~ f)
by JORDAN5D:40;
then
((GoB f) * (i1,j1)) `2 = N-bound (L~ f)
by A12, A11, A14, A15, GOBOARD5:1;
then
(GoB f) * (
i1,
j1)
in N-most (L~ f)
by A7, A8, A10, GOBOARD1:1, SPRECT_2:10;
then
(N-min (L~ f)) `1 <= ((GoB f) * (i1,j1)) `1
by PSCOMP_1:39;
hence
i_w_n f <= i1
by A6, A12, A4, A14, A17, GOBOARD5:3;
verum end;
A18:
len f > 1
by GOBOARD7:34, XXREAL_0:2;
then A19:
len f in dom f
by FINSEQ_3:25;
1 in dom f
by A18, FINSEQ_3:25;
then
|.((i_w_n f) - i1).| + |.((width (GoB f)) - j1).| = 1
by A1, A3, A6, A8, A9, A10, GOBOARD5:12;
then
( ( |.((i_w_n f) - i1).| = 1 & width (GoB f) = j1 ) or ( |.((width (GoB f)) - j1).| = 1 & i_w_n f = i1 ) )
by SEQM_3:42;
then A20:
( ( i1 = (i_w_n f) + 1 & width (GoB f) = j1 ) or ( width (GoB f) = j1 + 1 & i_w_n f = i1 ) )
by A11, A16, SEQM_3:41;
i_e_n f <= len (GoB f)
by JORDAN5D:45;
then
i_w_n f < len (GoB f)
by SPRECT_3:27, XXREAL_0:2;
then A21:
( 1 <= (i_w_n f) + 1 & (i_w_n f) + 1 <= len (GoB f) )
by NAT_1:11, NAT_1:13;
A22:
(len f) -' 1 <= len f
by NAT_D:44;
1 <= (len f) -' 1
by A7, NAT_D:55;
then A23:
(len f) -' 1 in dom f
by A22, FINSEQ_3:25;
then consider i2, j2 being Nat such that
A24:
[i2,j2] in Indices (GoB f)
and
A25:
f /. ((len f) -' 1) = (GoB f) * (i2,j2)
by GOBOARD5:11;
A26:
j2 <= width (GoB f)
by A24, MATRIX_0:32;
A27:
1 <= i2
by A24, MATRIX_0:32;
A28:
( 1 <= j2 & i2 <= len (GoB f) )
by A24, MATRIX_0:32;
A29:
now ( width (GoB f) = j2 implies i_w_n f <= i2 )assume A30:
width (GoB f) = j2
;
i_w_n f <= i2then
((GoB f) * (1,j2)) `2 = N-bound (L~ f)
by JORDAN5D:40;
then
((GoB f) * (i2,j2)) `2 = N-bound (L~ f)
by A26, A27, A28, GOBOARD5:1;
then
(GoB f) * (
i2,
j2)
in N-most (L~ f)
by A7, A23, A25, GOBOARD1:1, SPRECT_2:10;
then
(N-min (L~ f)) `1 <= ((GoB f) * (i2,j2)) `1
by PSCOMP_1:39;
hence
i_w_n f <= i2
by A6, A4, A27, A13, A30, GOBOARD5:3;
verum end;
A31:
len f > 4
by GOBOARD7:34;
then A32:
(GoB f) * (i2,j2) in L~ f
by A23, A25, GOBOARD1:1, XXREAL_0:2;
A33:
((len f) -' 1) + 1 = len f
by A31, XREAL_1:235, XXREAL_0:2;
then
f /. (((len f) -' 1) + 1) = f /. 1
by FINSEQ_6:def 1;
then
|.(i2 - (i_w_n f)).| + |.(j2 - (width (GoB f))).| = 1
by A1, A23, A3, A6, A24, A25, A19, A33, GOBOARD5:12;
then
( ( |.(i2 - (i_w_n f)).| = 1 & j2 = width (GoB f) ) or ( |.(j2 - (width (GoB f))).| = 1 & i2 = i_w_n f ) )
by SEQM_3:42;
then
( ( i2 = (i_w_n f) + 1 & j2 = width (GoB f) ) or ( j2 + 1 = width (GoB f) & i2 = i_w_n f ) )
by A26, A29, SEQM_3:41;
then
( (f /. 2) `2 = ((GoB f) * (1,(width (GoB f)))) `2 or (f /. ((len f) -' 1)) `2 = ((GoB f) * (1,(width (GoB f)))) `2 )
by A22, A10, A25, A5, A20, A21, A2, GOBOARD5:1, GOBOARD7:37;
then
( (f /. 2) `2 = N-bound (L~ f) or (f /. ((len f) -' 1)) `2 = N-bound (L~ f) )
by JORDAN5D:40;
then A34:
( f /. 2 in N-most (L~ f) or f /. ((len f) -' 1) in N-most (L~ f) )
by A7, A8, A25, A32, GOBOARD1:1, SPRECT_2:10;
reconsider A = L~ (Rev f) as non empty compact Subset of (TOP-REAL 2) ;
A35:
A = L~ f
by SPPOL_2:22;
((len f) -' 1) + (1 + 1) =
(((len f) -' 1) + 1) + 1
.=
(len f) + 1
by A31, XREAL_1:235, XXREAL_0:2
;
then A36:
(Rev f) /. 2 = f /. ((len f) -' 1)
by A23, FINSEQ_5:66;
(Rev f) /. 1 =
f /. (len f)
by FINSEQ_5:65
.=
N-min (L~ f)
by A1, FINSEQ_6:def 1
.=
N-min A
by SPPOL_2:22
;
hence
( f is clockwise_oriented or Rev f is clockwise_oriented )
by A1, A36, A35, A34, SPRECT_2:30; verum