let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st f is circular & f just_once_values p holds
Rev (Rotate (f,p)) = Rotate ((Rev f),p)
let p be Element of D; :: thesis: for f being FinSequence of D st f is circular & f just_once_values p holds
Rev (Rotate (f,p)) = Rotate ((Rev f),p)
let f be FinSequence of D; :: thesis: ( f is circular & f just_once_values p implies Rev (Rotate (f,p)) = Rotate ((Rev f),p) )
assume that
A1: f is circular and
A2: f just_once_values p ; :: thesis: Rev (Rotate (f,p)) = Rotate ((Rev f),p)
reconsider j = (len (f :- p)) - 1 as Element of NAT by INT_1:5, NAT_1:14;
A3: f /. 1 = f /. (len f) by A1;
A4: p in rng f by A2, FINSEQ_4:45;
then A5: f -: p = <*((f -: p) /. 1)*> ^ ((f -: p) /^ 1) by FINSEQ_5:29, FINSEQ_5:47
.= <*(f /. 1)*> ^ ((f -: p) /^ 1) by A4, FINSEQ_5:44 ;
A6: j + 1 = len (f :- p) ;
then A7: f :- p = ((f :- p) | j) ^ <*((f :- p) /. (len (f :- p)))*> by FINSEQ_5:21
.= ((f :- p) | j) ^ <*(f /. (len f))*> by A4, FINSEQ_5:54 ;
A8: p in rng (Rev f) by A4, FINSEQ_5:57;
thus Rev (Rotate (f,p)) = Rev ((f :- p) ^ ((f -: p) /^ 1)) by A4, Def2
.= (Rev ((f -: p) /^ 1)) ^ (Rev (f :- p)) by FINSEQ_5:64
.= (Rev ((f -: p) /^ 1)) ^ (<*(f /. (len f))*> ^ (Rev ((f :- p) | j))) by A7, FINSEQ_5:63
.= ((Rev ((f -: p) /^ 1)) ^ <*(f /. 1)*>) ^ (Rev ((f :- p) | j)) by A3, FINSEQ_1:32
.= (Rev (f -: p)) ^ (Rev ((f :- p) | j)) by A5, Th24
.= (Rev (f -: p)) ^ ((Rev (f :- p)) /^ 1) by A6, Th85
.= (Rev (f -: p)) ^ (((Rev f) -: p) /^ 1) by A2, Th87
.= ((Rev f) :- p) ^ (((Rev f) -: p) /^ 1) by A2, Th88
.= Rotate ((Rev f),p) by A8, Def2 ; :: thesis: verum