:: Rotating and reversing.(Finite sequences)
:: by Andrzej Trybulec
::
:: Received January 21, 1999
:: Copyright (c) 1999-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, SUBSET_1, XBOOLE_0, FINSEQ_1, FUNCT_1, RELAT_1, PARTFUN1, FINSEQ_4, ARYTM_3, FINSEQ_5, RFINSEQ, ORDINAL4, XXREAL_0, ARYTM_1, FINSEQ_6, CARD_1, NAT_1, ZFMISC_1, EUCLID, JORDAN2C, FINSEQ_2, SUPINF_2, TARSKI, GOBOARD1, MCART_1, PRE_TOPC, TOPREAL1, RLTOPSP1, GOBOARD2, GOBOARD5, MATRIX_1, COMPLEX1, GOBOARD9, CONNSP_1, TOPS_1, PSCOMP_1, SPRECT_2, TREES_1, JORDAN5D, RCOMP_1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, COMPLEX1, NAT_D, CARD_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, MATRIX_0, MATRIX_1, FINSEQ_4, RFINSEQ, FINSEQ_5, FINSEQ_6, ZFMISC_1, DOMAIN_1, SEQ_4, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_1, COMPTS_1, EUCLID, RLTOPSP1, TOPREAL1, GOBOARD1, GOBOARD2, GOBOARD5, GOBOARD9, PSCOMP_1, JORDAN5D, SPRECT_2;
definitions TOPREAL1, GOBOARD5, SPRECT_2, TARSKI, FINSEQ_6, GOBOARD1, XBOOLE_0, STRUCT_0, SEQM_3;
theorems FINSEQ_6, NAT_1, FINSEQ_5, FINSEQ_3, FINSEQ_4, NAT_2, FINSEQ_1, SPRECT_3, RFINSEQ, TOPREAL1, GOBOARD5, SPPOL_2, TARSKI, SPRECT_2, GOBOARD9, INT_1, SUBSET_1, JGRAPH_1, GOBOARD7, GOBOARD1, GOBOARD2, FUNCT_1, PARTFUN2, RELAT_1, FINSEQ_2, JORDAN5D, PSCOMP_1, EUCLID, TOPREAL3, XBOOLE_0, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1, NAT_D, SEQM_3, SEQ_4, MATRIX_0;
schemes ;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, FINSEQ_5, FINSEQ_6, STRUCT_0, GOBOARD2, GOBOARD9, SPRECT_1, SPRECT_2, CARD_1, COMPTS_1, EUCLID, ORDINAL1;
constructors HIDDEN, FINSEQOP, FINSEQ_4, RFINSEQ, NAT_D, TOPS_1, CONNSP_1, COMPTS_1, REALSET2, GOBOARD2, PSCOMP_1, GOBOARD9, SPRECT_2, JORDAN5D, REAL_1, GOBOARD1, RELSET_1, SEQ_4, RVSUM_1, MATRIX_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities TOPREAL1;
expansions TARSKI, GOBOARD1, XBOOLE_0, SEQM_3;


definition
let D be non empty set ;
let f be FinSequence of D;
:: original: constant
redefine attr f is constant means :Def1: :: REVROT_1:def 1
 for n, m being Nat st n in dom f & m in dom f holds
f /. n = f /. m;
compatibility
( f is constant iff for n, m being Nat st n in dom f & m in dom f holds
f /. n = f /. m )
proof end;
end;

:: deftheorem Def1 defines constant REVROT_1:def 1 :
for D being non empty set
for f being FinSequence of D holds
( f is constant iff for n, m being Nat st n in dom f & m in dom f holds
f /. n = f /. m );

theorem Th1: :: REVROT_1:1
for D being non empty set
for f being FinSequence of D st f just_once_values f /. (len f) holds
(f /. (len f)) .. f = len f
proof end;

theorem :: REVROT_1:2
for D being non empty set
for f being FinSequence of D holds f /^ (len f) = {} by RFINSEQ:27;

theorem Th3: :: REVROT_1:3
for D being non empty set
for f being non empty FinSequence of D holds f /. (len f) in rng f
proof end;

definition
let D be non empty set ;
let f be FinSequence of D;
let y be set ;
:: original: just_once_values
redefine pred f just_once_values y means :: REVROT_1:def 2
 ex x being set st
( x in dom f & y = f /. x & ( for z being set st z in dom f & z <> x holds
f /. z <> y ) );
compatibility
( f just_once_values y iff ex x being set st
( x in dom f & y = f /. x & ( for z being set st z in dom f & z <> x holds
f /. z <> y ) ) )
proof end;
end;

