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