reconsider ff = Rev f as non empty FinSequence of (TOP-REAL 2) ;
A1:
Rev ff = f
;
A2:
GoB ff = GoB f
by Lm1;
A3:
f is_sequence_on GoB f
by GOBOARD5:def 5;
A4:
len f = len ff
by FINSEQ_5:def 3;
A5:
ff is standard
proof
hereby GOBOARD5:def 5,
GOBOARD1:def 9 for b1 being set holds
( not b1 in dom ff or not b1 + 1 in dom ff or for b2, b3, b4, b5 being set holds
( not [b2,b3] in Indices (GoB ff) or not [b4,b5] in Indices (GoB ff) or not ff /. b1 = (GoB ff) * (b2,b3) or not ff /. (b1 + 1) = (GoB ff) * (b4,b5) or |.(b2 - b4).| + |.(b3 - b5).| = 1 ) )
let k be
Nat;
( k in dom ff implies ex i, j being Nat st
( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) ) )assume A6:
k in dom ff
;
ex i, j being Nat st
( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) )set l =
((len f) + 1) -' k;
A7:
k <= len f
by A4, A6, FINSEQ_3:25;
len f < (len f) + 1
by NAT_1:13;
then A8:
(((len f) + 1) -' k) + k = (len f) + 1
by A7, XREAL_1:235, XXREAL_0:2;
then
((len f) + 1) -' k in dom f
by A1, A4, A6, FINSEQ_5:59;
then consider i,
j being
Nat such that A9:
[i,j] in Indices (GoB f)
and A10:
f /. (((len f) + 1) -' k) = (GoB f) * (
i,
j)
by A3;
take i =
i;
ex j being Nat st
( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) )take j =
j;
( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) )thus
[i,j] in Indices (GoB ff)
by A9, Lm1;
ff /. k = (GoB ff) * (i,j)thus
ff /. k = (GoB ff) * (
i,
j)
by A1, A2, A4, A6, A8, A10, FINSEQ_5:66;
verum
end;
let k be
Nat;
( not k in dom ff or not k + 1 in dom ff or for b1, b2, b3, b4 being set holds
( not [b1,b2] in Indices (GoB ff) or not [b3,b4] in Indices (GoB ff) or not ff /. k = (GoB ff) * (b1,b2) or not ff /. (k + 1) = (GoB ff) * (b3,b4) or |.(b1 - b3).| + |.(b2 - b4).| = 1 ) )
assume that A11:
k in dom ff
and A12:
k + 1
in dom ff
;
for b1, b2, b3, b4 being set holds
( not [b1,b2] in Indices (GoB ff) or not [b3,b4] in Indices (GoB ff) or not ff /. k = (GoB ff) * (b1,b2) or not ff /. (k + 1) = (GoB ff) * (b3,b4) or |.(b1 - b3).| + |.(b2 - b4).| = 1 )
set l =
((len f) + 1) -' (k + 1);
k <= len f
by A4, A11, FINSEQ_3:25;
then
k + 1
<= (len f) + 1
by XREAL_1:6;
then A13:
(((len f) + 1) -' (k + 1)) + (k + 1) = (len f) + 1
by XREAL_1:235;
then A14:
((len f) + 1) -' (k + 1) in dom f
by A1, A4, A12, FINSEQ_5:59;
A15:
((((len f) + 1) -' (k + 1)) + 1) + k = (len f) + 1
by A13;
then A16:
(((len f) + 1) -' (k + 1)) + 1
in dom f
by A1, A4, A11, FINSEQ_5:59;
let i1,
j1,
i2,
j2 be
Nat;
( not [i1,j1] in Indices (GoB ff) or not [i2,j2] in Indices (GoB ff) or not ff /. k = (GoB ff) * (i1,j1) or not ff /. (k + 1) = (GoB ff) * (i2,j2) or |.(i1 - i2).| + |.(j1 - j2).| = 1 )
assume that A17:
[i1,j1] in Indices (GoB ff)
and A18:
[i2,j2] in Indices (GoB ff)
and A19:
ff /. k = (GoB ff) * (
i1,
j1)
and A20:
ff /. (k + 1) = (GoB ff) * (
i2,
j2)
;
|.(i1 - i2).| + |.(j1 - j2).| = 1
A21:
|.(i2 - i1).| =
|.(- (i1 - i2)).|
.=
|.(i1 - i2).|
by COMPLEX1:52
;
A22:
|.(j2 - j1).| =
|.(- (j1 - j2)).|
.=
|.(j1 - j2).|
by COMPLEX1:52
;
A23:
f /. (((len f) + 1) -' (k + 1)) = (GoB f) * (
i2,
j2)
by A1, A2, A4, A12, A13, A20, FINSEQ_5:66;
f /. ((((len f) + 1) -' (k + 1)) + 1) = (GoB f) * (
i1,
j1)
by A1, A2, A4, A11, A15, A19, FINSEQ_5:66;
hence
|.(i1 - i2).| + |.(j1 - j2).| = 1
by A2, A3, A14, A16, A17, A18, A21, A22, A23;
verum
end;
A24: ff /. 1 =
f /. (len f)
by FINSEQ_5:65
.=
f /. 1
by FINSEQ_6:def 1
.=
ff /. (len ff)
by A4, FINSEQ_5:65
;
ff is s.c.c.
proof
let i be
Nat;
GOBOARD5:def 4 for b1 being set holds
( b1 <= i + 1 or ( ( i <= 1 or len ff <= b1 ) & len ff <= b1 + 1 ) or LSeg (ff,i) misses LSeg (ff,b1) )let j be
Nat;
( j <= i + 1 or ( ( i <= 1 or len ff <= j ) & len ff <= j + 1 ) or LSeg (ff,i) misses LSeg (ff,j) )
assume that A25:
i + 1
< j
and A26:
( (
i > 1 &
j < len ff ) or
j + 1
< len ff )
;
LSeg (ff,i) misses LSeg (ff,j)
set k =
(len f) -' i;
set l =
(len f) -' j;
A27:
j <= len f
by A4, A26, NAT_1:13;
then A28:
((len f) -' j) + j = len f
by XREAL_1:235;
i < j
by A25, NAT_1:13;
then A29:
((len f) -' i) + i = len f
by A27, XREAL_1:235, XXREAL_0:2;
then
(i + 1) + ((len f) -' i) = (((len f) -' j) + 1) + j
by A28;
then
(((len f) -' j) + 1) + j < j + ((len f) -' i)
by A25, XREAL_1:6;
then A30:
((len f) -' j) + 1
< (len f) -' i
by XREAL_1:6;
A31:
j + 1
<= len f
by A4, A26, NAT_1:13;
per cases
( j + 1 = len f or ( i >= 1 & j + 1 < len f ) or i = 0 )
by A31, NAT_1:14, XXREAL_0:1;
suppose
j + 1
= len f
;
LSeg (ff,i) misses LSeg (ff,j)then
((len f) -' i) + 1
< len f
by A26, A29, FINSEQ_5:def 3, XREAL_1:6;
then
LSeg (
f,
((len f) -' i))
misses LSeg (
f,
((len f) -' j))
by A30, GOBOARD5:def 4;
then A32:
(LSeg (f,((len f) -' i))) /\ (LSeg (f,((len f) -' j))) = {}
;
LSeg (
f,
((len f) -' i))
= LSeg (
ff,
i)
by A29, SPPOL_2:2;
hence
(LSeg (ff,i)) /\ (LSeg (ff,j)) = {}
by A28, A32, SPPOL_2:2;
XBOOLE_0:def 7 verum end; suppose that A33:
i >= 1
and A34:
j + 1
< len f
;
LSeg (ff,i) misses LSeg (ff,j)A35:
(len f) -' j > 1
by A28, A34, XREAL_1:6;
((len f) -' i) + 1
<= len f
by A29, A33, XREAL_1:6;
then
(len f) -' i < len f
by NAT_1:13;
then
LSeg (
f,
((len f) -' i))
misses LSeg (
f,
((len f) -' j))
by A30, A35, GOBOARD5:def 4;
then A36:
(LSeg (f,((len f) -' i))) /\ (LSeg (f,((len f) -' j))) = {}
;
LSeg (
f,
((len f) -' i))
= LSeg (
ff,
i)
by A29, SPPOL_2:2;
hence
(LSeg (ff,i)) /\ (LSeg (ff,j)) = {}
by A28, A36, SPPOL_2:2;
XBOOLE_0:def 7 verum end;
end;
hence
Rev f is standard special_circular_sequence
by A5, A24, FINSEQ_6:def 1, SPPOL_2:28, SPPOL_2:40; verum