:: On the Decomposition of Finite Sequences
:: by Andrzej Trybulec
::
:: Received May 24, 1995
:: Copyright (c) 1995-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSEQ_1, ZFMISC_1, XBOOLE_0, FINSEQ_5, RELAT_1,
ORDINAL4, NAT_1, TARSKI, FUNCT_1, XXREAL_0, SUBSET_1, ARYTM_3, FINSEQ_4,
ARYTM_1, CARD_1, RFINSEQ, PARTFUN1, FINSEQ_6, JORDAN3;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, XXREAL_0, ZFMISC_1, REAL_1, NAT_1, NAT_D, RELAT_1, PARTFUN1,
RELSET_1, FUNCT_1, FINSEQ_1, FINSEQ_4, RFINSEQ, FINSEQ_5;
constructors XXREAL_0, NAT_1, INT_1, PARTFUN1, FINSEQ_4, RFINSEQ, BINARITH,
FINSEQ_5, REAL_1, RELSET_1, NAT_D, ENUMSET1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, INT_1, FINSEQ_1, FINSEQ_5,
ORDINAL1, NAT_1, CARD_1, XXREAL_0;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
expansions TARSKI, XBOOLE_0;
theorems NAT_1, FINSEQ_1, FINSEQ_4, FINSEQ_3, FINSEQ_2, FUNCT_1, ZFMISC_1,
FINSEQ_5, RELAT_1, RFINSEQ, TARSKI, ENUMSET1, PARTFUN2, GRFUNC_1, INT_1,
XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, PARTFUN1, NAT_D, XREAL_0,
XTUPLE_0;
begin :: Preliminaries
reserve x,y,z for set;
registration
let x,y,z;
cluster <*x,y,z*> -> non trivial;
coherence
proof
len <*x,y,z*> = 3 by FINSEQ_1:45;
hence thesis by NAT_D:60;
end;
end;
registration
let f be non empty FinSequence;
cluster Rev f -> non empty;
coherence
proof
dom f <> {};
hence thesis by FINSEQ_5:57,RELAT_1:38;
end;
end;
Lm1: rng <*x,y*> = { x,y }
proof
<*x,y*> = <*x*>^<*y*> by FINSEQ_1:def 9;
hence rng<*x,y*> = rng<*x*> \/ rng<*y*> by FINSEQ_1:31
.= {x} \/ rng<*y*> by FINSEQ_1:38
.= {x} \/ {y} by FINSEQ_1:38
.= {x,y} by ENUMSET1:1;
end;
Lm2: rng <*x,y,z*> = { x,y,z }
proof
<*x,y,z*> = <*x,y*>^<*z*> by FINSEQ_1:43;
hence rng<*x,y,z*> = rng<*x,y*> \/ rng<*z*> by FINSEQ_1:31
.= {x,y} \/ rng<*z*> by Lm1
.= {x,y} \/ {z} by FINSEQ_1:38
.= {x,y,z} by ENUMSET1:3;
end;
begin
reserve f,f1,f2,f3 for FinSequence,
p,p1,p2,p3 for set,
i,k for Nat;
theorem Th1:
for X being set, i st X c= Seg i & 1 in X holds (Sgm X).1 = 1
proof
let X be set, i such that
A1: X c= Seg i and
A2: 1 in X;
Sgm X <> {} by A1,A2,FINSEQ_1:51;
then len Sgm X >= 1 by NAT_1:14;
then 1 in dom Sgm X by FINSEQ_3:25;
then
A3: (Sgm X).1 in rng Sgm X by FUNCT_1:def 3;
rng Sgm X c= NAT by FINSEQ_1:def 4;
then reconsider k1 = (Sgm X).1 as Nat by A3;
assume
A4: (Sgm X).1 <> 1;
A5: rng Sgm X = X by A1,FINSEQ_1:def 13;
then consider x being object such that
A6: x in dom Sgm X and
A7: (Sgm X).x = 1 by A2,FUNCT_1:def 3;
A8: k1 >= 1 by A1,A5,A3,FINSEQ_1:1;
reconsider j = x as Nat by A6;
j >= 1 by A6,FINSEQ_3:25;
then
A9: 1 < j by A7,A4,XXREAL_0:1;
j <= len Sgm X by A6,FINSEQ_3:25;
hence contradiction by A1,A7,A8,A9,FINSEQ_1:def 13;
end;
theorem Th2:
for f being FinSequence holds k in dom f & (for i st 1 <= i & i <
k holds f.i <> f.k) implies (f.k)..f = k
proof
let f be FinSequence;
assume that
A1: k in dom f and
A2: for i st 1 <= i & i < k holds f.i <> f.k;
assume
A3: f.k..f <> k;
f.k..f <= k by A1,FINSEQ_4:24;
then
A4: f.k..f < k by A3,XXREAL_0:1;
A5: f.k in rng f by A1,FUNCT_1:def 3;
then f.(f.k..f) = f.k by FINSEQ_4:19;
hence contradiction by A2,A5,A4,FINSEQ_4:21;
end;
theorem Th3:
<*p1,p2*>| Seg 1 = <*p1*>
proof
set f = <*p1,p2*>| Seg 1;
len<*p1,p2*> = 2 by FINSEQ_1:44;
then 1 in dom<*p1,p2*> by FINSEQ_3:25;
then
A1: Seg 1 c= dom<*p1,p2*> by FINSEQ_1:2,ZFMISC_1:31;
A2: dom f = dom<*p1,p2*> /\ Seg 1 by RELAT_1:61
.= Seg 1 by A1,XBOOLE_1:28;
then reconsider f as FinSequence by FINSEQ_1:def 2;
1 in dom f by A2,FINSEQ_1:2,TARSKI:def 1;
then
A3: f.1 = <*p1,p2*>.1 by FUNCT_1:47
.= p1 by FINSEQ_1:44;
len f = 1 by A2,FINSEQ_1:def 3;
hence thesis by A3,FINSEQ_1:40;
end;
theorem Th4:
<*p1,p2,p3*>| Seg 1 = <*p1*>
proof
set f = <*p1,p2,p3*>| Seg 1;
len<*p1,p2,p3*> = 3 by FINSEQ_1:45;
then 1 in dom<*p1,p2,p3*> by FINSEQ_3:25;
then
A1: Seg 1 c= dom<*p1,p2,p3*> by FINSEQ_1:2,ZFMISC_1:31;
A2: dom f = dom<*p1,p2,p3*> /\ Seg 1 by RELAT_1:61
.= Seg 1 by A1,XBOOLE_1:28;
then reconsider f as FinSequence by FINSEQ_1:def 2;
1 in dom f by A2,FINSEQ_1:2,TARSKI:def 1;
then
A3: f.1 = <*p1,p2,p3*>.1 by FUNCT_1:47
.= p1 by FINSEQ_1:45;
len f = 1 by A2,FINSEQ_1:def 3;
hence thesis by A3,FINSEQ_1:40;
end;
theorem Th5:
<*p1,p2,p3*>| Seg 2 = <*p1,p2*>
proof
set f = <*p1,p2,p3*>| Seg 2;
A1: len<*p1,p2,p3*> = 3 by FINSEQ_1:45;
then
A2: 2 in dom<*p1,p2,p3*> by FINSEQ_3:25;
1 in dom<*p1,p2,p3*> by A1,FINSEQ_3:25;
then
A3: Seg 2 c= dom<*p1,p2,p3*> by A2,FINSEQ_1:2,ZFMISC_1:32;
A4: dom f = dom<*p1,p2,p3*> /\ Seg 2 by RELAT_1:61
.= Seg 2 by A3,XBOOLE_1:28;
then reconsider f as FinSequence by FINSEQ_1:def 2;
A5: len f = 2 by A4,FINSEQ_1:def 3;
then 2 in dom f by FINSEQ_3:25;
then
A6: f.2 = <*p1,p2,p3*>.2 by FUNCT_1:47
.= p2 by FINSEQ_1:45;
1 in dom f by A5,FINSEQ_3:25;
then f.1 = <*p1,p2,p3*>.1 by FUNCT_1:47
.= p1 by FINSEQ_1:45;
hence thesis by A5,A6,FINSEQ_1:44;
end;
theorem Th6:
p in rng f1 implies p..(f1^f2) = p..f1
proof
A1: dom f1 c= dom(f1^f2) by FINSEQ_1:26;
assume
A2: p in rng f1;
then
A3: p..f1 in dom f1 by FINSEQ_4:20;
A4: now
A5: (f1^f2).(p..f1) = f1.(p..f1) by A3,FINSEQ_1:def 7;
let i such that
A6: 1 <= i and
A7: i < p..f1;
p..f1 <= len f1 by A2,FINSEQ_4:21;
then i <= len f1 by A7,XXREAL_0:2;
then
A8: i in dom f1 by A6,FINSEQ_3:25;
then (f1^f2).i = f1.i by FINSEQ_1:def 7;
hence (f1^f2).i <> (f1^f2).(p..f1) by A2,A7,A8,A5,FINSEQ_4:19,24;
end;
f1.(p..f1) = p by A2,FINSEQ_4:19;
then (f1^f2).(p..f1) = p by A3,FINSEQ_1:def 7;
hence thesis by A3,A1,A4,Th2;
end;
theorem Th7:
p in rng f2 \ rng f1 implies p..(f1^f2) = len f1 + p..f2
proof
assume
A1: p in rng f2 \ rng f1;
then
A2: p..f2 in dom f2 by FINSEQ_4:20;
f2.(p..f2) = p by A1,FINSEQ_4:19;
then
A3: (f1^f2).(len f1 + p..f2) = p by A2,FINSEQ_1:def 7;
A4: now
let i such that
A5: 1 <= i and
A6: i < len f1 + p..f2;
per cases;
suppose
i <= len f1;
then
A7: i in dom f1 by A5,FINSEQ_3:25;
assume (f1^f2).i = (f1^f2).(len f1 + p..f2);
then f1.i = p by A3,A7,FINSEQ_1:def 7;
then p in rng f1 by A7,FUNCT_1:def 3;
hence contradiction by A1,XBOOLE_0:def 5;
end;
suppose
A8: i > len f1;
then reconsider j = i - len f1 as Element of NAT by INT_1:5;
j > 0 by A8,XREAL_1:50;
then
A9: 1 <= j by NAT_1:14;
A10: i = j + len f1;
then
A11: j < p..f2 by A6,XREAL_1:6;
A12: (f1^f2).(len f1 + p..f2) = f2.(p..f2) by A2,FINSEQ_1:def 7;
A13: p..f2 <= len f2 by A1,FINSEQ_4:21;
j <= p..f2 by A6,A10,XREAL_1:6;
then j <= len f2 by A13,XXREAL_0:2;
then
A14: j in dom f2 by A9,FINSEQ_3:25;
then (f1^f2).i = f2.j by A10,FINSEQ_1:def 7;
hence (f1^f2).i <> (f1^f2).(len f1 + p..f2) by A1,A11,A14,A12,FINSEQ_4:19
,24;
end;
end;
len f1 + p..f2 in dom(f1^f2) by A2,FINSEQ_1:28;
hence thesis by A3,A4,Th2;
end;
theorem Th8:
p in rng f1 implies (f1^f2)|--p = (f1|--p)^f2
proof
assume
A1: p in rng f1;
then
A2: p..f1 = p..(f1^f2) by Th6;
A3: len(f1|--p) = len f1 - p..f1 by A1,FINSEQ_4:def 6;
A4: now
let k;
assume
A5: k in dom((f1|--p)^f2);
per cases by A5,FINSEQ_1:25;
suppose
A6: k in dom(f1|--p);
len(f1|--p) = len f1 - p..f1 by A1,FINSEQ_4:def 6;
then
A7: len(f1|--p) + p..f1 = len f1;
k <= len(f1|--p) by A6,FINSEQ_3:25;
then
A8: k + p..f1 <= len f1 by A7,XREAL_1:6;
A9: k <= k + p..f1 by NAT_1:11;
1 <= k by A6,FINSEQ_3:25;
then 1 <= k + p..f1 by A9,XXREAL_0:2;
then
A10: k + p..f1 in dom f1 by A8,FINSEQ_3:25;
thus ((f1|--p)^f2).k = (f1|--p).k by A6,FINSEQ_1:def 7
.= f1.(k + p..f1) by A1,A6,FINSEQ_4:def 6
.= (f1^f2).(k + p..(f1^f2)) by A2,A10,FINSEQ_1:def 7;
end;
suppose
ex n being Nat st n in dom f2 & k = len(f1|--p) + n;
then consider n being Nat such that
A11: n in dom f2 and
A12: k = len(f1|--p) + n;
thus ((f1|--p)^f2).k = f2.n by A11,A12,FINSEQ_1:def 7
.= (f1^f2).(len f1 + n) by A11,FINSEQ_1:def 7
.= (f1^f2).(k + p..(f1^f2)) by A2,A3,A12;
end;
end;
rng(f1^f2) = rng f1 \/ rng f2 by FINSEQ_1:31;
then
A13: p in rng(f1^f2) by A1,XBOOLE_0:def 3;
len((f1|--p)^f2) = len f1 - p..f1 + len f2 by A3,FINSEQ_1:22
.= len f1 + len f2 - p..f1
.= len(f1^f2) - p..(f1^f2) by A2,FINSEQ_1:22;
hence thesis by A13,A4,FINSEQ_4:def 6;
end;
theorem Th9:
p in rng f2 \ rng f1 implies (f1^f2)|--p = f2|--p
proof
assume
A1: p in rng f2 \ rng f1;
then
A2: len f1 + p..f2 = p..(f1^f2) by Th7;
A3: now
let k;
A4: k <= k + p..f2 by NAT_1:11;
len(f2|--p) = len f2 - p..f2 by A1,FINSEQ_4:def 6;
then
A5: len(f2|--p) + p..f2 = len f2;
assume
A6: k in dom(f2|--p);
then k <= len(f2|--p) by FINSEQ_3:25;
then
A7: k + p..f2 <= len f2 by A5,XREAL_1:6;
1 <= k by A6,FINSEQ_3:25;
then 1 <= k + p..f2 by A4,XXREAL_0:2;
then
A8: k + p..f2 in dom f2 by A7,FINSEQ_3:25;
thus (f2|--p).k = f2.(k + p..f2) by A1,A6,FINSEQ_4:def 6
.= (f1^f2).(len f1 + (k + p..f2)) by A8,FINSEQ_1:def 7
.= (f1^f2).(k + p..(f1^f2)) by A2;
end;
rng(f1^f2) = rng f1 \/ rng f2 by FINSEQ_1:31;
then
A9: p in rng(f1^f2) by A1,XBOOLE_0:def 3;
len(f2|--p) = len f2 - p..f2 by A1,FINSEQ_4:def 6
.= len f1 + len f2 - (len f1 + p..f2)
.= len(f1^f2) - p..(f1^f2) by A2,FINSEQ_1:22;
hence thesis by A9,A3,FINSEQ_4:def 6;
end;
theorem Th10:
f1 c= f1^f2
proof
A1: for x be object st x in dom f1 holds f1.x = (f1^f2).x by FINSEQ_1:def 7;
dom f1 c= dom(f1^f2) by FINSEQ_1:26;
hence thesis by A1,GRFUNC_1:2;
end;
theorem
for A being set st A c= dom f1 holds (f1^f2)|A = f1 | A by Th10,GRFUNC_1:27;
theorem Th12:
p in rng f1 implies (f1^f2)-|p = f1-|p
proof
assume
A1: p in rng f1;
then consider n being Nat such that
A2: n = p..f1 - 1 and
A3: f1 | Seg n = f1 -| p by FINSEQ_4:def 5;
A4: p..f1 <= len f1 by A1,FINSEQ_4:21;
n + 1 = p..f1 by A2;
then n <= p..f1 by NAT_1:11;
then n <= len f1 by A4,XXREAL_0:2;
then Seg n c= Seg len f1 by FINSEQ_1:5;
then Seg n c= dom f1 by FINSEQ_1:def 3;
then
A5: (f1^f2) | Seg n = f1 | Seg n by Th10,GRFUNC_1:27;
rng(f1^f2) = rng f1 \/ rng f2 by FINSEQ_1:31;
then
A6: p in rng(f1^f2) by A1,XBOOLE_0:def 3;
n = p..(f1^f2) - 1 by A1,A2,Th6;
hence thesis by A3,A6,A5,FINSEQ_4:def 5;
end;
registration
let f1;
let i be Nat;
cluster f1|Seg i -> FinSequence-like;
coherence by FINSEQ_1:15;
end;
theorem Th13:
f1 c= f2 implies f3^f1 c= f3^f2
proof
assume
A1: f1 c= f2;
A2: dom(f3^f1) c= dom(f3^f2)
proof
let x be object;
assume
A3: x in dom(f3^f1);
then reconsider i = x as Nat;
per cases by A3,FINSEQ_1:25;
suppose
A4: i in dom f3;
dom f3 c= dom(f3^f2) by FINSEQ_1:26;
hence thesis by A4;
end;
suppose
A5: ex n being Nat st n in dom f1 & i=len f3 + n;
dom f1 c= dom f2 by A1,RELAT_1:11;
hence thesis by A5,FINSEQ_1:28;
end;
end;
for x being object st x in dom(f3^f1) holds (f3^f1).x = (f3^f2).x
proof
let x be object;
assume
A6: x in dom(f3^f1);
then reconsider i = x as Nat;
per cases by A6,FINSEQ_1:25;
suppose
A7: i in dom f3;
hence (f3^f1).x = f3.i by FINSEQ_1:def 7
.= (f3^f2).x by A7,FINSEQ_1:def 7;
end;
suppose
A8: ex n being Nat st n in dom f1 & i=len f3 + n;
A9: dom f1 c= dom f2 by A1,RELAT_1:11;
consider k be Nat such that
A10: k in dom f1 and
A11: i = len f3 + k by A8;
thus (f3^f1).x = f1.k by A10,A11,FINSEQ_1:def 7
.= f2.k by A1,A10,GRFUNC_1:2
.= (f3^f2).x by A10,A11,A9,FINSEQ_1:def 7;
end;
end;
hence thesis by A2,GRFUNC_1:2;
end;
theorem Th14:
(f1^f2)|Seg(len f1 + i) = f1^(f2|Seg i)
proof
A1: dom(f1^(f2|Seg i)) c= Seg(len f1 + i)
proof
let x be object;
assume
A2: x in dom(f1^(f2|Seg i));
then reconsider j = x as Nat;
per cases by A2,FINSEQ_1:25;
suppose
A3: j in dom f1;
len f1 <= len f1 + i by NAT_1:11;
then
A4: Seg len f1 c= Seg(len f1 + i) by FINSEQ_1:5;
j in Seg len f1 by A3,FINSEQ_1:def 3;
hence thesis by A4;
end;
suppose
ex n being Nat st n in dom(f2|Seg i) & j=len f1 + n;
then consider k be Nat such that
A5: k in dom(f2|Seg i) and
A6: j = len f1 + k;
A7: k <= j by A6,NAT_1:11;
dom(f2|Seg i) = dom f2 /\ Seg i by RELAT_1:61;
then k in Seg i by A5,XBOOLE_0:def 4;
then k <= i by FINSEQ_1:1;
then
A8: j <= len f1 + i by A6,XREAL_1:6;
1 <= k by A5,FINSEQ_3:25;
then 1 <= j by A7,XXREAL_0:2;
hence thesis by A8,FINSEQ_1:1;
end;
end;
A9: dom(f1^f2) /\ Seg(len f1 + i) c= dom(f1^(f2|Seg i))
proof
let x be object;
assume
A10: x in dom(f1^f2) /\ Seg(len f1 + i);
then
A11: x in dom(f1^f2) by XBOOLE_0:def 4;
reconsider j = x as Nat by A10;
per cases by A11,FINSEQ_1:25;
suppose
A12: j in dom f1;
dom f1 c= dom(f1^(f2|Seg i)) by FINSEQ_1:26;
hence thesis by A12;
end;
suppose
ex n being Nat st n in dom f2 & j=len f1 + n;
then consider k be Nat such that
A13: k in dom f2 and
A14: j = len f1 + k;
A15: 1 <= k by A13,FINSEQ_3:25;
A16: dom(f2|Seg i) = dom f2 /\ Seg i by RELAT_1:61;
j in Seg(len f1 + i) by A10,XBOOLE_0:def 4;
then j <= len f1 + i by FINSEQ_1:1;
then k <= i by A14,XREAL_1:6;
then k in Seg i by A15,FINSEQ_1:1;
then k in dom(f2|Seg i) by A13,A16,XBOOLE_0:def 4;
hence thesis by A14,FINSEQ_1:28;
end;
end;
A17: dom((f1^f2)|Seg(len f1 + i)) = dom(f1^f2) /\ Seg(len f1 + i) by RELAT_1:61
;
A18: now
let k be Nat;
assume
A19: k in dom((f1^f2)|Seg(len f1 + i));
then
A20: 1 <= k by FINSEQ_3:25;
per cases;
suppose
k <= len f1;
then
A21: k in dom f1 by A20,FINSEQ_3:25;
thus ((f1^f2)|Seg(len f1 + i)).k = (f1^f2).k by A19,FUNCT_1:47
.= f1.k by A21,FINSEQ_1:def 7
.= (f1^(f2|Seg i)).k by A21,FINSEQ_1:def 7;
end;
suppose
A22: k > len f1;
then reconsider j = k - len f1 as Element of NAT by INT_1:5;
j > 0 by A22,XREAL_1:50;
then
A23: 1 <= j by NAT_1:14;
A24: k = len f1 + j;
A25: not k in dom f1 by A22,FINSEQ_3:25;
k in dom(f1^f2) by A17,A19,XBOOLE_0:def 4;
then
A26: ex n being Nat st n in dom f2 & k =len f1 + n by A25,FINSEQ_1:25;
k in Seg(len f1 + i) by A17,A19,XBOOLE_0:def 4;
then k <= len f1 + i by FINSEQ_1:1;
then j <= i by A24,XREAL_1:6;
then
A27: j in Seg i by A23,FINSEQ_1:1;
dom(f2|Seg i) = (dom f2) /\ Seg i by RELAT_1:61;
then
A28: j in dom(f2|Seg i) by A27,A26,XBOOLE_0:def 4;
thus ((f1^f2)|Seg(len f1 + i)).k = (f1^f2).k by A19,FUNCT_1:47
.= f2.j by A26,FINSEQ_1:def 7
.= (f2|Seg i).j by A28,FUNCT_1:47
.= (f1^(f2|Seg i)).k by A24,A28,FINSEQ_1:def 7;
end;
end;
f1^(f2|Seg i) c= f1^f2 by Th13,RELAT_1:59;
then dom(f1^(f2|Seg i)) c= dom(f1^f2) by RELAT_1:11;
then dom(f1^(f2|Seg i)) c= dom(f1^f2) /\ Seg(len f1 + i) by A1,XBOOLE_1:19;
then dom((f1^f2)|Seg(len f1 + i)) = dom(f1^(f2|Seg i)) by A17,A9;
hence thesis by A18,FINSEQ_1:13;
end;
theorem Th15:
p in rng f2 \ rng f1 implies (f1^f2)-|p = f1^(f2-|p)
proof
assume
A1: p in rng f2 \ rng f1;
then consider n being Nat such that
A2: n = p..f2 - 1 and
A3: f2 | Seg n = f2 -| p by FINSEQ_4:def 5;
p..(f1^f2) = len f1 + p..f2 by A1,Th7;
then
A4: len f1 + n = p..(f1^f2) - 1 by A2;
rng(f1^f2) = rng f1 \/ rng f2 by FINSEQ_1:31;
then
A5: p in rng(f1^f2) by A1,XBOOLE_0:def 3;
(f1^f2) | Seg(len f1 + n) = f1^(f2-|p) by A3,Th14;
hence thesis by A5,A4,FINSEQ_4:def 5;
end;
theorem Th16:
f1^f2 just_once_values p implies p in rng f1 \+\ rng f2
proof
A1: rng(f1^f2) = rng f1 \/ rng f2 by FINSEQ_1:31;
assume
A2: f1^f2 just_once_values p;
A3: now
assume
A4: p in rng f1 /\ rng f2;
then p in rng f1 by XBOOLE_0:def 4;
then (f1^f2)|--p = (f1|--p)^f2 by Th8;
then
A5: not p in rng((f1|--p)^f2) by A2,FINSEQ_4:45;
rng((f1|--p)^f2) = rng(f1|--p) \/ rng f2 by FINSEQ_1:31;
then not p in rng f2 by A5,XBOOLE_0:def 3;
hence contradiction by A4,XBOOLE_0:def 4;
end;
p in rng(f1^f2) by A2,FINSEQ_4:5;
then p in (rng f1 \/ rng f2) \ rng f1 /\ rng f2 by A1,A3,XBOOLE_0:def 5;
hence thesis by XBOOLE_1:101;
end;
theorem
f1^f2 just_once_values p & p in rng f1 implies f1 just_once_values p
proof
assume that
A1: f1^f2 just_once_values p and
A2: p in rng f1;
(f1^f2)|--p = (f1|--p)^f2 by A2,Th8;
then
A3: rng((f1^f2)|--p) = rng(f1|--p) \/ rng f2 by FINSEQ_1:31;
not p in rng((f1^f2)|--p) by A1,FINSEQ_4:45;
then not p in rng(f1|--p) by A3,XBOOLE_0:def 3;
hence thesis by A2,FINSEQ_4:45;
end;
theorem Th18:
p..<*p*> = 1
proof
A1: for i st 1<=i & i<1 holds <*p*>.i <> <*p*>.1;
dom<*p*> = Seg 1 by FINSEQ_1:38;
then
A2: 1 in dom<*p*> by FINSEQ_1:2,TARSKI:def 1;
<*p*>.1 = p by FINSEQ_1:40;
hence thesis by A2,A1,Th2;
end;
theorem Th19:
p1..<*p1,p2*> = 1
proof
A1: for i st 1<=i & i<1 holds <*p1,p2*>.i <> <*p1,p2*>.1;
len<*p1,p2*> = 2 by FINSEQ_1:44;
then
A2: 1 in dom<*p1,p2*> by FINSEQ_3:25;
<*p1,p2*>.1 = p1 by FINSEQ_1:44;
hence thesis by A2,A1,Th2;
end;
theorem Th20:
p1 <> p2 implies p2..<*p1,p2*> = 2
proof
A1: <*p1,p2*>.2 = p2 by FINSEQ_1:44;
A2: <*p1,p2*>.1 = p1 by FINSEQ_1:44;
assume
A3: p1 <> p2;
A4: now
let i;
assume
A5: 1<=i;
assume i<1+1;
then i <= 1 by NAT_1:13;
hence <*p1,p2*>.i <> <*p1,p2*>.2 by A3,A1,A2,A5,XXREAL_0:1;
end;
2 <= len<*p1,p2*> by FINSEQ_1:44;
then 2 in dom<*p1,p2*> by FINSEQ_3:25;
hence thesis by A1,A4,Th2;
end;
theorem Th21:
p1..<*p1,p2,p3*> = 1
proof
A1: for i st 1<=i & i<1 holds <*p1,p2,p3*>.i <> <*p1,p2,p3*>.1;
len<*p1,p2,p3*> = 3 by FINSEQ_1:45;
then
A2: 1 in dom<*p1,p2,p3*> by FINSEQ_3:25;
<*p1,p2,p3*>.1 = p1 by FINSEQ_1:45;
hence thesis by A2,A1,Th2;
end;
theorem Th22:
p1 <> p2 implies p2..<*p1,p2,p3*> = 2
proof
A1: <*p1,p2,p3*>.2 = p2 by FINSEQ_1:45;
A2: <*p1,p2,p3*>.1 = p1 by FINSEQ_1:45;
assume
A3: p1 <> p2;
A4: now
let i;
assume
A5: 1<=i;
assume i<1+1;
then i <= 1 by NAT_1:13;
hence <*p1,p2,p3*>.i <> <*p1,p2,p3*>.2 by A3,A1,A2,A5,XXREAL_0:1;
end;
len<*p1,p2,p3*> = 3 by FINSEQ_1:45;
then 2 in dom<*p1,p2,p3*> by FINSEQ_3:25;
hence thesis by A1,A4,Th2;
end;
theorem Th23:
p1 <> p3 & p2 <> p3 implies p3..<*p1,p2,p3*> = 3
proof
assume that
A1: p1 <> p3 and
A2: p2 <> p3;
A3: <*p1,p2,p3*>.3 = p3 by FINSEQ_1:45;
A4: <*p1,p2,p3*>.1 = p1 by FINSEQ_1:45;
A5: <*p1,p2,p3*>.2 = p2 by FINSEQ_1:45;
A6: now
let i;
assume 1<=i;
then
A7: i <> 0;
assume i<2+1;
then i <= 2 by NAT_1:13;
then i = 0 or ... or i = 2;
hence <*p1,p2,p3*>.i <> <*p1,p2,p3*>.3 by A1,A2,A3,A5,A4,A7;
end;
3 <= len<*p1,p2,p3*> by FINSEQ_1:45;
then 3 in dom<*p1,p2,p3*> by FINSEQ_3:25;
hence thesis by A3,A6,Th2;
end;
theorem Th24:
for f being FinSequence holds Rev(<*p*>^f) = Rev f ^ <*p*>
proof
let f be FinSequence;
thus Rev(<*p*>^f) = Rev f ^ Rev<*p*> by FINSEQ_5:64
.= Rev f ^ <*p*> by FINSEQ_5:60;
end;
theorem
for f being FinSequence holds Rev Rev f = f;
theorem Th26:
x <> y implies <*x,y*> -| y = <*x*>
proof
assume x <> y;
then y..<*x,y*> = 1+1 by Th20;
then
A1: 1 = y..<*x,y*>-1;
rng<*x,y*> = { x,y } by Lm1;
then y in rng<*x,y*> by TARSKI:def 2;
hence <*x,y*> -| y = <*x,y*>| Seg 1 by A1,FINSEQ_4:33
.= <*x*> by Th3;
end;
theorem Th27:
x <> y implies <*x,y,z*> -| y = <*x*>
proof
assume x <> y;
then y..<*x,y,z*> = 1+1 by Th22;
then
A1: 1 = y..<*x,y,z*>-1;
rng<*x,y,z*> = { x,y,z } by Lm2;
then y in rng<*x,y,z*> by ENUMSET1:def 1;
hence <*x,y,z*> -| y = <*x,y,z*>| Seg 1 by A1,FINSEQ_4:33
.= <*x*> by Th4;
end;
theorem Th28:
x <> z & y <> z implies <*x,y,z*> -| z = <*x,y*>
proof
assume that
A1: x <> z and
A2: y <> z;
rng<*x,y,z*> = { x,y,z } by Lm2;
then
A3: z in rng<*x,y,z*> by ENUMSET1:def 1;
z..<*x,y,z*> = 2+1 by A1,A2,Th23;
then 2 = z..<*x,y,z*>-1;
hence <*x,y,z*> -| z = <*x,y,z*>| Seg 2 by A3,FINSEQ_4:33
.= <*x,y*> by Th5;
end;
theorem
<*x,y*>|--x = <*y*>
proof
A1: x..<*x,y*> = 1 by Th19;
then len<*y*> + x..<*x,y*> = 1 + 1 by FINSEQ_1:40
.= len<*x,y*> by FINSEQ_1:44;
then
A2: len<*y*> = len<*x,y*> - x..<*x,y*>;
A3: now
let k;
assume k in dom<*y*>;
then k in Seg 1 by FINSEQ_1:38;
then
A4: k = 1 by FINSEQ_1:2,TARSKI:def 1;
hence <*y*>.k = y by FINSEQ_1:40
.= <*x,y*>.(k + x..<*x,y*>) by A1,A4,FINSEQ_1:44;
end;
x in { x,y } by TARSKI:def 2;
then x in rng<*x,y*> by Lm1;
hence thesis by A2,A3,FINSEQ_4:def 6;
end;
theorem Th30:
x <> y implies <*x,y,z*>|--y = <*z*>
proof
assume x <> y;
then
A1: y..<*x,y,z*> = 2 by Th22;
then len<*z*> + y..<*x,y,z*> = 1 + 2 by FINSEQ_1:40
.= len<*x,y,z*> by FINSEQ_1:45;
then
A2: len<*z*> = len<*x,y,z*> - y..<*x,y,z*>;
A3: now
let k;
assume k in dom<*z*>;
then k in Seg 1 by FINSEQ_1:38;
then
A4: k = 1 by FINSEQ_1:2,TARSKI:def 1;
hence <*z*>.k = z by FINSEQ_1:40
.= <*x,y,z*>.(k + y..<*x,y,z*>) by A1,A4,FINSEQ_1:45;
end;
y in { x,y,z } by ENUMSET1:def 1;
then y in rng<*x,y,z*> by Lm2;
hence thesis by A2,A3,FINSEQ_4:def 6;
end;
theorem
<*x,y,z*>|--x = <*y,z*>
proof
A1: x..<*x,y,z*> = 1 by Th21;
then len<*y,z*> + x..<*x,y,z*> = 2 + 1 by FINSEQ_1:44
.= len<*x,y,z*> by FINSEQ_1:45;
then
A2: len<*y,z*> = len<*x,y,z*> - x..<*x,y,z*>;
A3: len<*y,z*> = 2 by FINSEQ_1:44;
A4: now
let k;
assume k in dom<*y,z*>;
then
A5: k in Seg 2 by A3,FINSEQ_1:def 3;
per cases by A5,FINSEQ_1:2,TARSKI:def 2;
suppose
A6: k = 1;
hence <*y,z*>.k = y by FINSEQ_1:44
.= <*x,y,z*>.(k + x..<*x,y,z*>) by A1,A6,FINSEQ_1:45;
end;
suppose
A7: k = 2;
hence <*y,z*>.k = z by FINSEQ_1:44
.= <*x,y,z*>.(k + x..<*x,y,z*>) by A1,A7,FINSEQ_1:45;
end;
end;
x in { x,y,z } by ENUMSET1:def 1;
then x in rng<*x,y,z*> by Lm2;
hence thesis by A2,A4,FINSEQ_4:def 6;
end;
theorem Th32:
<*z*>|--z = {} & <*z*>-|z = {}
proof
z in { z } by TARSKI:def 1;
then
A1: z in rng<*z*> by FINSEQ_1:39;
A2: z..<*z*> = 1 by Th18;
len<*z*> = 1 by FINSEQ_1:39;
hence <*z*>|--z = {} by A1,A2,FINSEQ_4:49;
thus thesis by A1,A2,FINSEQ_4:40;
end;
theorem Th33:
x <> y implies <*x,y*> |-- y = {}
proof
y in { x,y } by TARSKI:def 2;
then
A1: y in rng<*x,y*> by Lm1;
assume x <> y;
then
A2: y..<*x,y*> = 2 by Th20;
len<*x,y*> = 2 by FINSEQ_1:44;
hence thesis by A1,A2,FINSEQ_4:49;
end;
theorem Th34:
x <> z & y <> z implies <*x,y,z*> |-- z = {}
proof
assume that
A1: x <> z and
A2: y <> z;
A3: len<*x,y,z*> = 3 by FINSEQ_1:45;
z in { x,y,z } by ENUMSET1:def 1;
then
A4: z in rng<*x,y,z*> by Lm2;
z..<*x,y,z*> = 3 by A1,A2,Th23;
hence thesis by A4,A3,FINSEQ_4:49;
end;
theorem Th35:
x in rng f & y in rng(f-|x) implies f-|x-|y = f-|y
proof
assume that
A1: x in rng f and
A2: y in rng(f-|x);
thus f-|y = ((f -| x) ^ <* x *> ^ (f |-- x))-|y by A1,FINSEQ_4:51
.= ((f -| x) ^ (<* x *> ^ (f |-- x)))-|y by FINSEQ_1:32
.= f-|x-|y by A2,Th12;
end;
theorem Th36:
not x in rng f1 implies x..(f1^<*x*>^f2) = len f1 + 1
proof
x in {x} by TARSKI:def 1;
then
A1: x in rng<*x*> by FINSEQ_1:38;
assume not x in rng f1;
then x in rng<*x*> \ rng f1 by A1,XBOOLE_0:def 5;
then
A2: (f1^<*x*>)|--x = <*x*>|--x by Th9
.= {} by Th32;
rng(f1^<*x*>) = rng f1 \/ rng<*x*> by FINSEQ_1:31;
then
A3: x in rng(f1^<*x*>) by A1,XBOOLE_0:def 3;
then len(f1^<*x*>) - x..(f1^<*x*>) = len ((f1^<*x*>)|--x) by FINSEQ_4:def 6
.= 0 by A2;
hence x..(f1^<*x*>^f2) = len(f1^<*x*>) by A3,Th6
.= len f1 + len<*x*> by FINSEQ_1:22
.= len f1 + 1 by FINSEQ_1:39;
end;
theorem Th37:
f just_once_values x implies x..f + x..Rev f = len f + 1
proof
assume
A1: f just_once_values x;
then
A2: x in rng f by FINSEQ_4:5;
then
A3: f = (f -| x) ^ <* x *> ^ (f |-- x) by FINSEQ_4:51;
then
A4: len f = len((f -| x) ^ <* x *>) + len(f |-- x) by FINSEQ_1:22
.= len(f -| x) + len<* x *> + len(f |-- x) by FINSEQ_1:22
.= len(f -| x) + 1 + len(f |-- x) by FINSEQ_1:39;
not x in rng(f|--x) by A1,FINSEQ_4:45;
then
A5: not x in rng Rev(f |-- x) by FINSEQ_5:57;
Rev f = Rev(f |-- x) ^ Rev((f -| x) ^ <* x *>) by A3,FINSEQ_5:64
.= Rev(f |-- x) ^ (<*x*> ^ Rev(f -| x)) by FINSEQ_5:63
.= Rev(f |-- x) ^ <*x*> ^ Rev(f -| x) by FINSEQ_1:32;
then
A6: x..Rev f = len Rev(f |-- x) + 1 by A5,Th36;
len(f -| x) + 1 = x..f - 1 + 1 by A2,FINSEQ_4:34
.= x..f;
hence x..f + x..Rev f = len(f -| x) + 1 + len Rev(f |-- x) + 1 by A6
.= len f + 1 by A4,FINSEQ_5:def 3;
end;
theorem Th38:
f just_once_values x implies Rev(f-|x) = Rev f |--x
proof
A1: len Rev(f-|x) = len(f-|x) by FINSEQ_5:def 3;
assume
A2: f just_once_values x;
then
A3: x in rng f by FINSEQ_4:5;
then
A4: x in rng Rev f by FINSEQ_5:57;
A5: x..f + x..Rev f = len f + 1 by A2,Th37;
A6: now
let k;
consider m being Nat such that
m = x..f - 1 and
A7: f-|x = f | Seg m by A3,FINSEQ_4:def 5;
assume
A8: k in dom Rev(f-|x);
then
A9: 1 <= k by FINSEQ_3:25;
then
A10: x..f - k <= x..f - 1 by XREAL_1:13;
A11: len(f-|x) = x..f - 1 by A3,FINSEQ_4:34;
k in dom(f-|x) by A8,FINSEQ_5:57;
then k <= x..f - 1 by A11,FINSEQ_3:25;
then
A12: k + 1 <= x..f by XREAL_1:19;
then k < x..f by NAT_1:13;
then k + x..Rev f < len f + 1 by A5,XREAL_1:6;
then k + x..Rev f <= len f by NAT_1:13;
then
A13: k + x..Rev f <= len Rev f by FINSEQ_5:def 3;
A14: 1 <= x..f - k by A12,XREAL_1:19;
then 0 <= x..f - k;
then x..f - k in NAT by INT_1:5,XREAL_1:49;
then
A15: x..f - 1 - k + 1 in dom(f | Seg m) by A7,A11,A14,A10,FINSEQ_3:25;
k <= k + x..Rev f by NAT_1:11;
then 1 <= k + x..Rev f by A9,XXREAL_0:2;
then
A16: k + x..Rev f in dom Rev f by A13,FINSEQ_3:25;
thus (Rev(f-|x)).k = (f-|x).(x..f - 1 - k + 1) by A8,A11,FINSEQ_5:def 3
.= f.(len f -(k + x..Rev f) + 1) by A5,A7,A15,FUNCT_1:47
.= (Rev f).(k + x..Rev f) by A16,FINSEQ_5:def 3;
end;
len(f-|x) = x..f - 1 by A3,FINSEQ_4:34
.= len f - x..Rev f by A5
.= len Rev f - x..Rev f by FINSEQ_5:def 3;
hence thesis by A4,A1,A6,FINSEQ_4:def 6;
end;
theorem
f just_once_values x implies Rev f just_once_values x
proof
assume
A1: f just_once_values x;
then
A2: x in rng f by FINSEQ_4:5;
then not x in rng(f-|x) by FINSEQ_4:37;
then not x in rng Rev(f-|x) by FINSEQ_5:57;
then
A3: not x in rng(Rev f |-- x) by A1,Th38;
x in rng Rev f by A2,FINSEQ_5:57;
hence thesis by A3,FINSEQ_4:45;
end;
begin
reserve D for non empty set,
p,p1,p2,p3 for Element of D,
f,f1,f2 for FinSequence of D;
theorem Th40:
p in rng f implies f-:p = (f -| p)^<*p*>
proof
assume p in rng f;
hence (f -| p)^<*p*> = f|(p..f) by FINSEQ_5:24
.= f-:p by FINSEQ_5:def 1;
end;
theorem Th41:
p in rng f implies f:-p = <*p*>^(f |-- p)
proof
assume p in rng f;
hence <*p*>^(f |-- p) = <*p*>^(f/^(p..f)) by FINSEQ_5:35
.= f:-p by FINSEQ_5:def 2;
end;
theorem Th42:
f <> {} implies f/.1 in rng f
proof
assume f <> {};
then 1 in dom f by FINSEQ_5:6;
hence thesis by PARTFUN2:2;
end;
theorem Th43:
f <> {} implies f/.1..f = 1
proof
assume f <> {};
then
A1: 1 in dom f by FINSEQ_5:6;
f/.1 in {f/.1} by TARSKI:def 1;
then
A2: 1 in (f qua Relation of NAT,D)"{f/.1} by A1,PARTFUN2:26;
f"{f/.1} c= dom f by RELAT_1:132;
then
A3: f"{f/.1} c= Seg len f by FINSEQ_1:def 3;
thus f/.1..f = Sgm(f"{f/.1}).1 by FINSEQ_4:def 4
.= 1 by A3,A2,Th1;
end;
theorem Th44:
f <> {} & f/.1 = p implies f-:p = <*p*> & f:-p = f
proof
assume that
A1: f <> {} and
A2: f/.1 = p;
A3: p in rng f by A1,A2,Th42;
p..f = 1 by A1,A2,Th43;
then
A4: f -| p = {} by A3,FINSEQ_4:40;
hence f-:p = {}^<*p*> by A3,Th40
.= <*p*> by FINSEQ_1:34;
thus f = {} ^ <* p *> ^ (f |-- p) by A3,A4,FINSEQ_4:51
.= <* p *> ^ (f |-- p) by FINSEQ_1:34
.= f:-p by A3,Th41;
end;
theorem Th45:
(<*p1*>^f)/^1 = f
proof
A1: (<*p1*>^f)/.1 = p1 by FINSEQ_5:15;
1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then
A2: 1 in dom<*p1*> by FINSEQ_1:38;
dom<*p1*> c= dom(<*p1*>^f) by FINSEQ_1:26;
then <*(<*p1*>^f)/.(0+1)*>^((<*p1*>^f)/^1) = (<*p1*>^f)/^0 by A2,FINSEQ_5:31
.= <*p1*>^f by FINSEQ_5:28;
hence thesis by A1,FINSEQ_1:33;
end;
theorem Th46:
<*p1,p2*>/^1 = <*p2*>
proof
<*p1,p2*> = <*p1*>^<*p2*> by FINSEQ_1:def 9;
hence thesis by Th45;
end;
theorem Th47:
<*p1,p2,p3*>/^1 = <*p2,p3*>
proof
<*p1,p2,p3*> = <*p1*>^<*p2,p3*> by FINSEQ_1:43;
hence thesis by Th45;
end;
theorem Th48:
k in dom f & (for i st 1 <= i & i < k holds f/.i <> f/.k) implies f/.k..f = k
proof
assume that
A1: k in dom f and
A2: for i st 1 <= i & i < k holds f/.i <> f/.k;
A3: f/.k in rng f by A1,PARTFUN2:2;
assume
A4: f/.k..f <> k;
f/.k..f <= k by A1,FINSEQ_5:39;
then f/.k..f < k by A4,XXREAL_0:1;
then f/.(f/.k..f) <> f/.k by A2,A3,FINSEQ_4:21;
hence contradiction by A3,FINSEQ_5:38;
end;
theorem Th49:
p1 <> p2 implies <*p1,p2*>-:p2 = <*p1,p2*>
proof
assume
A1: p1 <> p2;
rng<*p1,p2*> = { p1,p2 } by Lm1;
then p2 in rng<*p1,p2*> by TARSKI:def 2;
hence <*p1,p2*>-:p2 = (<*p1,p2*> -| p2)^<*p2*> by Th40
.= <*p1*>^<*p2*> by A1,Th26
.= <*p1,p2*> by FINSEQ_1:def 9;
end;
theorem Th50:
p1 <> p2 implies <*p1,p2,p3*>-:p2 = <*p1,p2*>
proof
assume
A1: p1 <> p2;
rng<*p1,p2,p3*> = { p1,p2,p3 } by Lm2;
then p2 in rng<*p1,p2,p3*> by ENUMSET1:def 1;
hence <*p1,p2,p3*>-:p2 = (<*p1,p2,p3*> -| p2)^<*p2*> by Th40
.= <*p1*>^<*p2*> by A1,Th27
.= <*p1,p2*> by FINSEQ_1:def 9;
end;
theorem Th51:
p1 <> p3 & p2 <> p3 implies <*p1,p2,p3*>-:p3 = <*p1,p2,p3*>
proof
assume that
A1: p1 <> p3 and
A2: p2 <> p3;
rng<*p1,p2,p3*> = { p1,p2,p3 } by Lm2;
then p3 in rng<*p1,p2,p3*> by ENUMSET1:def 1;
hence <*p1,p2,p3*>-:p3 = (<*p1,p2,p3*> -| p3)^<*p3*> by Th40
.= <*p1,p2*>^<*p3*> by A1,A2,Th28
.= <*p1,p2,p3*> by FINSEQ_1:43;
end;
theorem
<*p*>:-p = <*p*> & <*p*>-:p = <*p*>
proof
p in { p } by TARSKI:def 1;
then
A1: p in rng<*p*> by FINSEQ_1:39;
hence <*p*>:-p = <*p*>^(<*p*>|--p )by Th41
.= <*p*>^{} by Th32
.= <*p*> by FINSEQ_1:34;
thus <*p*>-:p = (<*p*>-|p)^<*p*> by A1,Th40
.= {}^<*p*> by Th32
.= <*p*> by FINSEQ_1:34;
end;
theorem Th53:
p1 <> p2 implies <*p1,p2*>:-p2 = <*p2*>
proof
assume
A1: p1 <> p2;
p2 in { p1,p2 } by TARSKI:def 2;
then p2 in rng<*p1,p2*> by Lm1;
hence <*p1,p2*>:-p2 = <*p2*>^(<*p1,p2*> |-- p2) by Th41
.= <*p2*>^{} by A1,Th33
.= <*p2*> by FINSEQ_1:34;
end;
theorem Th54:
p1 <> p2 implies <*p1,p2,p3*>:-p2 = <*p2,p3*>
proof
assume
A1: p1 <> p2;
p2 in { p1,p2,p3 } by ENUMSET1:def 1;
then p2 in rng<*p1,p2,p3*> by Lm2;
hence <*p1,p2,p3*>:-p2 = <*p2*>^(<*p1,p2,p3*> |-- p2) by Th41
.= <*p2*>^<*p3*> by A1,Th30
.= <*p2,p3*> by FINSEQ_1:def 9;
end;
theorem Th55:
p1 <> p3 & p2 <> p3 implies <*p1,p2,p3*>:-p3 = <*p3*>
proof
assume that
A1: p1 <> p3 and
A2: p2 <> p3;
p3 in { p1,p2,p3 } by ENUMSET1:def 1;
then p3 in rng<*p1,p2,p3*> by Lm2;
hence <*p1,p2,p3*>:-p3 = <*p3*>^(<*p1,p2,p3*> |-- p3) by Th41
.= <*p3*>^{} by A1,A2,Th34
.= <*p3*> by FINSEQ_1:34;
end;
theorem Th56:
p in rng f & p..f > k implies p..f = k + p..(f/^k)
proof
assume that
A1: p in rng f and
A2: p..f > k;
reconsider i = p..f - k as Element of NAT by A2,INT_1:5;
A3: i + k <= len f by A1,FINSEQ_4:21;
then
A4: i <= len f - k by XREAL_1:19;
k <= k + i by NAT_1:11;
then k <= len f by A3,XXREAL_0:2;
then
A5: i <= len(f/^k) by A4,RFINSEQ:def 1;
i <> 0 by A2;
then 1 <= i by NAT_1:14;
then
A6: i in dom(f/^k) by A5,FINSEQ_3:25;
A7: k+i = p..f;
A8: now
let j be Nat such that
A9: 1 <= j and
A10: j < i;
reconsider J=j as Nat;
k+j >= j by NAT_1:11;
then
A11: 1 <= k+j by A9,XXREAL_0:2;
j <= len(f/^k) by A5,A10,XXREAL_0:2;
then j in dom(f/^k) by A9,FINSEQ_3:25;
then
A12: f/.(k+j) = (f/^k)/.j by FINSEQ_5:27;
A13: k+i <= len f by A1,FINSEQ_4:21;
k+j < k+i by A10,XREAL_1:6;
then k+j <= len f by A13,XXREAL_0:2;
then
A14: k+J in dom f by A11,FINSEQ_3:25;
k+j < p..f by A7,A10,XREAL_1:6;
then
A15: f/.(k+j) <> p by A14,FINSEQ_5:39;
f/.(k+i) = (f/^k)/.i by A6,FINSEQ_5:27;
hence (f/^k)/.j <> (f/^k)/.i by A1,A12,A15,FINSEQ_5:38;
end;
(f/^k)/.i = f/.(k+i) by A6,FINSEQ_5:27
.= p by A1,FINSEQ_5:38;
then p..f - k = p..(f/^k) by A6,A8,Th48;
hence thesis;
end;
theorem Th57:
p in rng f & p..f > k implies p in rng(f/^k)
proof
assume that
A1: p in rng f and
A2: p..f > k;
A3: k+p..(f/^k) = p..f by A1,A2,Th56;
then p..(f/^k) <> 0 by A2;
then
A4: 1 <= p..(f/^k) by NAT_1:14;
p..f <= len f by A1,FINSEQ_4:21;
then k <= len f by A2,XXREAL_0:2;
then len(f/^k) = len f - k by RFINSEQ:def 1;
then
A5: len(f/^k) + k = len f;
k + p..(f/^k) <= len f by A1,A3,FINSEQ_4:21;
then p..(f/^k) <= len(f/^k) by A5,XREAL_1:6;
then
A6: p..(f/^k) in dom(f/^k) by A4,FINSEQ_3:25;
then (f/^k)/.(p..(f/^k)) in rng(f/^k) by PARTFUN2:2;
then f/.(k+p..(f/^k)) in rng(f/^k) by A6,FINSEQ_5:27;
hence thesis by A1,A3,FINSEQ_5:38;
end;
theorem Th58:
k < i & i in dom f implies f/.i in rng(f/^k)
proof
assume that
A1: k < i and
A2: i in dom f;
reconsider j = i - k as Element of NAT by A1,INT_1:5;
j > 0 by A1,XREAL_1:50;
then
A3: 1 <= j by NAT_1:14;
A4: i = j + k;
A5: i <= len f by A2,FINSEQ_3:25;
then k <= len f by A1,XXREAL_0:2;
then len(f/^k) = len f - k by RFINSEQ:def 1;
then len(f/^k) + k = len f;
then j <= len(f/^k) by A4,A5,XREAL_1:6;
then
A6: j in dom(f/^k) by A3,FINSEQ_3:25;
then f/.i = (f/^k)/.j by A4,FINSEQ_5:27;
hence thesis by A6,PARTFUN2:2;
end;
theorem Th59:
p in rng f & p..f > k implies (f/^k)-:p = (f-:p)/^k
proof
assume that
A1: p in rng f and
A2: p..f > k;
A3: p in rng(f/^k) by A1,A2,Th57;
p..f = k + p..(f/^k) by A1,A2,Th56;
then
A4: len((f/^k)-:p) = p..f - k by A3,FINSEQ_5:42
.= len(f-:p) - k by A1,FINSEQ_5:42;
A5: now
let m be Nat;
A6: m+k >= m by NAT_1:11;
reconsider M=m as Nat;
assume
A7: m in dom((f/^k)-:p);
then m <= len(f-:p) - k by A4,FINSEQ_3:25;
then
A8: m+k <= len(f-:p) by XREAL_1:19;
1 <= m by A7,FINSEQ_3:25;
then 1 <= m+k by A6,XXREAL_0:2;
then
A9: M+k in dom(f-:p) by A8,FINSEQ_3:25;
len((f/^k)-:p) = p..(f/^k) by A3,FINSEQ_5:42;
then
A10: m in Seg(p..(f/^k)) by A7,FINSEQ_1:def 3;
(f/^k)-:p = (f/^k)|(p..(f/^k)) by FINSEQ_5:def 1;
then
A11: dom((f/^k)-:p) c= dom(f/^k) by FINSEQ_5:18;
len(f-:p) = p..f by A1,FINSEQ_5:42;
then
A12: m+k in Seg(p..f) by A9,FINSEQ_1:def 3;
thus ((f/^k)-:p).m = ((f/^k)-:p)/.m by A7,PARTFUN1:def 6
.= (f/^k)/.m by A3,A10,FINSEQ_5:43
.= f/.(m+k) by A7,A11,FINSEQ_5:27
.= (f-:p)/.(M+k) by A1,A12,FINSEQ_5:43
.= (f-:p).(m+k) by A9,PARTFUN1:def 6;
end;
k <= len(f-:p) by A1,A2,FINSEQ_5:42;
hence thesis by A4,A5,RFINSEQ:def 1;
end;
theorem Th60:
p in rng f & p..f <> 1 implies (f/^1)-:p = (f-:p)/^1
proof
assume that
A1: p in rng f and
A2: p..f <> 1;
p..f >= 1 by A1,FINSEQ_4:21;
then p..f > 1 by A2,XXREAL_0:1;
hence thesis by A1,Th59;
end;
theorem Th61:
p in rng(f:-p)
proof
rng<*p*> = {p} by FINSEQ_1:39;
then
A1: p in rng<*p*> by TARSKI:def 1;
f:-p = <*p*>^(f/^p..f) by FINSEQ_5:def 2;
then rng(f:-p) = rng<*p*> \/ rng(f/^p..f) by FINSEQ_1:31;
hence thesis by A1,XBOOLE_0:def 3;
end;
theorem Th62:
x in rng f & p in rng f & x..f >= p..f implies x in rng(f:-p)
proof
assume that
A1: x in rng f and
A2: p in rng f and
A3: x..f >= p..f;
per cases by A3,XXREAL_0:1;
suppose
A4: x..f > p..f;
rng f c= D by FINSEQ_1:def 4;
then reconsider q = x as Element of D by A1;
f:-p = <*p*>^(f/^p..f) by FINSEQ_5:def 2;
then
A5: rng(f:-p) = rng<*p*> \/ rng(f/^p..f) by FINSEQ_1:31;
q in rng(f/^(p..f)) by A1,A4,Th57;
hence thesis by A5,XBOOLE_0:def 3;
end;
suppose
x..f = p..f;
then x = f.(p..f) by A1,FINSEQ_4:19
.= p by A2,FINSEQ_4:19;
hence thesis by Th61;
end;
end;
theorem Th63:
p in rng f & k <= len f & k >= p..f implies f/.k in rng(f:-p)
proof
assume that
A1: p in rng f and
A2: k <= len f and
A3: k >= p..f;
set x = f/.k;
per cases by A3,XXREAL_0:1;
suppose
A4: k > p..f;
reconsider q = x as Element of D;
1 <= p..f by A1,FINSEQ_4:21;
then 1 <= k by A3,XXREAL_0:2;
then k in dom f by A2,FINSEQ_3:25;
then
A5: q in rng(f/^(p..f)) by A4,Th58;
f:-p = <*p*>^(f/^p..f) by FINSEQ_5:def 2;
then rng(f:-p) = rng<*p*> \/ rng(f/^p..f) by FINSEQ_1:31;
hence thesis by A5,XBOOLE_0:def 3;
end;
suppose
k = p..f;
then x = p by A1,FINSEQ_5:38;
hence thesis by Th61;
end;
end;
theorem Th64:
p in rng f1 implies (f1^f2):-p = (f1:-p)^f2
proof
assume
A1: p in rng f1;
rng(f1^f2) = rng f1 \/ rng f2 by FINSEQ_1:31;
then p in rng(f1^f2) by A1,XBOOLE_0:def 3;
hence (f1^f2):-p = <*p*>^((f1^f2)|--p) by Th41
.= <*p*>^((f1|--p)^f2) by A1,Th8
.= <*p*>^(f1|--p)^f2 by FINSEQ_1:32
.= (f1:-p)^f2 by A1,Th41;
end;
theorem Th65:
p in rng f2 \ rng f1 implies (f1^f2):-p = f2:-p
proof
assume
A1: p in rng f2 \ rng f1;
rng(f1^f2) = rng f1 \/ rng f2 by FINSEQ_1:31;
then p in rng(f1^f2) by A1,XBOOLE_0:def 3;
hence (f1^f2):-p = <*p*>^((f1^f2)|--p) by Th41
.= <*p*>^(f2|--p) by A1,Th9
.= f2:-p by A1,Th41;
end;
theorem Th66:
p in rng f1 implies (f1^f2)-:p = f1-:p
proof
assume
A1: p in rng f1;
rng(f1^f2) = rng f1 \/ rng f2 by FINSEQ_1:31;
then p in rng(f1^f2) by A1,XBOOLE_0:def 3;
hence (f1^f2)-:p = ((f1^f2)-|p)^<*p*> by Th40
.= (f1-|p)^<*p*> by A1,Th12
.= f1-:p by A1,Th40;
end;
theorem Th67:
p in rng f2 \ rng f1 implies (f1^f2)-:p = f1^(f2-:p)
proof
assume
A1: p in rng f2 \ rng f1;
rng(f1^f2) = rng f1 \/ rng f2 by FINSEQ_1:31;
then p in rng(f1^f2) by A1,XBOOLE_0:def 3;
hence (f1^f2)-:p = ((f1^f2)-|p)^<*p*> by Th40
.= f1^(f2-|p)^<*p*> by A1,Th15
.= f1^((f2-|p)^<*p*>) by FINSEQ_1:32
.= f1^(f2-:p) by A1,Th40;
end;
theorem
f:-p:-p = f:-p
proof
A1: (<*p*>^(f/^p..f))/.1 = p by FINSEQ_5:15;
thus f:-p:-p = (<*p*>^(f/^p..f)):-p by FINSEQ_5:def 2
.= <*p*>^(f/^p..f) by A1,Th44
.= f:-p by FINSEQ_5:def 2;
end;
theorem Th69:
p1 in rng f & p2 in rng f \ rng(f-:p1) implies f|--p2 = f|--p1 |--p2
proof
assume that
A1: p1 in rng f and
A2: p2 in rng f \ rng(f-:p1);
not p2 in rng(f-:p1) by A2,XBOOLE_0:def 5;
then
A3: not p2 in rng((f-|p1)^<* p1 *>) by A1,Th40;
f = (f-|p1)^<* p1 *>^(f|--p1) by A1,FINSEQ_4:51;
then rng f = rng((f-|p1)^<* p1 *>) \/ rng(f|--p1) by FINSEQ_1:31;
then p2 in rng(f|--p1) by A2,A3,XBOOLE_0:def 3;
then
A4: p2 in rng(f|--p1) \ rng((f-|p1)^<* p1 *>) by A3,XBOOLE_0:def 5;
thus f|--p2 = ((f-|p1)^<* p1 *>^(f|--p1))|--p2 by A1,FINSEQ_4:51
.= f|--p1|--p2 by A4,Th9;
end;
theorem Th70:
p in rng f implies rng f = rng(f-:p) \/ rng(f:-p)
proof
assume
A1: p in rng f;
then f-:p = (f -| p)^<*p*> by Th40;
then
A2: rng( f-:p) = rng(f -| p) \/ rng<*p*> by FINSEQ_1:31;
f:-p = <*p*>^(f |-- p) by A1,Th41;
then
A3: rng(f:-p) = rng<*p*> \/ rng(f |-- p) by FINSEQ_1:31;
f = (f-|p)^<* p *>^(f|--p) by A1,FINSEQ_4:51;
hence rng f = rng((f-|p)^<* p *>) \/ rng(f|--p) by FINSEQ_1:31
.= rng(f-|p) \/ (rng<* p *> \/ rng<* p *>) \/ rng(f|--p) by FINSEQ_1:31
.= rng(f-|p) \/ rng<* p *> \/ rng<* p *> \/ rng(f|--p) by XBOOLE_1:4
.= rng(f-:p) \/ rng(f:-p) by A2,A3,XBOOLE_1:4;
end;
theorem Th71:
p1 in rng f & p2 in rng f \ rng(f-:p1) implies f:-p1:-p2 = f:-p2
proof
assume that
A1: p1 in rng f and
A2: p2 in rng f \ rng(f-:p1);
A3: not p2 in rng(f-:p1) by A2,XBOOLE_0:def 5;
f-:p1 = (f -| p1)^<*p1*> by A1,Th40;
then rng(f-:p1) = rng(f -| p1) \/ rng<*p1*> by FINSEQ_1:31;
then
A4: not p2 in rng<*p1*> by A3,XBOOLE_0:def 3;
rng f = rng(f-:p1) \/ rng(f:-p1) by A1,Th70;
then
A5: p2 in rng(f:-p1) by A2,A3,XBOOLE_0:def 3;
f:-p1 = <*p1*>^(f |-- p1) by A1,Th41;
then rng(f:-p1) = rng<*p1*> \/ rng(f |-- p1) by FINSEQ_1:31;
then p2 in rng(f|--p1) by A5,A4,XBOOLE_0:def 3;
then
A6: p2 in rng(f|--p1) \ rng<*p1*> by A4,XBOOLE_0:def 5;
thus f:-p1:-p2 = <*p2*>^((f:-p1)|--p2) by A5,Th41
.= <*p2*>^((<*p1*>^(f|--p1))|--p2) by A1,Th41
.= <*p2*>^(f|--p1|--p2) by A6,Th9
.= <*p2*>^(f|--p2) by A1,A2,Th69
.= f:-p2 by A2,Th41;
end;
theorem Th72:
p in rng f implies p..(f-:p) = p..f
proof
assume
A1: p in rng f;
then
A2: p..f <= len(f-:p) by FINSEQ_5:42;
A3: now
p..f <> 0 by A1,FINSEQ_4:21;
then p..f in Seg(p..f) by FINSEQ_1:3;
then
A4: (f-:p)/.(p..f) = f/.(p..f) by A1,FINSEQ_5:43;
let i such that
A5: 1 <= i and
A6: i < p..f;
i in Seg(p..f) by A5,A6,FINSEQ_1:1;
then
A7: (f-:p)/.i = f/.i by A1,FINSEQ_5:43;
p..f <= len f by A1,FINSEQ_4:21;
then i <= len f by A6,XXREAL_0:2;
then
A8: i in dom f by A5,FINSEQ_3:25;
f/.(p..f) = p by A1,FINSEQ_5:38;
hence (f-:p)/.i <> (f-:p)/.(p..f) by A6,A7,A4,A8,FINSEQ_5:39;
end;
1 <= p..f by A1,FINSEQ_4:21;
then
A9: p..f in dom(f-:p) by A2,FINSEQ_3:25;
(f-:p)/.(p..f) = p by A1,FINSEQ_5:45;
hence thesis by A9,A3,Th48;
end;
theorem Th73:
f|i|i = f|i
proof
f|i = f|Seg i by FINSEQ_1:def 15;
hence f|i|i = f|(Seg i)|Seg i by FINSEQ_1:def 15
.= f|((Seg i) /\ Seg i)
.= f|i by FINSEQ_1:def 15;
end;
theorem Th74:
p in rng f implies f-:p-:p = f-:p
proof
assume p in rng f;
then
A1: p..(f-:p) = p..f by Th72;
thus f-:p-:p = (f-:p)|(p..(f-:p)) by FINSEQ_5:def 1
.= (f|(p..f))|(p..f) by A1,FINSEQ_5:def 1
.= f|(p..f) by Th73
.= f-:p by FINSEQ_5:def 1;
end;
theorem Th75:
p1 in rng f & p2 in rng(f-:p1) implies f-:p1-:p2 = f-:p2
proof
assume that
A1: p1 in rng f and
A2: p2 in rng(f-:p1);
per cases;
suppose
p1 = p2;
hence thesis by A1,Th74;
end;
suppose
p1 <> p2;
then not p2 in { p1 } by TARSKI:def 1;
then
A3: not p2 in rng<*p1*> by FINSEQ_1:39;
f-:p1 = (f-|p1)^<*p1*> by A1,Th40;
then rng(f-:p1) = rng(f-|p1) \/ rng<*p1*> by FINSEQ_1:31;
then
A4: p2 in rng(f-|p1) by A2,A3,XBOOLE_0:def 3;
A5: rng(f-|p1) c= rng f by A1,FINSEQ_4:39;
thus f-:p1-:p2 = ((f-:p1)-|p2)^<*p2*> by A2,Th40
.= (((f-|p1)^<*p1*>)-|p2)^<*p2*> by A1,Th40
.= ((f-|p1)-|p2)^<*p2*> by A4,Th12
.= (f-|p2)^<*p2*> by A1,A4,Th35
.= f-:p2 by A4,A5,Th40;
end;
end;
theorem Th76:
p in rng f implies (f-:p)^((f:-p)/^1) = f
proof
A1: rng f c= D by FINSEQ_1:def 4;
assume
A2: p in rng f;
then rng(f|--p) c= rng f by FINSEQ_4:44;
then rng(f|--p) c= D by A1;
then reconsider f1 = f|--p as FinSequence of D by FINSEQ_1:def 4;
thus (f-:p)^((f:-p)/^1) = (f-|p)^<*p*>^((f:-p)/^1) by A2,Th40
.= (f-|p)^<*p*>^((<*p*>^f1)/^1) by A2,Th41
.= (f-|p)^<*p*>^(f|--p) by Th45
.= f by A2,FINSEQ_4:51;
end;
theorem Th77:
f1 <> {} implies (f1^f2)/^1 = (f1/^1)^f2
proof
assume f1 <> {};
then consider p being Element of D, df1 being FinSequence of D such that
p = f1.1 and
A1: f1 = <*p*>^df1 by FINSEQ_3:102;
thus (f1^f2)/^1 = (<*p*>^(df1^f2))/^1 by A1,FINSEQ_1:32
.= df1^f2 by Th45
.= (f1/^1)^f2 by A1,Th45;
end;
theorem Th78:
p2 in rng f & p2..f <> 1 implies p2 in rng(f/^1)
proof
assume that
A1: p2 in rng f and
A2: p2..f <> 1;
f = <*f/.1*>^(f/^1) by A1,FINSEQ_5:29,RELAT_1:38;
then
A3: rng f = rng<*f/.1*> \/ rng(f/^1) by FINSEQ_1:31;
assume not p2 in rng(f/^1);
then p2 in rng<*f/.1*> by A1,A3,XBOOLE_0:def 3;
then p2 in { f/.1 } by FINSEQ_1:39;
then p2 = f/.1 by TARSKI:def 1;
hence contradiction by A1,A2,Th43,RELAT_1:38;
end;
theorem Th79:
p..(f:-p) = 1
proof
(f:-p)/.1 = p by FINSEQ_5:53;
hence thesis by Th43;
end;
Lm3: p in rng f & p..f > i implies i + p..(f/^i) = p..f
proof
assume that
A1: p in rng f and
A2: p..f > i;
reconsider k = p..f - i as Element of NAT by A2,INT_1:5;
A3: p..f <= len f by A1,FINSEQ_4:21;
then
A4: i <= len f by A2,XXREAL_0:2;
p..f - i <= len f - i by A3,XREAL_1:9;
then
A5: k <= len(f/^i) by A4,RFINSEQ:def 1;
k <> 0 by A2;
then 1 <= k by NAT_1:14;
then
A6: k in dom(f/^i) by A5,FINSEQ_3:25;
A7: now
let j be Nat such that
A8: 1 <= j and
A9: j < k;
j <= i + j by NAT_1:11;
then
A10: 1 <= i + j by A8,XXREAL_0:2;
i + k = p..f;
then
A11: i + j < p..f by A9,XREAL_1:6;
then i + j <= len f by A3,XXREAL_0:2;
then
A12: i + j in dom f by A10,FINSEQ_3:25;
j <= len(f/^i) by A5,A9,XXREAL_0:2;
then j in dom(f/^i) by A8,FINSEQ_3:25;
then
A13: f.(i+j) = (f/^i).j by A4,RFINSEQ:def 1;
f.(i+k) = (f/^i).k by A4,A6,RFINSEQ:def 1;
hence (f/^i).j <> (f/^i).k by A1,A13,A11,A12,FINSEQ_4:19,24;
end;
(f/^i).k = f.(k+i) by A4,A6,RFINSEQ:def 1
.= p by A1,FINSEQ_4:19;
then p..(f/^i) = k by A6,A7,Th2;
hence thesis;
end;
theorem Th80:
<*>D/^k = <*>D
proof
per cases;
suppose
k = 0;
hence thesis by FINSEQ_5:28;
end;
suppose
k > 0;
then k > len <*>D;
hence thesis by RFINSEQ:def 1;
end;
end;
theorem Th81:
f/^(i+k) = f/^i/^k
proof
per cases;
suppose
A1: i+k <= len f;
i <= i+k by NAT_1:11;
then
A2: i <= len f by A1,XXREAL_0:2;
then
A3: len(f/^i) = len f - i by RFINSEQ:def 1;
then
A4: k <= len(f/^i) by A1,XREAL_1:19;
A5: now
let m be Nat;
assume
A6: m in dom(f/^i/^k);
then
A7: m+k in dom(f/^i) by FINSEQ_5:26;
thus (f/^i/^k).m = (f/^i).(m+k) by A4,A6,RFINSEQ:def 1
.= f.(m+k+i) by A2,A7,RFINSEQ:def 1
.= f.(m+(i+k));
end;
len(f/^i/^k) = len(f/^i) - k by A4,RFINSEQ:def 1
.= len f -(i+k) by A3;
hence thesis by A1,A5,RFINSEQ:def 1;
end;
suppose that
A8: i+k > len f and
A9: i<= len f;
len(f/^i) = len f - i by A9,RFINSEQ:def 1;
then len(f/^i) + i = len f;
then
A10: k > len(f/^i) by A8,XREAL_1:6;
thus f/^(i+k) = <*>D by A8,RFINSEQ:def 1
.= f/^i/^k by A10,RFINSEQ:def 1;
end;
suppose that
A11: i+k > len f and
A12: i > len f;
thus f/^(i+k) = <*>D by A11,RFINSEQ:def 1
.= <*>D/^k by Th80
.= f/^i/^k by A12,RFINSEQ:def 1;
end;
end;
theorem Th82:
p in rng f & p..f > k implies (f/^k):-p = f:-p
proof
assume that
A1: p in rng f and
A2: p..f > k;
thus (f/^k):-p =<*p*>^(f/^k/^(p..(f/^k))) by FINSEQ_5:def 2
.=<*p*>^(f/^(k + p..(f/^k))) by Th81
.=<*p*>^(f/^p..f) by A1,A2,Lm3
.= f:-p by FINSEQ_5:def 2;
end;
theorem Th83:
p in rng f & p..f <> 1 implies (f/^1):-p = f:-p
proof
assume that
A1: p in rng f and
A2: p..f <> 1;
p..f >= 1 by A1,FINSEQ_4:21;
then p..f > 1 by A2,XXREAL_0:1;
hence thesis by A1,Th82;
end;
theorem Th84:
i + k = len f implies Rev(f/^k) = Rev f|i
proof
assume
A1: i + k = len f;
then
A2: k <= len f by NAT_1:11;
i <= len f by A1,NAT_1:11;
then i <= len Rev f by FINSEQ_5:def 3;
then
A3: len(Rev f|i) = len f - k by A1,FINSEQ_1:59
.= len(f/^k) by A2,RFINSEQ:def 1;
now
A4: len(f/^k) = len f - k by A2,RFINSEQ:def 1;
let j be Nat;
A5: dom(Rev f|i) c= dom Rev f by FINSEQ_5:18;
assume
A6: j in dom(Rev f|i);
then j <= len(f/^k) by A3,FINSEQ_3:25;
then reconsider m = len(f/^k) - j as Element of NAT by INT_1:5;
j >= 1 by A6,FINSEQ_3:25;
then len(f/^k) - j <= len(f/^k) - 1 by XREAL_1:10;
then
A7: len(f/^k) - j + 1 <= len(f/^k) by XREAL_1:19;
1 <= m + 1 by NAT_1:11;
then
A8: m + 1 in dom(f/^k) by A7,FINSEQ_3:25;
thus (Rev f|i).j = (Rev f|i)/.j by A6,PARTFUN1:def 6
.= (Rev f)/.j by A6,FINSEQ_4:70
.= (Rev f).j by A6,A5,PARTFUN1:def 6
.= f.(len(f/^k) + k - j + 1) by A6,A5,A4,FINSEQ_5:def 3
.= f.(m + 1 + k)
.= (f/^k).(len(f/^k) - j + 1) by A2,A8,RFINSEQ:def 1;
end;
hence thesis by A3,FINSEQ_5:def 3;
end;
theorem Th85:
i + k = len f implies Rev(f|k) = Rev f/^i
proof
assume i + k = len f;
then
A1: i + k = len Rev f by FINSEQ_5:def 3;
thus Rev(f|k) = Rev(Rev Rev f |k)
.= Rev Rev(Rev f/^i) by A1,Th84
.= Rev f/^i;
end;
theorem Th86:
f just_once_values p implies Rev(f|--p) = Rev f -|p
proof
assume
A1: f just_once_values p;
then
A2: p in rng f by FINSEQ_4:5;
then
A3: p in rng Rev f by FINSEQ_5:57;
then reconsider n = p..Rev f - 1 as Element of NAT
by FINSEQ_4:21,INT_1:5;
p..f + p..Rev f = len f + 1 by A1,Th37;
then
A4: n + p..f = len f;
Rev(f|--p) = Rev(f/^(p..f)) by A2,FINSEQ_5:35
.= (Rev f) | n by A4,Th84
.= (Rev f) | Seg n by FINSEQ_1:def 15;
hence thesis by A3,FINSEQ_4:def 5;
end;
theorem Th87:
f just_once_values p implies Rev(f:-p) = Rev f -:p
proof
assume
A1: f just_once_values p;
then
A2: p in rng f by FINSEQ_4:5;
then
A3: p in rng Rev f by FINSEQ_5:57;
thus Rev(f:-p) = Rev(<*p*>^(f|--p)) by A2,Th41
.= Rev(f|--p)^<*p*> by Th24
.= (Rev f -|p)^<*p*> by A1,Th86
.= Rev f -:p by A3,Th40;
end;
theorem Th88:
f just_once_values p implies Rev(f-:p) = Rev f :-p
proof
assume
A1: f just_once_values p;
then
A2: p in rng f by FINSEQ_4:5;
then
A3: p in rng Rev f by FINSEQ_5:57;
thus Rev(f-:p) = Rev((f-|p)^<*p*>) by A2,Th40
.= <*p*>^Rev(f-|p) by FINSEQ_5:63
.= <*p*>^(Rev f |-- p) by A1,Th38
.= Rev f :-p by A3,Th41;
end;
begin :: rotation, circular
definition
let D be non empty set;
let IT be FinSequence of D;
attr IT is circular means
:Def1:
IT/.1 = IT/.len IT;
end;
definition
let D,f,p;
func Rotate(f,p) -> FinSequence of D equals
:Def2:
(f:-p)^((f-:p)/^1) if p
in rng f otherwise f;
correctness;
end;
registration
let D;
let f be non empty FinSequence of D, p be Element of D;
cluster Rotate(f,p) -> non empty;
coherence
proof
per cases;
suppose
A1: p in rng f;
(f:-p)^((f-:p)/^1) is non empty;
hence thesis by A1,Def2;
end;
suppose
not p in rng f;
hence thesis by Def2;
end;
end;
end;
registration
let D;
cluster circular 1-element for FinSequence of D;
existence
proof
set d = the Element of D;
take <*d*>;
<*d*>/.1 = <*d*>/.len<*d*> by FINSEQ_1:39;
hence <*d*> is circular;
thus thesis;
end;
cluster circular non trivial for FinSequence of D;
existence
proof
set d = the Element of D;
take <*d,d*>;
len<*d,d*> = 2 by FINSEQ_1:44;
then <*d,d*>/.len<*d,d*> = d by FINSEQ_4:17
.= <*d,d*>/.1 by FINSEQ_4:17;
hence <*d,d*> is circular;
thus thesis;
end;
end;
theorem Th89:
Rotate(f,f/.1) = f
proof
A1: len<*f/.1*> = 1 by FINSEQ_1:39;
per cases;
suppose
A2: f is non empty;
then f/.1 in rng f by Th42;
hence Rotate(f,f/.1) = (f:-f/.1)^((f-:f/.1)/^1) by Def2
.= f^((f-:f/.1)/^1) by A2,Th44
.= f^(<*f/.1*>/^1) by A2,Th44
.= f^{} by A1,FINSEQ_5:32
.= f by FINSEQ_1:34;
end;
suppose
f is empty;
hence thesis by Def2,RELAT_1:38;
end;
end;
registration
let D,p;
let f be circular non empty FinSequence of D;
cluster Rotate(f,p) -> circular;
coherence
proof
per cases;
suppose
not p in rng f;
hence thesis by Def2;
end;
suppose that
A1: p in rng f and
A2: p <> f/.1;
A3: p..f >= 1 by A1,FINSEQ_4:21;
A4: Rotate(f,p) = (f:-p)^((f-:p)/^1) by A1,Def2;
p..f <> 1 by A1,A2,FINSEQ_5:38;
then p..f > 1 by A3,XXREAL_0:1;
then p..f >= 1+1 by NAT_1:13;
then
A5: len(f-:p) >= 1+1 by A1,FINSEQ_5:42;
then 1 <= len(f-:p) by XXREAL_0:2;
then
A6: len((f-:p)/^1) = len(f-:p)-1 by RFINSEQ:def 1;
then len((f-:p)/^1) + 1 = len(f-:p);
then len((f-:p)/^1) >= 1 by A5,XREAL_1:6;
then
A7: len((f-:p)/^1) in dom((f-:p)/^1) by FINSEQ_3:25;
1 in dom(f:-p) by FINSEQ_5:6;
hence (Rotate(f,p))/.1 = (f:-p)/.1 by A4,FINSEQ_4:68
.= p by FINSEQ_5:53
.= (f-:p)/.(p..f) by A1,FINSEQ_5:45
.= (f-:p)/.(len((f-:p)/^1)+1) by A1,A6,FINSEQ_5:42
.= ((f-:p)/^1)/.(len((f-:p)/^1)) by A7,FINSEQ_5:27
.= ((f:-p)^((f-:p)/^1))/.(len(f:-p)+len((f-:p)/^1)) by A7,FINSEQ_4:69
.= (Rotate(f,p))/.len Rotate(f,p) by A4,FINSEQ_1:22;
end;
suppose
p in rng f & p = f/.1;
hence thesis by Th89;
end;
end;
end;
theorem
f is circular & p in rng f implies rng Rotate(f,p) = rng f
proof
assume that
A1: f is circular and
A2: p in rng f;
A3: Rotate(f,p) = (f:-p)^((f-:p)/^1) by A2,Def2;
A4: rng((f-:p)/^1) c= rng(f-:p) by FINSEQ_5:33;
rng(f-:p) c= rng f by FINSEQ_5:48;
then
A5: rng((f-:p)/^1) c= rng f by A4;
A6: rng((f:-p)^((f-:p)/^1)) = rng(f:-p) \/ rng((f-:p)/^1) by FINSEQ_1:31;
rng(f:-p) c= rng f by A2,FINSEQ_5:55;
hence rng Rotate(f,p) c= rng f by A3,A6,A5,XBOOLE_1:8;
let x be object;
assume x in rng f;
then consider i being Nat such that
A7: i in dom f and
A8: f.i = x by FINSEQ_2:10;
A9: x = f/.i by A7,A8,PARTFUN1:def 6;
per cases;
suppose
A10: i = 1;
len(f:-p) = len(<*p*>^(f/^p..f)) by FINSEQ_5:def 2
.= len<*p*> + len(f/^p..f) by FINSEQ_1:22
.= 1 + len(f/^p..f) by FINSEQ_1:39;
then 1 <= len(f:-p) by NAT_1:11;
then
A11: len(f:-p) in dom(f:-p) by FINSEQ_3:25;
x = f/.len f by A1,A9,A10
.= (f:-p)/.len(f:-p) by A2,FINSEQ_5:54;
then x in rng(f:-p) by A11,PARTFUN2:2;
hence thesis by A3,A6,XBOOLE_0:def 3;
end;
suppose that
A12: i <= p..f and
A13: i <> 1;
A14: i <> 0 by A7,FINSEQ_3:25;
then
A15: i > 0+1 by A13,NAT_1:25;
then
A16: i in Seg(p..f) by A12,FINSEQ_1:1;
consider j being Nat such that
A17: i = j+1 by A14,NAT_1:6;
A18: j >= 1 by A15,A17,NAT_1:14;
A19: i <= len(f-:p) by A2,A12,FINSEQ_5:42;
then 1 <= len(f-:p) by A14,NAT_1:25,XXREAL_0:2;
then len((f-:p)/^1) = len(f-:p) - 1 by RFINSEQ:def 1;
then len((f-:p)/^1) + 1 = len(f-:p);
then j <= len((f-:p)/^1) by A17,A19,XREAL_1:6;
then
A20: j in dom((f-:p)/^1) by A18,FINSEQ_3:25;
A21: len<*(f-:p)/.1*> = 1 by FINSEQ_1:39;
f-:p = <*(f-:p)/.1*>^((f-:p)/^1) by A2,FINSEQ_5:29,47;
then ((f-:p)/^1)/.j = (f-:p)/.i by A17,A20,A21,FINSEQ_4:69
.= f/.i by A2,A16,FINSEQ_5:43;
then x in rng((f-:p)/^1) by A9,A20,PARTFUN2:2;
hence thesis by A3,A6,XBOOLE_0:def 3;
end;
suppose
i > p..f;
then reconsider j = i - p..f as Element of NAT by INT_1:5;
A22: j+1 >= 1 by NAT_1:11;
i <= len f by A7,FINSEQ_3:25;
then
A23: j <= len f - p..f by XREAL_1:9;
len (f:-p) = len f - p..f + 1 by A2,FINSEQ_5:50;
then j + 1 <= len(f:-p) by A23,XREAL_1:6;
then
A24: j+1 in dom(f:-p) by A22,FINSEQ_3:25;
j + p..f = i;
then f/.i = (f:-p)/.(j+1) by A2,A24,FINSEQ_5:52;
then x in rng(f:-p) by A9,A24,PARTFUN2:2;
hence thesis by A3,A6,XBOOLE_0:def 3;
end;
end;
theorem Th91:
p in rng f implies p in rng Rotate(f,p)
proof
p in {p} by TARSKI:def 1;
then p in rng<*p*> by FINSEQ_1:39;
then p in rng<*p*> \/ rng(f/^p..f) by XBOOLE_0:def 3;
then p in rng(<*p*>^(f/^p..f)) by FINSEQ_1:31;
then
A1: p in rng(f:-p) by FINSEQ_5:def 2;
assume p in rng f;
then Rotate(f,p) = (f:-p)^((f-:p)/^1) by Def2;
then rng Rotate(f,p) = rng(f:-p) \/ rng((f-:p)/^1) by FINSEQ_1:31;
hence thesis by A1,XBOOLE_0:def 3;
end;
theorem Th92:
p in rng f implies (Rotate(f,p))/.1 = p
proof
assume p in rng f;
then Rotate(f,p) =(f:-p)^((f-:p)/^1) by Def2
.= <*p*>^(f/^p..f)^((f-:p)/^1) by FINSEQ_5:def 2
.= <*p*>^((f/^p..f)^((f-:p)/^1)) by FINSEQ_1:32;
hence thesis by FINSEQ_5:15;
end;
theorem Th93:
Rotate(Rotate(f,p),p) = Rotate(f,p)
proof
per cases;
suppose
A1: p in rng f;
then reconsider f9 = f as non empty FinSequence of D;
A2: (Rotate(f,p))/.1 = p by A1,Th92;
then
A3: Rotate(f9,p):-p = Rotate(f,p) by Th44;
A4: p in rng Rotate(f,p) by A1,Th91;
A5: len<*p*> = 1 by FINSEQ_1:39;
Rotate(f9,p)-:p = <*p*> by A2,Th44;
hence Rotate(Rotate(f,p),p) = Rotate(f,p)^(<*p*>/^1) by A3,A4,Def2
.= Rotate(f,p)^{} by A5,FINSEQ_5:32
.= Rotate(f,p) by FINSEQ_1:34;
end;
suppose
not p in rng f;
hence thesis by Def2;
end;
end;
theorem
Rotate(<*p*>,p) = <*p*>
proof
<*p*>/.1 = p by FINSEQ_4:16;
hence thesis by Th89;
end;
theorem Th95:
Rotate(<*p1,p2*>,p1) = <*p1,p2*>
proof
<*p1,p2*>/.1 = p1 by FINSEQ_4:17;
hence thesis by Th89;
end;
theorem
Rotate(<*p1,p2*>,p2) = <*p2,p2*>
proof
per cases;
suppose
p1 = p2;
hence thesis by Th95;
end;
suppose
A1: p1 <> p2;
rng<*p1,p2*> = {p1,p2} by Lm1;
then p2 in rng<*p1,p2*> by TARSKI:def 2;
hence Rotate(<*p1,p2*>,p2) = (<*p1,p2*>:-p2)^((<*p1,p2*>-:p2)/^1) by Def2
.= <*p2*>^((<*p1,p2*>-:p2)/^1) by A1,Th53
.= <*p2*>^(<*p1,p2*>/^1) by A1,Th49
.= <*p2*>^<*p2*> by Th46
.= <*p2,p2*> by FINSEQ_1:def 9;
end;
end;
theorem Th97:
Rotate(<*p1,p2,p3*>,p1) = <*p1,p2,p3*>
proof
<*p1,p2,p3*>/.1 = p1 by FINSEQ_4:18;
hence thesis by Th89;
end;
theorem
p1 <> p2 implies Rotate(<*p1,p2,p3*>,p2) = <*p2,p3,p2*>
proof
assume
A1: p1 <> p2;
rng<*p1,p2,p3*> = {p1,p2,p3} by Lm2;
then p2 in rng<*p1,p2,p3*> by ENUMSET1:def 1;
hence
Rotate(<*p1,p2,p3*>,p2) = (<*p1,p2,p3*>:-p2)^((<*p1,p2,p3*>-:p2)/^1) by Def2
.= <*p2,p3*>^((<*p1,p2,p3*>-:p2)/^1) by A1,Th54
.= <*p2,p3*>^(<*p1,p2*>/^1) by A1,Th50
.= <*p2,p3*>^<*p2*> by Th46
.= <*p2,p3,p2*> by FINSEQ_1:43;
end;
theorem
p2 <> p3 implies Rotate(<*p1,p2,p3*>,p3) = <*p3,p2,p3*>
proof
assume
A1: p2 <> p3;
per cases;
suppose
p1 = p3;
hence thesis by Th97;
end;
suppose
A2: p1 <> p3;
rng<*p1,p2,p3*> = {p1,p2,p3} by Lm2;
then p3 in rng<*p1,p2,p3*> by ENUMSET1:def 1;
hence Rotate(<*p1,p2,p3*>,p3) = (<*p1,p2,p3*>:-p3)^((<*p1,p2,p3*>-:p3)/^1)
by Def2
.= <*p3*>^((<*p1,p2,p3*>-:p3)/^1) by A1,A2,Th55
.= <*p3*>^(<*p1,p2,p3*>/^1) by A1,A2,Th51
.= <*p3*>^<*p2,p3*> by Th47
.= <*p3,p2,p3*> by FINSEQ_1:43;
end;
end;
theorem
for f being circular non trivial FinSequence of D holds rng(f/^1) = rng f
proof
let f be circular non trivial FinSequence of D;
thus rng(f/^1) c= rng f by FINSEQ_5:33;
let x be object;
f = <*f/.1*>^(f/^1) by FINSEQ_5:29;
then
A1: rng f = rng<*f/.1*> \/ rng(f/^1) by FINSEQ_1:31;
assume
A2: x in rng f;
per cases by A1,A2,XBOOLE_0:def 3;
suppose
x in rng<*f/.1*>;
then x in {f/.1} by FINSEQ_1:39;
then x = f/.1 by TARSKI:def 1;
then
A3: x = f/.len f by Def1;
A4: len f >= 1+1 by NAT_D:60;
then len f >= 1 by XXREAL_0:2;
then
A5: len(f/^1) = len f - 1 by RFINSEQ:def 1;
then 1 <= len(f/^1) by A4,XREAL_1:19;
then
A6: len(f/^1) in dom(f/^1) by FINSEQ_3:25;
len(f/^1) + 1 = len f by A5;
then x = (f/^1)/.len(f/^1) by A3,A6,FINSEQ_5:27;
hence thesis by A6,PARTFUN2:2;
end;
suppose
x in rng(f/^1);
hence thesis;
end;
end;
theorem Th101:
rng(f/^1) c= rng Rotate(f,p)
proof
per cases;
suppose
A1: p in rng f;
then Rotate(f,p) = (f:-p)^((f-:p)/^1) by Def2;
then
A2: rng Rotate(f,p) = rng(f:-p) \/ rng((f-:p)/^1) by FINSEQ_1:31;
thus thesis
proof
let x be object;
assume
A3: x in rng(f/^1);
A4: rng(f/^1) c= rng f by FINSEQ_5:33;
then
A5: x in rng f by A3;
per cases;
suppose that
A6: x..f < p..f and
A7: x..(f/^1) >= p..(f/^1);
A8: p..f >= 1 by A1,FINSEQ_4:21;
p..f <> 1 by A3,A4,A6,FINSEQ_4:21;
then p..f > 1 by A8,XXREAL_0:1;
then p..f = p..(f/^1) + 1 by A1,Th56;
then
A9: x..(f/^1)+1 >= p..f by A7,XREAL_1:6;
rng f c= D by FINSEQ_1:def 4;
then reconsider q = x as Element of D by A5;
A10: x..(f/^1) in dom(f/^1) by A3,FINSEQ_4:20;
f <> {} by A1;
then len f >= 1 by NAT_1:14;
then len f - 1 = len(f/^1) by RFINSEQ:def 1;
then
A11: len f = len(f/^1) + 1;
x..(f/^1) <= len(f/^1) by A3,FINSEQ_4:21;
then
A12: x..(f/^1)+1 <= len f by A11,XREAL_1:6;
q = (f/^1)/.(q..(f/^1)) by A3,FINSEQ_5:38
.= f/.(q..(f/^1)+1) by A10,FINSEQ_5:27;
then x in rng(f:-p) by A1,A12,A9,Th63;
hence thesis by A2,XBOOLE_0:def 3;
end;
suppose that
A13: x..f < p..f and
A14: x..(f/^1) <= p..(f/^1);
A15: p..f <> 1 by A3,A4,A13,FINSEQ_4:21;
p..f >= 1 by A1,FINSEQ_4:21;
then p..f > 1 by A15,XXREAL_0:1;
then p in rng(f/^1) by A1,Th57;
then x in rng((f/^1)-:p) by A3,A14,FINSEQ_5:46;
then x in rng((f-:p)/^1) by A1,A15,Th60;
hence thesis by A2,XBOOLE_0:def 3;
end;
suppose
x..f >= p..f;
then x in rng(f:-p) by A1,A3,A4,Th62;
hence thesis by A2,XBOOLE_0:def 3;
end;
end;
end;
suppose
not p in rng f;
then Rotate(f,p) = f by Def2;
hence thesis by FINSEQ_5:33;
end;
end;
theorem Th102:
p2 in rng f \ rng(f-:p1) implies Rotate(Rotate(f,p1),p2) = Rotate(f,p2)
proof
assume
A1: p2 in rng f \ rng(f-:p1);
per cases;
suppose
A2: p1 in rng f;
then
A3: Rotate(f,p1) = (f:-p1)^((f-:p1)/^1) by Def2;
A4: p1..(f:-p1) = 1 by Th79;
rng((f-:p1)/^1) c= rng(f-:p1) by FINSEQ_5:33;
then
A5: not p2 in rng((f-:p1)/^1) by A1,XBOOLE_0:def 5;
A6: rng(f/^1) c= rng Rotate(f,p1) by Th101;
A7: f-:p1 <> {} by A2,FINSEQ_5:47;
A8: not p2 in rng(f-:p1) by A1,XBOOLE_0:def 5;
p1..f <= p1..f;
then
A9: p1 <> p2 by A2,A8,FINSEQ_5:46;
rng f = rng(f-:p1) \/ rng(f:-p1) by A2,Th70;
then
A10: p2 in rng(f:-p1) by A1,A8,XBOOLE_0:def 3;
p1 in rng(f:-p1) by Th61;
then
A11: p2..(f:-p1) <> 1 by A10,A9,A4,FINSEQ_5:9;
then p2 in rng((f:-p1)/^1) by A10,Th78;
then
A12: p2 in rng((f:-p1)/^1)\rng((f-:p1)/^1) by A5,XBOOLE_0:def 5;
A13: now
assume p2..f = 1;
then p2..f <= p1..f by A2,FINSEQ_4:21;
hence contradiction by A1,A2,A8,FINSEQ_5:46;
end;
then p2 in rng(f/^1) by A1,Th78;
hence
Rotate(Rotate(f,p1),p2) = (((f:-p1)^((f-:p1)/^1)):-p2)^((((f:-p1)^((f
-:p1)/^1))-:p2)/^1) by A3,A6,Def2
.= (f:-p1:-p2)^((f-:p1)/^1)^((((f:-p1)^((f-:p1)/^1))-:p2)/^1) by A10,Th64
.= (f:-p2)^((f-:p1)/^1)^((((f:-p1)^((f-:p1)/^1))-:p2)/^1) by A1,A2,Th71
.= (f:-p2)^((f-:p1)/^1)^(((f:-p1)-:p2)/^1) by A10,Th66
.= (f:-p2)^((f-:p1)/^1)^(((f:-p1)/^1)-:p2) by A10,A11,Th60
.= (f:-p2)^(((f-:p1)/^1)^(((f:-p1)/^1)-:p2)) by FINSEQ_1:32
.= (f:-p2)^((((f-:p1)/^1)^((f:-p1)/^1))-:p2) by A12,Th67
.= (f:-p2)^((((f-:p1)^((f:-p1)/^1))/^1)-:p2) by A7,Th77
.= (f:-p2)^((f/^1)-:p2) by A2,Th76
.= (f:-p2)^((f-:p2)/^1) by A1,A13,Th60
.= Rotate(f,p2) by A1,Def2;
end;
suppose
not p1 in rng f;
hence thesis by Def2;
end;
end;
theorem Th103:
p2..f <> 1 & p2 in rng f \ rng(f:-p1) implies Rotate(Rotate(f,
p1),p2) = Rotate(f,p2)
proof
assume that
A1: p2..f <> 1 and
A2: p2 in rng f \ rng(f:-p1);
per cases;
suppose
A3: p1 in rng f;
then
A4: f-:p1 <> {} by FINSEQ_5:47;
A5: not p2 in rng(f:-p1) by A2,XBOOLE_0:def 5;
rng f = rng(f-:p1) \/ rng(f:-p1) by A3,Th70;
then
A6: p2 in rng(f-:p1) by A2,A5,XBOOLE_0:def 3;
(f-:p1)^((f:-p1)/^1) = f by A3,Th76;
then
A7: p2..(f-:p1) <> 1 by A1,A6,Th6;
then
A8: p2 in rng((f-:p1)/^1) by A6,Th78;
then
A9: p2 in rng((f-:p1)/^1) \ rng(f:-p1) by A5,XBOOLE_0:def 5;
A10: Rotate(f,p1) = (f:-p1)^((f-:p1)/^1) by A3,Def2;
then rng Rotate(f,p1) = rng(f:-p1) \/ rng((f-:p1)/^1) by FINSEQ_1:31;
then p2 in rng Rotate(f,p1) by A8,XBOOLE_0:def 3;
hence
Rotate(Rotate(f,p1),p2) = (((f:-p1)^((f-:p1)/^1)):-p2)^((((f:-p1)^((f
-:p1)/^1))-:p2)/^1) by A10,Def2
.= (((f-:p1)/^1):-p2)^((((f:-p1)^((f-:p1)/^1))-:p2)/^1) by A9,Th65
.= (((f-:p1)/^1):-p2)^(((f:-p1)^(((f-:p1)/^1)-:p2))/^1) by A9,Th67
.= (((f-:p1)/^1):-p2)^(((f:-p1)/^1)^(((f-:p1)/^1)-:p2)) by Th77
.= (((f-:p1)/^1):-p2)^((f:-p1)/^1)^(((f-:p1)/^1)-:p2) by FINSEQ_1:32
.= ((((f-:p1)/^1)^((f:-p1)/^1)):-p2)^(((f-:p1)/^1)-:p2) by A8,Th64
.= ((((f-:p1)^((f:-p1)/^1)/^1)):-p2)^(((f-:p1)/^1)-:p2) by A4,Th77
.= ((f/^1):-p2)^(((f-:p1)/^1)-:p2) by A3,Th76
.= (f:-p2)^(((f-:p1)/^1)-:p2) by A1,A2,Th83
.= (f:-p2)^((f-:p1-:p2)/^1) by A6,A7,Th60
.= (f:-p2)^((f-:p2)/^1) by A3,A6,Th75
.= Rotate(f,p2) by A2,Def2;
end;
suppose
not p1 in rng f;
hence thesis by Def2;
end;
end;
theorem Th104:
p2 in rng(f/^1) & f just_once_values p2 implies Rotate(Rotate(f
,p1),p2) = Rotate(f,p2)
proof
per cases;
suppose
A1: p1 in rng f;
assume that
A2: p2 in rng(f/^1) and
A3: f just_once_values p2;
f = (f -| p1) ^ <* p1 *> ^ (f |-- p1) by A1,FINSEQ_4:51;
then
A4: p2 in rng((f -| p1)^<* p1 *>) \+\ rng(f |-- p1) by A3,Th16;
A5: now
per cases by A4,XBOOLE_0:1;
case that
p2 in rng((f -| p1)^<* p1 *>) and
A6: not p2 in rng(f |-- p1);
now
per cases;
case
not p2 in rng<* p1 *>;
then not p2 in rng(f |-- p1) \/ rng<* p1 *> by A6,XBOOLE_0:def 3;
then not p2 in rng(<* p1 *>^(f |-- p1)) by FINSEQ_1:31;
hence not p2 in rng(f:-p1) by A1,Th41;
end;
case
p2 in rng<* p1 *>;
then p2 in { p1 } by FINSEQ_1:39;
hence p2 = p1 by TARSKI:def 1;
end;
end;
hence p2 in rng(f:-p1) implies p1 = p2;
end;
case
not p2 in rng((f -| p1)^<* p1 *>);
hence not p2 in rng(f-:p1) by A1,Th40;
end;
end;
A7: p2 in rng f by A3,FINSEQ_4:5;
then f = <*f/.1*>^(f/^1) by FINSEQ_5:29,RELAT_1:38;
then p2 in rng<*f/.1*> \+\ rng(f/^1) by A3,Th16;
then not p2 in rng<*f/.1*> by A2,XBOOLE_0:1;
then not p2 in {f/.1} by FINSEQ_1:39;
then p2 <> f/.1 by TARSKI:def 1;
then
A8: p2..f <> 1 by A7,FINSEQ_5:38;
now
per cases by A7,A5,XBOOLE_0:def 5;
suppose
p1 = p2;
hence thesis by Th93;
end;
suppose
p2 in rng f \ rng(f-:p1);
hence thesis by Th102;
end;
suppose
p2 in rng f \ rng(f:-p1);
hence thesis by A8,Th103;
end;
end;
hence thesis;
end;
suppose
not p1 in rng f;
hence thesis by Def2;
end;
end;
theorem
f is circular & f just_once_values p2 implies Rotate(Rotate(f,p1),p2)
= Rotate(f,p2)
proof
per cases;
suppose
A1: p1 in rng f;
assume that
A2: f is circular and
A3: f just_once_values p2;
A4: p2 in rng f by A3,FINSEQ_4:45;
now
per cases;
suppose
rng f is trivial;
then p1 = p2 by A1,A4,ZFMISC_1:def 10;
hence thesis by Th93;
end;
suppose
A5: rng f is not trivial;
then f = <*f/.1*>^(f/^1) by FINSEQ_5:29,RELAT_1:38;
then
A6: rng f = rng<*f/.1*> \/ rng(f/^1) by FINSEQ_1:31;
now
f qua set is non trivial by A5;
then len f >= 1 + 1 by NAT_D:60;
then
A7: 1 < len f by NAT_1:13;
assume
A8: not p2 in rng(f/^1);
then p2 in rng<*f/.1*> by A4,A6,XBOOLE_0:def 3;
then p2 in {f/.1} by FINSEQ_1:39;
then p2 = f/.1 by TARSKI:def 1;
then
A9: p2 = f/.len f by A2;
len f in dom f by A5,FINSEQ_5:6,RELAT_1:38;
hence contradiction by A8,A9,A7,Th58;
end;
hence thesis by A3,Th104;
end;
end;
hence thesis;
end;
suppose
not p1 in rng f;
hence thesis by Def2;
end;
end;
theorem
f is circular & f just_once_values p implies Rev Rotate(f,p) = Rotate(
Rev f,p)
proof
assume that
A1: f is circular and
A2: f just_once_values 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,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;
end;
begin :: Addenda
:: from AMISTD_1, 2007.07.26, A.T.
theorem
for f being trivial FinSequence of D holds f is empty or ex x being
Element of D st f = <*x*>
proof
let f be trivial FinSequence of D;
A1: rng f c= D by FINSEQ_1:def 4;
assume f is non empty;
then consider x being object such that
A2: f = {x} by ZFMISC_1:131;
A3: 1 in dom f by A2,FINSEQ_5:6;
A4: x in {x} by TARSKI:def 1;
then consider y, z being object such that
A5: x = [y,z] by A2,RELAT_1:def 1;
reconsider z as set by TARSKI:1;
take z;
z in rng f by A2,A4,A5,XTUPLE_0:def 13;
hence z is Element of D by A1;
dom f = {y} by A2,A5,RELAT_1:9;
then 1 = y by A3,TARSKI:def 1;
hence f = <*z*> by A2,A5,FINSEQ_1:def 5;
end;
begin :: from JORDAN3, 2010.02.25, A.T.
reserve D for non empty set;
theorem
for i be Nat for p,q being FinSequence st len p*).1=f.1 & (f^<*x*>).1=f/.1 & (<*x*>^f).(len f +1)=f.len f & (<*x*>^f).(len f
+1)=f/.len f
proof
let x be set,f be FinSequence of D;
assume
A1: 1<=len f;
then
A2: len f in dom f by FINSEQ_3:25;
1 in dom f by A1,FINSEQ_3:25;
then
A3: (f^<*x*>).1=f.1 by FINSEQ_1:def 7;
(<*x*>^f).(len f +1) =(<*x*>^f).(len <*x*>+len f) by FINSEQ_1:39
.=f.len f by A2,FINSEQ_1:def 7;
hence thesis by A1,A3,FINSEQ_4:15;
end;
theorem Th110:
for f being FinSequence st len f=1 holds Rev f=f
proof
let f be FinSequence;
assume len f=1;
then f=<*f.1*> by FINSEQ_1:40;
hence thesis by FINSEQ_5:60;
end;
theorem
for f being FinSequence of D,k being Nat holds len (f/^k)=len f-'k by
RFINSEQ:29;
definition
let f be FinSequence,k1,k2 be Nat;
func mid(f,k1,k2) -> FinSequence equals
:Def3:
(f/^(k1-'1))|(k2-'k1+1)
if k1<=k2 otherwise Rev ((f/^(k2-'1))|(k1-'k2+1));
correctness;
end;
definition
let D;
let f be FinSequence of D,k1,k2 be Nat;
redefine func mid(f,k1,k2) -> FinSequence of D;
coherence
proof
mid(f,k1,k2) = (f/^(k1-'1))|(k2-'k1+1) or
mid(f,k1,k2) = Rev ((f/^(k2-'1))|(k1-'k2+1)) by Def3;
hence thesis;
end;
end;
::$CT
theorem
for f being FinSequence of D,k1,k2 being Nat st 1<=k1
& k1<=len f & 1<=k2 & k2<=len f holds Rev mid(f,k1,k2)=mid(Rev f,len f-'k2+1,
len f-'k1+1)
proof
let f be FinSequence of D,k1,k2 be Nat;
assume that
A1: 1<=k1 and
A2: k1<=len f and
A3: 1<=k2 and
A4: k2<=len f;
per cases;
suppose
A5: k1<=k2;
A6: len f-'(k1-'1)=len f-(k1-'1) by A2,NAT_D:50,XREAL_1:233
.=len f-(k1-1) by A1,XREAL_1:233
.=len f-k1+1
.=len f-'k1+1 by A2,XREAL_1:233;
A7: len f-'k1=len f-k1 by A2,XREAL_1:233;
A8: len f-'k2=len f-k2 by A4,XREAL_1:233;
k2-k1<=len f-k1 by A4,XREAL_1:9;
then k2-'k1<=len f-k1 by A5,XREAL_1:233;
then k2-'k1<=len f-'k1 by A2,XREAL_1:233;
then k2-'k1+1<=len f-'k1+1 by XREAL_1:6;
then
A9: (len f-'(k1-'1)-'(k2-'k1+1)) =(len f-'k1+1)-(k2-'k1+1) by A6,XREAL_1:233
.=(len f-k1+1)-(k2-k1+1) by A5,A7,XREAL_1:233
.=len f+1-1-k2
.=len f-'k2 by A4,XREAL_1:233;
then
A10: (len (f/^(k1-'1))-'(k2-'k1+1))+(k2-'k1+1) =len f-'k2+(k2-'k1+1) by
RFINSEQ:29
.=len f-k2+(k2-k1+1) by A5,A8,XREAL_1:233
.=len f-(k1-1)
.=len f-(k1-'1) by A1,XREAL_1:233
.=len f-'(k1-'1) by A2,NAT_D:50,XREAL_1:233
.=len (f/^(k1-'1)) by RFINSEQ:29;
A11: len f-'k1<=len f-'k1+1 by NAT_1:11;
len f-'k1>=len f-'k2 by A5,NAT_D:41;
then
A12: len f-'(k1-'1)-'(len f-'k2) =len f-'k1+1-(len f-'k2) by A6,A11,XREAL_1:233
,XXREAL_0:2
.=len f-k1+1-(len f-k2) by A4,A7,XREAL_1:233
.=k2-k1+1
.=k2-'k1+1 by A5,XREAL_1:233;
A13: (len f-'(k1-'1))+(k1-'1) =(len f-(k1-'1))+(k1-'1) by A2,NAT_D:50
,XREAL_1:233
.=len f;
len f-'k1>=len f-'k2 by A5,NAT_D:41;
then len f-'k1+1>=len f-'k2+1 by XREAL_1:6;
then
A14: (len f-'k1+1)-'(len f-'k2+1)+1 =(len f-'k1+1)-(len f-'k2+1)+1 by
XREAL_1:233
.=(len f-k1+1)-(len f-k2+1)+1 by A4,A7,XREAL_1:233
.=k2-k1+1
.=k2-'k1+1 by A5,XREAL_1:233;
len f-'k1>=len f-'k2 by A5,NAT_D:41;
then len f-'k1+1>=len f-'k2+1 by XREAL_1:6;
then mid(Rev f,len f-'k2+1,len f-'k1+1) =(((Rev f)/^((len f-'k2+1)-'1))|(
k2-'k1+1)) by A14,Def3
.=(Rev f/^(len f-'k2))|(len f-'(k1-'1)-'(len f-'k2)) by A12,NAT_D:34
.=(Rev f|(len f-'(k1-'1)))/^(len f-'k2) by FINSEQ_5:80
.=(Rev f|(len f-'(k1-'1)))/^(len (f/^(k1-'1))-'(k2-'k1+1)) by A9,
RFINSEQ:29
.=(Rev (f/^(k1-'1)))/^(len (f/^(k1-'1))-'(k2-'k1+1)) by A13,Th84
.=Rev (((f/^(k1-'1))|(k2-'k1+1))) by A10,Th85
.=Rev mid(f,k1,k2) by A5,Def3;
hence thesis;
end;
suppose
A15: k1>k2;
A16: len f-'(k2-'1)=len f-(k2-'1) by A4,NAT_D:50,XREAL_1:233
.=len f-(k2-1) by A3,XREAL_1:233
.=len f-k2+1
.=len f-'k2+1 by A4,XREAL_1:233;
A17: len f-'k2=len f-k2 by A4,XREAL_1:233;
len f-'k2>=len f-'k1 by A15,NAT_D:41;
then len f-'k2+1>=len f-'k1+1 by XREAL_1:6;
then
A18: (len f-'k2+1)-'(len f-'k1+1)+1 =(len f-'k2+1)-(len f-'k1+1)+1 by
XREAL_1:233
.=(len f-k2+1)-(len f-k1+1)+1 by A2,A17,XREAL_1:233
.=k1-k2+1
.=k1-'k2+1 by A15,XREAL_1:233;
A19: len f-'k1=len f-k1 by A2,XREAL_1:233;
A20: len f-'k2<=len f-'k2+1 by NAT_1:11;
len f-'k2>=len f-'k1 by A15,NAT_D:41;
then
A21: len f-'(k2-'1)-'(len f-'k1) =len f-'k2+1-(len f-'k1) by A16,A20,
XREAL_1:233,XXREAL_0:2
.=len f-k2+1-(len f-k1) by A2,A17,XREAL_1:233
.=k1-k2+1
.=k1-'k2+1 by A15,XREAL_1:233;
A22: (len f-'(k2-'1))+(k2-'1) =(len f-(k2-'1))+(k2-'1) by A4,NAT_D:50
,XREAL_1:233
.=len f;
k1-k2<=len f-k2 by A2,XREAL_1:9;
then k1-'k2<=len f-k2 by A15,XREAL_1:233;
then k1-'k2<=len f-'k2 by A4,XREAL_1:233;
then k1-'k2+1<=len f-'k2+1 by XREAL_1:6;
then
A23: (len f-'(k2-'1)-'(k1-'k2+1)) =(len f-'k2+1)-(k1-'k2+1) by A16,XREAL_1:233
.=(len f-k2+1)-(k1-k2+1) by A15,A17,XREAL_1:233
.=len f+1-1-k1
.=len f-'k1 by A2,XREAL_1:233;
then
A24: (len (f/^(k2-'1))-'(k1-'k2+1))+(k1-'k2+1) =len f-'k1+(k1-'k2+1) by
RFINSEQ:29
.=len f-k1+(k1-k2+1) by A15,A19,XREAL_1:233
.=len f-(k2-1)
.=len f-(k2-'1) by A3,XREAL_1:233
.=len f-'(k2-'1) by A4,NAT_D:50,XREAL_1:233
.=len (f/^(k2-'1)) by RFINSEQ:29;
len f-k2>len f-k1 by A15,XREAL_1:10;
then len f-'k2+1>len f-'k1+1 by A17,A19,XREAL_1:6;
then
mid(Rev f,len f-'k2+1,len f-'k1+1) =Rev((((Rev f)/^((len f-'k1+1)-'1)
)|(k1-'k2+1))) by A18,Def3
.=Rev((Rev f/^(len f-'k1))|(len f-'(k2-'1)-'(len f-'k1))) by A21,NAT_D:34
.=Rev((Rev f|(len f-'(k2-'1)))/^(len f-'k1)) by FINSEQ_5:80
.=Rev((Rev f|(len f-'(k2-'1)))/^(len (f/^(k2-'1))-'(k1-'k2+1))) by A23,
RFINSEQ:29
.=Rev((Rev (f/^(k2-'1)))/^(len (f/^(k2-'1))-'(k1-'k2+1))) by A22,Th84
.=Rev(Rev (((f/^(k2-'1))|(k1-'k2+1)))) by A24,Th85
.= Rev mid(f,k1,k2) by A15,Def3;
hence thesis;
end;
end;
theorem Th113:
for n,m being Nat,f being FinSequence of D st 1<= m &
m+n<=len f holds (f/^n).m=f.(m+n)
proof
let n,m be Nat,f be FinSequence of D;
assume that
A1: 1<= m and
A2: m+n<=len f;
A3: m+n-n<=len f -n by A2,XREAL_1:9;
n<=n+m by NAT_1:11;
then
A4: n<=len f by A2,XXREAL_0:2;
then len (f/^n) = len f -n by RFINSEQ:def 1;
then m in dom (f/^n) by A1,A3,FINSEQ_3:25;
hence thesis by A4,RFINSEQ:def 1;
end;
theorem Th114:
for i being Nat,f being FinSequence of D st 1<=i & i
<=len f holds (Rev f).i=f.(len f -i+1)
proof
let i be Nat,f be FinSequence of D;
assume that
A1: 1<=i and
A2: i<=len f;
i in dom (f) by A1,A2,FINSEQ_3:25;
hence thesis by FINSEQ_5:58;
end;
theorem
for f being FinSequence of D,k being Nat st 1<=k holds mid(f,1,k)=f|k
proof
let f be FinSequence of D,k be Nat;
1-'1=0 by XREAL_1:232;
then
A1: f/^(1-'1)=f by FINSEQ_5:28;
assume
A2: 1<=k;
then mid(f,1,k)=(f/^(1-'1))|(k-'1+1) by Def3;
hence thesis by A2,A1,XREAL_1:235;
end;
theorem
for f being FinSequence of D,k being Nat st k<=len f
holds mid(f,k,len f)=f/^(k-'1)
proof
let f be FinSequence of D,k be Nat;
assume
A1: k<=len f;
then
A2: mid(f,k,len f)=(f/^(k-'1))|(len f-'k+1) by Def3;
k-'1<=len f by A1,NAT_D:44;
then
A3: len (f/^(k-'1))=len f-(k-'1) by RFINSEQ:def 1;
A4: len f-'k+1=len f-k+1 by A1,XREAL_1:233
.=len f -(k-1);
now
per cases;
case
A5: k=0;
0-1<0;
then k-'1=0 by A5,XREAL_0:def 2;
then
A6: f/^(k-'1)=f by FINSEQ_5:28;
len f-'k+1=len f +1 by A5,NAT_D:40;
then len f <= len f-'k+1 by NAT_1:11;
then Seg len f c= Seg (len f -'k+1) by FINSEQ_1:5;
then dom (f/^(k-'1)) c= Seg (len f -'k+1) by A6,FINSEQ_1:def 3;
then (f/^(k-'1))|Seg (len f -'k+1)= f/^(k-'1) by RELAT_1:68;
hence thesis by A2,FINSEQ_1:def 15;
end;
case
k<>0;
then 0+1<=k by NAT_1:13;
then len (f/^(k-'1))=len f-'k+1 by A3,A4,XREAL_1:233;
hence mid(f,k,len f)=(f/^(k-'1))|Seg len (f/^(k-'1)) by A2,
FINSEQ_1:def 15
.=(f/^(k-'1))|dom (f/^(k-'1)) by FINSEQ_1:def 3
.=(f/^(k-'1));
end;
end;
hence thesis;
end;
theorem Th117:
for f being FinSequence of D,k1,k2 being Nat st 1<=k1
& k1<=len f & 1<=k2 & k2<=len f holds mid(f,k1,k2).1=f.k1 & (k1<=k2 implies len
mid(f,k1,k2) = k2 -' k1 +1 & for i being Nat st 1<=i & i<=len mid(f,
k1,k2) holds mid(f,k1,k2).i=f.(i+k1-'1)) & (k1>k2 implies len mid(f,k1,k2) = k1
-' k2 +1 & for i being Nat st 1<=i & i<=len mid(f,k1,k2) holds mid(f
,k1,k2).i=f.(k1-'i+1))
proof
let f be FinSequence of D,k11,k21 be Nat;
assume that
A1: 1<=k11 and
A2: k11<=len f and
A3: 1<=k21 and
A4: k21<=len f;
k21-'1<=len f by A4,NAT_D:44;
then
A5: len (f/^(k21-'1))=len f -(k21-'1) by RFINSEQ:def 1;
A6: k21-1>=0 by A3,XREAL_1:48;
then
A7: k21-'1=k21-1 by XREAL_0:def 2;
A8: now
let k1,k2 be Nat;
now
assume that
A9: k1<=k2 and
A10: 1<=k1 and
A11: k1<=len f;
A12: mid(f,k1,k2).1=((f/^(k1-'1))|(k2-'k1+1)).1 by A9,Def3
.=((f/^(k1-'1))|(Seg (k2-'k1+1))).1 by FINSEQ_1:def 15;
k1-1>=0 by A10,XREAL_1:48;
then
A13: 1+(k1-'1)=1+(k1-1) by XREAL_0:def 2
.=k1;
then 1+(k1-'1)<=len f -(k1-'1)+(k1-'1) by A11;
then
A14: 1<=len f - (k1-'1) by XREAL_1:6;
A15: k1-'1<=len f by A11,NAT_D:44;
then len (f/^(k1-'1))=len f -(k1-'1) by RFINSEQ:def 1;
then 1 in Seg(len (f/^(k1-'1))) by A14,FINSEQ_1:1;
then
A16: 1 in dom (f/^(k1-'1)) by FINSEQ_1:def 3;
0+1<=k2-'k1+1 by XREAL_1:6;
then 1 in Seg(k2-'k1+1) by FINSEQ_1:1;
then 1 in dom (f/^(k1-'1)) /\ Seg(k2-'k1+1) by A16,XBOOLE_0:def 4;
then 1 in dom ((f/^(k1-'1))|(Seg (k2-'k1+1))) by RELAT_1:61;
then mid(f,k1,k2).1=(f/^(k1-'1)).1 by A12,FUNCT_1:47;
hence mid(f,k1,k2).1=f.k1 by A13,A15,A16,RFINSEQ:def 1;
end;
hence k1<=k2 & 1<=k1 & k1<=len f implies mid(f,k1,k2).1=f.k1;
end;
thus mid(f,k11,k21).1=f.k11
proof
per cases;
suppose
k11<=k21;
hence thesis by A1,A2,A8;
end;
suppose
A17: k11>k21;
A18: k21-1>=0 by A3,XREAL_1:48;
A19: k11-k21>=0 by A17,XREAL_1:48;
then k11-'k21=k11-k21 by XREAL_0:def 2;
then
A20: k21-'1 +(k11-'k21+1)= k21-1+(k11-(k21-1)) by A18,XREAL_0:def 2
.=k11;
k21-'1<=len f by A4,NAT_D:44;
then
A21: len (f/^(k21-'1))=len f -(k21-'1) by RFINSEQ:def 1;
A22: 1<=(k11-'k21+1) by NAT_1:11;
k11-'k21+1=k11-k21+1 by A19,XREAL_0:def 2
.=k11-(k21-1)
.=k11-(k21-'1) by A18,XREAL_0:def 2;
then
A23: k11-'k21+1 <=len (f/^(k21-'1)) by A2,A21,XREAL_1:9;
then
A24: len ((f/^(k21-'1))|(k11-'k21+1))=(k11-'k21+1) by FINSEQ_1:59;
then
A25: k11-'k21+1 in dom ((f/^(k21-'1))|(k11-'k21+1)) by A22,FINSEQ_3:25;
A26: k11-'k21+1 in dom (f/^(k21-'1)) by A22,A23,FINSEQ_3:25;
A27: ((f/^(k21-'1))|(k11-'k21+1)).len ((f/^(k21-'1))|(k11-'k21+1)) =((f
/^(k21-'1))|(k11-'k21+1))/.(k11-'k21+1) by A22,A24,FINSEQ_4:15
.=(f/^(k21-'1))/.(k11-'k21+1) by A25,FINSEQ_4:70
.=f/.((k21-'1 +(k11-'k21+1))) by A26,FINSEQ_5:27
.=f.k11 by A1,A2,A20,FINSEQ_4:15;
1 in dom ((f/^(k21-'1))|(k11-'k21+1)) by A22,A24,FINSEQ_3:25;
then
(Rev ((f/^(k21-'1))|(k11-'k21+1))).1 = ((f/^(k21-'1))|(k11-'k21+1))
.(len ((f/^(k21-'1))|(k11-'k21+1)) - 1 + 1) by FINSEQ_5:58
.= f.k11 by A27;
hence thesis by A17,Def3;
end;
end;
thus k11<=k21 implies len mid(f,k11,k21) = k21 -' k11 +1 & for i being
Nat st 1<=i & i<=len mid(f,k11,k21) holds mid(f,k11,k21).i=f.(i+k11
-'1)
proof
A28: k11-1>=0 by A1,XREAL_1:48;
then
A29: k11-'1=k11-1 by XREAL_0:def 2;
k11-'1<=len f by A2,NAT_D:44;
then
A30: len (f/^(k11-'1))=len f -(k11-'1) by RFINSEQ:def 1;
assume
A31: k11<=k21;
then
A32: mid(f,k11,k21)=(f/^(k11-'1))|(k21-'k11+1) by Def3;
A33: k21-k11>=0 by A31,XREAL_1:48;
then
A34: k21-'k11=k21-k11 by XREAL_0:def 2;
k21-'k11+1=k21-k11+1 by A33,XREAL_0:def 2
.=k21-(k11-1)
.=k21-(k11-'1) by A28,XREAL_0:def 2;
then
A35: k21-'k11+1 <=len (f/^(k11-'1)) by A4,A30,XREAL_1:9;
then
A36: len ((f/^(k11-'1))|(k21-'k11+1))=(k21-'k11+1) by FINSEQ_1:59;
for i being Nat st 1<=i & i<=len mid(f,k11,k21) holds mid(
f,k11,k21).i=f.(i+k11-'1)
proof
let i be Nat;
assume that
A37: 1<=i and
A38: i<=len mid(f,k11,k21);
A39: i<= (k21-'k11+1) by A32,A35,A38,FINSEQ_1:59;
i+(k11-1)<=k21-(k11-1)+(k11-1) by A32,A34,A36,A38,XREAL_1:6;
then
A40: i+(k11-'1)<=len f by A4,A29,XXREAL_0:2;
A41: k11<=k11+i by NAT_1:11;
A42: i+(k11-'1)=i+(k11-1) by A28,XREAL_0:def 2
.=i+k11-1
.=i+k11-'1 by A1,A41,XREAL_1:233,XXREAL_0:2;
mid(f,k11,k21).i=(f/^(k11-'1))|(k21-'k11+1).i by A31,Def3
.=(f/^(k11-'1)).i by A39,FINSEQ_3:112
.=f.(i+(k11-'1)) by A37,A40,Th113;
hence thesis by A42;
end;
hence thesis by A32,A35,FINSEQ_1:59;
end;
assume
A43: k11>k21;
then
A44: k11-k21>=0 by XREAL_1:48;
then
A45: k11-'k21=k11-k21 by XREAL_0:def 2;
A46: mid(f,k11,k21)=Rev ((f/^(k21-'1))|(k11-'k21+1)) by A43,Def3;
then
A47: len mid(f,k11,k21)=len ((f/^(k21-'1))|(k11-'k21+1)) by FINSEQ_5:def 3;
k11-'k21+1=k11-k21+1 by A44,XREAL_0:def 2
.=k11-(k21-1)
.=k11-(k21-'1) by A6,XREAL_0:def 2;
then
A48: k11-'k21+1 <=len (f/^(k21-'1)) by A2,A5,XREAL_1:9;
hence
A49: len mid(f,k11,k21) = k11 -' k21 +1 by A47,FINSEQ_1:59;
A50: len ((f/^(k21-'1))|(k11-'k21+1))=(k11-'k21+1) by A48,FINSEQ_1:59;
thus for i being Nat st 1<=i & i<=len mid(f,k11,k21) holds mid(f,
k11,k21).i=f.(k11-'i+1)
proof
let i be Nat;
assume that
A51: 1<=i and
A52: i<=len mid(f,k11,k21);
A53: i+(k21-1)<=k11-(k21-1)+(k21-1) by A45,A49,A52,XREAL_1:6;
k11-'k21+1<= k11-'k21+1+(i-'1) by NAT_1:11;
then k11-'k21+1<= k11-'k21+1+(i-1) by A51,XREAL_1:233;
then k11-'k21+1-(i-1)<= k11-'k21+1+(i-1)-(i-1) by XREAL_1:9;
then
A54: k11-'k21+1-i+1<= k11-'k21+1;
i<=k11-'k21+1 by A47,A48,A52,FINSEQ_1:59;
then
A55: (k11-'k21+1-'i+1)<=(k11-'k21+1) by A54,XREAL_1:233;
A56: i+k11<=i+len f by A2,XREAL_1:6;
A57: i<=i+(k21-'1) by NAT_1:11;
A58: k11-'k21+1-'i+1+(k21-'1) =k11-'k21+1-i+1+(k21-'1) by A49,A52,XREAL_1:233
.= k11-(k21-1)-i+1+(k21-1) by A6,A45,XREAL_0:def 2
.=k11-i+1
.=k11-'i+1 by A7,A53,A57,XREAL_1:233,XXREAL_0:2;
1+k11<=i+k11 by A51,XREAL_1:6;
then 1+k11<=i+len f by A56,XXREAL_0:2;
then 1+k11-i<=i+len f -i by XREAL_1:9;
then k11-i+1<=len f;
then
A59: k11-'k21+1-'i+1+(k21-'1)<= len f by A7,A53,A57,A58,XREAL_1:233,XXREAL_0:2;
mid(f,k11,k21).i=((f/^(k21-'1))|(k11-'k21+1)) .(len ((f/^(k21-'1))|(
k11-'k21+1)) -i+1) by A46,A47,A51,A52,Th114
.=((f/^(k21-'1))|(k11-'k21+1)) .(len ((f/^(k21-'1))|(k11-'k21+1)) -'i+
1) by A47,A52,XREAL_1:233
.=(f/^(k21-'1)).(k11-'k21+1-'i+1) by A50,A55,FINSEQ_3:112
.=f.(k11-'i+1) by A58,A59,Th113,NAT_1:11;
hence thesis;
end;
end;
theorem
for f being FinSequence of D,k1,k2 being Nat holds
rng mid(f,k1,k2) c= rng f
proof
let f be FinSequence of D,k1,k2 be Nat;
per cases;
suppose
k1<=k2;
then mid(f,k1,k2) = (f/^(k1-'1))|(k2-'k1+1) by Def3;
then
A1: rng mid(f,k1,k2) c= rng (f/^(k1-'1)) by FINSEQ_5:19;
rng (f/^(k1-'1)) c= rng f by FINSEQ_5:33;
hence thesis by A1;
end;
suppose
k1>k2;
then mid(f,k1,k2) = Rev ((f/^(k2-'1))|(k1-'k2+1)) by Def3;
then rng mid(f,k1,k2) = rng ((f/^(k2-'1))|(k1-'k2+1)) by FINSEQ_5:57;
then
A2: rng mid(f,k1,k2) c= rng (f/^(k2-'1)) by FINSEQ_5:19;
rng (f/^(k2-'1)) c= rng f by FINSEQ_5:33;
hence thesis by A2;
end;
end;
theorem
for f being FinSequence of D st 1<=len f holds mid(f,1,len f)=f
proof
let f be FinSequence of D;
assume
A1: 1<=len f;
then mid(f,1,len f)=(f/^(1-'1))|(len f-'1+1) by Def3
.=(f/^0)|(len f-'1+1) by XREAL_1:232
.=f|(len f-'1+1) by FINSEQ_5:28
.=f|len f by A1,XREAL_1:235
.=f by FINSEQ_1:58;
hence thesis;
end;
theorem
for f being FinSequence of D st 1<=len f holds mid(f,len f,1)=Rev f
proof
let f be FinSequence of D;
assume
A1: 1<=len f;
A2: 1-'1=0 by XREAL_1:232;
per cases;
suppose
len f<>1;
then 1=1+k1 by A4,XREAL_1:6;
then
A7: i+k1-1>=1+k1-1 by XREAL_1:9;
A8: i<=k2-k1+1 implies i<=k2-'k1+1 by A2,XREAL_1:233;
i-1>=1-1 by A4,XREAL_1:9;
then
A9: i-'1+k1=i-1+k1 by XREAL_0:def 2
.=i+k1-'1 by A7,XREAL_0:def 2;
A10: 1<=k2 by A1,A2,XXREAL_0:2;
then len mid(f,k1,k2)=k2-'k1+1 by A1,A2,A3,A6,Th117;
hence
A11: mid(f,k1,k2).i=f.(i+k1-'1) & mid(f,k1,k2).i=f.(i-'1+k1) by A1,A2,A3,A4,A5
,A10,A6,A8,A9,Th117;
hence mid(f,k1,k2).i=f.(i+k1-1) by A7,XREAL_0:def 2;
thus thesis by A4,A11,XREAL_1:233;
end;
theorem
for f being FinSequence of D,k,i being Nat st 1<=i & i<=k & k<=
len f holds mid(f,1,k).i=f.i
proof
let f be FinSequence of D,k,i be Nat;
assume that
A1: 1<=i and
A2: i<=k and
A3: k<=len f;
A4: i<=k-1+1 by A2;
1<=k by A1,A2,XXREAL_0:2;
then mid(f,1,k).i=f.(i+1-'1) by A1,A3,A4,Th121;
hence thesis by NAT_D:34;
end;
theorem
for f being FinSequence of D, k1,k2 being Nat st 1<=k1 & k1
<=k2 & k2<=len f holds len mid(f,k1,k2)<=len f
proof
let f be FinSequence of D, k1,k2 be Nat;
assume that
A1: 1<=k1 and
A2: k1<=k2 and
A3: k2<=len f;
A4: k1<=len f by A2,A3,XXREAL_0:2;
k2-k1>=0 by A2,XREAL_1:48;
then
A5: k2-'k1+1=k2-k1+1 by XREAL_0:def 2
.=k2-(k1-1);
k2<=k2+(k1-'1) by NAT_1:11;
then
A6: k2-(k1-'1)<=k2+(k1-'1)-(k1-'1) by XREAL_1:9;
k1-1>=0 by A1,XREAL_1:48;
then
A7: k1-1=k1-'1 by XREAL_0:def 2;
1<=k2 by A1,A2,XXREAL_0:2;
then len mid(f,k1,k2)=k2-'k1+1 by A1,A2,A3,A4,Th117;
hence thesis by A3,A5,A7,A6,XXREAL_0:2;
end;
theorem Th124:
for D for f being FinSequence of D, k being Nat, p
being Element of D holds (<*p*>^f)|(k+1) = <*p*>^(f|k)
proof
let D;
let f be FinSequence of D, k be Nat, p be Element of D;
A1: f|Seg k = f|k by FINSEQ_1:def 15;
thus (<*p*>^f)|(k+1) = (<*p*>^f)|Seg(k+1) by FINSEQ_1:def 15
.= (<*p*>^f)|Seg(k+len<*p*>) by FINSEQ_1:39
.= <*p*>^(f|k) by A1,Th14;
end;
theorem
for D for f being FinSequence of D, k1,k2 being Nat
st k1 < k2 & k1 in dom f holds mid(f,k1,k2) = <*f.k1*>^ mid(f,k1+1,k2)
proof
let D;
let f be FinSequence of D, k1,k2 be Nat;
assume
A1: k1 < k2;
then
A2: k1+1 <= k2 by NAT_1:13;
A3: 1 <= k2 -' k1
proof
per cases by A2,XXREAL_0:1;
suppose
k1 + 1 = k2;
hence thesis by NAT_D:34;
end;
suppose
A4: k1 + 1 < k2;
k2-'k1 <= 1 implies k2 <= 1 + k1
proof
assume k2-'k1 <= 1;
then k2-'k1 +k1 <= 1 + k1 by XREAL_1:6;
hence thesis by A1,XREAL_1:235;
end;
hence thesis by A4;
end;
end;
then k2-'k1 = k2-k1 by NAT_D:39;
then
A5: k2-'k1-'1 = k2-k1-1 by A3,XREAL_1:233
.= k2-(k1+1)
.= k2-'(k1+1) by A2,XREAL_1:233;
assume
A6: k1 in dom f;
then
A7: f.k1 = f/.k1 by PARTFUN1:def 6;
1 <= k1 by A6,FINSEQ_3:25;
then k1 -' 1 + 1 = k1 by XREAL_1:235;
then (f/^(k1-'1)) = <*f/.k1*>^(f/^k1) by A6,FINSEQ_5:31;
hence mid(f,k1,k2) = (<*f/.k1*>^ (f/^k1))|(k2-'k1+1) by A1,Def3
.= <*f.k1*>^ ((f/^k1)|(k2-'k1)) by A7,Th124
.= <*f.k1*>^ ((f/^k1)|(k2-'(k1+1)+1)) by A3,A5,XREAL_1:235
.= <*f.k1*>^ ((f/^(k1+1-'1))|(k2-'(k1+1)+1)) by NAT_D:34
.= <*f.k1*>^ mid(f,k1+1,k2) by A2,Def3;
end;
*