:: deftheorem defines just_once_values REVROT_1:def 2 :
for D being non empty set
for f being FinSequence of D
for y being set holds
( f just_once_values y iff ex x being set st
( x in dom f & y = f /. x & ( for z being set st z in dom f & z <> x holds
f /. z <> y ) ) );

theorem Th4: :: REVROT_1:4
for D being non empty set
for f being FinSequence of D st f just_once_values f /. (len f) holds
f -: (f /. (len f)) = f
proof end;

theorem Th5: :: REVROT_1:5
for D being non empty set
for f being FinSequence of D st f just_once_values f /. (len f) holds
f :- (f /. (len f)) = <*(f /. (len f))*>
proof end;

theorem Th6: :: REVROT_1:6
for D being non empty set
for p being Element of D
for f being FinSequence of D holds 1 <= len (f :- p)
proof end;

theorem :: REVROT_1:7
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
len (f :- p) <= len f
proof end;

theorem :: REVROT_1:8
for D being non empty set
for f being non empty circular FinSequence of D holds Rev f is circular
proof end;

theorem Th9: :: REVROT_1:9
for i being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & 1 <= i & i <= len (f :- p) holds
(Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f))
proof end;

theorem Th10: :: REVROT_1:10
for i being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & p .. f <= i & i <= len f holds
f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f))
proof end;

theorem Th11: :: REVROT_1:11
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
(Rotate (f,p)) /. (len (f :- p)) = f /. (len f)
proof end;

theorem Th12: :: REVROT_1:12
for i being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & len (f :- p) < i & i <= len f holds
(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))
proof end;

theorem :: REVROT_1:13
for i being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & 1 < i & i <= p .. f holds
f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f))
proof end;

theorem Th14: :: REVROT_1:14
for D being non empty set
for p being Element of D
for f being FinSequence of D holds len (Rotate (f,p)) = len f
proof end;

theorem Th15: :: REVROT_1:15
for D being non empty set
for p being Element of D
for f being FinSequence of D holds dom (Rotate (f,p)) = dom f
proof end;

theorem Th16: :: REVROT_1:16
for D being non empty set
for f being circular FinSequence of D
for p being Element of D st ( for i being Nat st 1 < i & i < len f holds
f /. i <> f /. 1 ) holds
Rotate ((Rotate (f,p)),(f /. 1)) = f
proof end;

theorem Th17: :: REVROT_1:17
for i being Nat
for D being non empty set
for p being Element of D
for f being circular FinSequence of D st p in rng f & len (f :- p) <= i & i <= len f holds
(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))
proof end;

theorem Th18: :: REVROT_1:18
for i being Nat
for D being non empty set
for p being Element of D
for f being circular FinSequence of D st p in rng f & 1 <= i & i <= p .. f holds
f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f))
proof end;

registration
let D be non trivial set ;
cluster V1() V4( NAT ) V5(D) Function-like V8() V33() FinSequence-like FinSubsequence-like circular for FinSequence of D;
existence
ex b1 being FinSequence of D st
( b1 is V8() & b1 is circular )
proof end;
end;

registration
let D be non trivial set ;
let p be Element of D;
let f be V8() circular FinSequence of D;
cluster Rotate (f,p) -> V8() ;
coherence
not Rotate (f,p) is constant
proof end;
end;

theorem Th19: :: REVROT_1:19
for n being non zero Nat holds 0.REAL n <> 1.REAL n
proof end;

registration
let n be non zero Nat;
cluster TOP-REAL n -> non trivial ;
coherence
not TOP-REAL n is trivial
proof end;
end;

theorem Th20: :: REVROT_1:20
for f, g being FinSequence of (TOP-REAL 2) st rng f c= rng g holds
rng (X_axis f) c= rng (X_axis g)
proof end;

theorem Th21: :: REVROT_1:21
for f, g being FinSequence of (TOP-REAL 2) st rng f = rng g holds
rng (X_axis f) = rng (X_axis g) by Th20;

theorem Th22: :: REVROT_1:22
for f, g being FinSequence of (TOP-REAL 2) st rng f c= rng g holds
rng (Y_axis f) c= rng (Y_axis g)
proof end;

theorem Th23: :: REVROT_1:23
for f, g being FinSequence of (TOP-REAL 2) st rng f = rng g holds
rng (Y_axis f) = rng (Y_axis g) by Th22;

registration
let p be Point of (TOP-REAL 2);
let f be circular special FinSequence of (TOP-REAL 2);
cluster Rotate (f,p) -> special ;
coherence
Rotate (f,p) is special
proof end;
end;

