reconsider ff = Rev f as non empty FinSequence of (TOP-REAL 2) ;
A1:
Rev ff = f
by FINSEQ_6:29;
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 11 for b1 being Element of NAT holds
( not b1 in dom ff or not b1 + 1 in dom ff or for b2, b3, b4, b5 being Element of NAT 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 K63((abs K67(b2,b4)),(abs K67(b3,b5))) = 1 ) )
let k be
Element of
NAT ;
( k in dom ff implies ex i, j being Element of NAT st
( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * i,j ) )assume A6:
k in dom ff
;
ex i, j being Element of 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:27;
len f < (len f) + 1
by NAT_1:13;
then A8:
(((len f) + 1) -' k) + k = (len f) + 1
by A7, XREAL_1:237, XXREAL_0:2;
then
((len f) + 1) -' k in dom f
by A1, A4, A6, FINSEQ_5:62;
then consider i,
j being
Element of
NAT such that A9:
[i,j] in Indices (GoB f)
and A10:
f /. (((len f) + 1) -' k) = (GoB f) * i,
j
by A3, GOBOARD1:def 11;
take i =
i;
ex j being Element of 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,jthus
ff /. k = (GoB ff) * i,
j
by A1, A2, A4, A6, A8, A10, FINSEQ_5:69;
verum
end;
let k be
Element of
NAT ;
( not k in dom ff or not k + 1 in dom ff or for b1, b2, b3, b4 being Element of NAT 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 K63((abs K67(b1,b3)),(abs K67(b2,b4))) = 1 ) )
assume that A11:
k in dom ff
and A12:
k + 1
in dom ff
;
for b1, b2, b3, b4 being Element of NAT 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 K63((abs K67(b1,b3)),(abs K67(b2,b4))) = 1 )
set l =
((len f) + 1) -' (k + 1);
k <= len f
by A4, A11, FINSEQ_3:27;
then
k + 1
<= (len f) + 1
by XREAL_1:8;
then A13:
(((len f) + 1) -' (k + 1)) + (k + 1) = (len f) + 1
by XREAL_1:237;
then A14:
((len f) + 1) -' (k + 1) in dom f
by A1, A4, A12, FINSEQ_5:62;
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:62;
let i1,
j1,
i2,
j2 be
Element of
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 K63((abs K67(i1,i2)),(abs K67(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
;
K63((abs K67(i1,i2)),(abs K67(j1,j2))) = 1
A21:
abs (i2 - i1) =
abs (- (i1 - i2))
.=
abs (i1 - i2)
by COMPLEX1:138
;
A22:
abs (j2 - j1) =
abs (- (j1 - j2))
.=
abs (j1 - j2)
by COMPLEX1:138
;
A23:
f /. (((len f) + 1) -' (k + 1)) = (GoB f) * i2,
j2
by A1, A2, A4, A12, A13, A20, FINSEQ_5:69;
f /. ((((len f) + 1) -' (k + 1)) + 1) = (GoB f) * i1,
j1
by A1, A2, A4, A11, A15, A19, FINSEQ_5:69;
hence
(abs (i1 - i2)) + (abs (j1 - j2)) = 1
by A2, A3, A14, A16, A17, A18, A21, A22, A23, GOBOARD1:def 11;
verum
end;
A24: ff /. 1 =
f /. (len f)
by FINSEQ_5:68
.=
f /. 1
by FINSEQ_6:def 1
.=
ff /. (len ff)
by A4, FINSEQ_5:68
;
ff is s.c.c.
proof
let i be
Element of
NAT ;
GOBOARD5:def 4 for b1 being Element of NAT 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
Element of
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:237;
i < j
by A25, NAT_1:13;
then A29:
((len f) -' i) + i = len f
by A27, XREAL_1:237, 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:8;
then A30:
((len f) -' j) + 1
< (len f) -' i
by XREAL_1:8;
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,jthen
((len f) -' i) + 1
< len f
by A26, A29, FINSEQ_5:def 3, XREAL_1:8;
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)) = {}
by XBOOLE_0:def 7;
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,jA35:
(len f) -' j > 1
by A28, A34, XREAL_1:8;
((len f) -' i) + 1
<= len f
by A29, A33, XREAL_1:8;
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)) = {}
by XBOOLE_0:def 7;
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:29, SPPOL_2:42; verum