theorem Th24: :: REVROT_1:24
for i being Nat
for p being Point of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2) st p in rng f & 1 <= i & i < len (f :- p) holds
LSeg ((Rotate (f,p)),i) = LSeg (f,((i -' 1) + (p .. f)))
proof end;

theorem Th25: :: REVROT_1:25
for i being Nat
for p being Point of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2) st p in rng f & p .. f <= i & i < len f holds
LSeg (f,i) = LSeg ((Rotate (f,p)),((i -' (p .. f)) + 1))
proof end;

theorem Th26: :: REVROT_1:26
for p being Point of (TOP-REAL 2)
for f being circular FinSequence of (TOP-REAL 2) holds Incr (X_axis f) = Incr (X_axis (Rotate (f,p)))
proof end;

theorem Th27: :: REVROT_1:27
for p being Point of (TOP-REAL 2)
for f being circular FinSequence of (TOP-REAL 2) holds Incr (Y_axis f) = Incr (Y_axis (Rotate (f,p)))
proof end;

theorem Th28: :: REVROT_1:28
for p being Point of (TOP-REAL 2)
for f being non empty circular FinSequence of (TOP-REAL 2) holds GoB (Rotate (f,p)) = GoB f
proof end;

theorem Th29: :: REVROT_1:29
for p being Point of (TOP-REAL 2)
for f being V8() standard special_circular_sequence holds Rev (Rotate (f,p)) = Rotate ((Rev f),p)
proof end;

theorem Th30: :: REVROT_1:30
for f being circular s.c.c. FinSequence of (TOP-REAL 2) st len f > 4 holds
(LSeg (f,((len f) -' 1))) /\ (LSeg (f,1)) = {(f /. 1)}
proof end;

theorem Th31: :: REVROT_1:31
for i being Nat
for p being Point of (TOP-REAL 2)
for f being circular FinSequence of (TOP-REAL 2) st p in rng f & len (f :- p) <= i & i < len f holds
LSeg ((Rotate (f,p)),i) = LSeg (f,((i + (p .. f)) -' (len f)))
proof end;

registration
let p be Point of (TOP-REAL 2);
let f be circular s.c.c. FinSequence of (TOP-REAL 2);
cluster Rotate (f,p) -> s.c.c. ;
coherence
Rotate (f,p) is s.c.c.
proof end;
end;

registration
let p be Point of (TOP-REAL 2);
let f be V8() standard special_circular_sequence;
cluster Rotate (f,p) -> unfolded ;
coherence
Rotate (f,p) is unfolded
proof end;
end;

theorem Th32: :: REVROT_1:32
for i being Nat
for p being Point of (TOP-REAL 2)
for f being circular FinSequence of (TOP-REAL 2) st p in rng f & 1 <= i & i < p .. f holds
LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f)))
proof end;

theorem Th33: :: REVROT_1:33
for p being Point of (TOP-REAL 2)
for f being circular FinSequence of (TOP-REAL 2) holds L~ (Rotate (f,p)) = L~ f
proof end;

theorem Th34: :: REVROT_1:34
for p being Point of (TOP-REAL 2)
for f being circular FinSequence of (TOP-REAL 2)
for G being Go-board holds
( f is_sequence_on G iff Rotate (f,p) is_sequence_on G )
proof end;

registration
let p be Point of (TOP-REAL 2);
let f be non empty circular standard FinSequence of (TOP-REAL 2);
cluster Rotate (f,p) -> standard ;
coherence
Rotate (f,p) is standard
proof end;
end;

theorem Th35: :: REVROT_1:35
for f being V8() standard special_circular_sequence
for p being Point of (TOP-REAL 2)
for k being Nat st p in rng f & 1 <= k & k < p .. f holds
left_cell (f,k) = left_cell ((Rotate (f,p)),((k + (len f)) -' (p .. f)))
proof end;

theorem Th36: :: REVROT_1:36
for p being Point of (TOP-REAL 2)
for f being V8() standard special_circular_sequence holds LeftComp (Rotate (f,p)) = LeftComp f
proof end;

theorem :: REVROT_1:37
for p being Point of (TOP-REAL 2)
for f being V8() standard special_circular_sequence holds RightComp (Rotate (f,p)) = RightComp f
proof end;

Lm1: for f being V8() standard special_circular_sequence holds
( not f /. 1 = N-min (L~ f) or f is clockwise_oriented or Rev f is clockwise_oriented )
proof end;

registration
let p be Point of (TOP-REAL 2);
let f be V8() standard clockwise_oriented special_circular_sequence;
cluster Rotate (f,p) -> clockwise_oriented ;
coherence
Rotate (f,p) is clockwise_oriented
proof end;
end;

theorem :: REVROT_1:38
for f being V8() standard special_circular_sequence holds
( f is clockwise_oriented or Rev f is clockwise_oriented )
proof end;