:: On the Decomposition of Finite Sequences
:: by Andrzej Trybulec
::
:: Received May 24, 1995
:: Copyright (c) 1995-2026 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, INT_1, FINSET_1,
GRAPH_2, ORDINAL1, FUNCT_4, FUNCT_7, NUMBER09;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
FINSET_1, XCMPLX_0, XXREAL_0, XXREAL_2, FUNCT_4, ZFMISC_1, REAL_1, INT_1,
NAT_1, NAT_D, RELAT_1, FUNCT_7, 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, CARD_1, WELLORD2, FUNCT_4,
MEMBERED, XXREAL_2, FUNCT_7;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, INT_1, FINSEQ_1, FINSEQ_5,
ORDINAL1, NAT_1, CARD_1, XXREAL_0, FINSET_1, VALUED_0, NUMBERS, MEMBERED,
XXREAL_2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, FINSEQ_1, SEQM_3;
equalities FINSEQ_1;
expansions TARSKI, XBOOLE_0, FINSEQ_1, SEQM_3;
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, ORDINAL1, CARD_1, CARD_2, XCMPLX_1, XXREAL_2, MEMBERED,
FUNCT_7, SUBSET_1;
schemes NAT_1, FINSEQ_1;
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
thus 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
thus 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 included_in_Seg set st 1 in X holds (Sgm X).1 = 1
proof
let X be included_in_Seg set such that
A2: 1 in X;
Sgm X <> {} by 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;
reconsider k1 = (Sgm X).1 as Nat;
assume
A4: (Sgm X).1 <> 1;
A5: rng Sgm X = X by FINSEQ_1:def 14;
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;
ex k being Nat st X c= Seg k by FINSEQ_1:def 13;
then
A8: k1 >= 1 by 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 A7,A8,A9,FINSEQ_1:def 14;
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;
then
A3: f.1 = <*p1,p2*>.1 by FUNCT_1:47
.= p1;
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;
then
A3: f.1 = <*p1,p2,p3*>.1 by FUNCT_1:47
.= p1;
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;
1 in dom f by A5,FINSEQ_3:25;
then f.1 = <*p1,p2,p3*>.1 by FUNCT_1:47
.= p1;
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;
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;
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;
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*>;
thus 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;
thus thesis by A2,A1,Th2;
end;
theorem Th20:
p1 <> p2 implies p2..<*p1,p2*> = 2
proof
A2: <*p1,p2*>.1 = p1;
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,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 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;
thus thesis by A2,A1,Th2;
end;
theorem Th22:
p1 <> p2 implies p2..<*p1,p2,p3*> = 2
proof
A2: <*p1,p2,p3*>.1 = p1;
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,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 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;
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,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 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
.= <*x,y*>.(k + x..<*x,y*>) by A1,A4;
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
.= <*x,y,z*>.(k + y..<*x,y,z*>) by A1,A4;
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
.= <*x,y,z*>.(k + x..<*x,y,z*>) by A1,A6;
end;
suppose
A7: k = 2;
hence <*y,z*>.k = z
.= <*x,y,z*>.(k + x..<*x,y,z*>) by A1,A7;
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 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 f"{f/.1} c= Seg len f by FINSEQ_1:def 3;
then
A3: f"{f/.1} is included_in_Seg;
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;
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;
hence thesis by A1,FINSEQ_1:33;
end;
theorem Th46:
<*p1,p2*>/^1 = <*p2*> by Th45;
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;
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;
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*>;
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;
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;
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
f|i|i = f|i;
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 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;
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;
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 :Def1A:
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*>;
thus <*d*> is circular by FINSEQ_1:39;
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 Th90:
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:-p)/.len(f:-p) by A2,FINSEQ_5:54,A1,A9,A10;
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;
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;
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;
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 Def1A;
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;
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<i & (i<=len p + len q or i<=len (p^q)) holds
(p^q).i=q.(i-len p)
proof
let i be Nat;
let p,q be FinSequence;
assume that
A1: len p<i and
A2: i<=len p +len q or i<=len (p^q);
i<=len p + len q by A2,FINSEQ_1:22;
then
A3: i-len p<=len p+len q -len p by XREAL_1:9;
len p +1<=i by A1,NAT_1:13;
then
A4: len p +1-len p<=i-len p by XREAL_1:9;
then
A5: len p+(i-'len p)=len p+(i-len p) by XREAL_0:def 2
.=i;
i-len p=i-'len p by A4,XREAL_0:def 2;
then i-'len p in dom q by A4,A3,FINSEQ_3:25;
hence thesis by A5,FINSEQ_1:def 7;
end;
theorem
for x being set,f being FinSequence of D st 1<=len f holds
(f^<*x*>).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; :: redefines mid (FINSEQ_6, definition)
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 st
1<= m & m+n<=len f holds (f/^n).m=f.(m+n)
proof
let n,m be Nat,f be FinSequence;
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 st
1<=i & i<=len f holds (Rev f).i=f.(len f -i+1)
proof
let i be Nat,f be FinSequence;
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, k being Nat st 1<=k holds mid(f,1,k)=f|k
proof
let f be FinSequence,k be Nat;
1-'1=0 by XREAL_1:232;
then
A1: f/^(1-'1)=f;
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,k being Nat st k<=len f
holds mid(f,k,len f)=f/^(k-'1)
proof
let f be FinSequence,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;
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;
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
.=(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,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,k11,k21 be Nat;
assume that
A1: 1<=k11 and
A2: k11<=len f and
A3: 1<=k21 and
A4: k21<=len f;
reconsider fa = f as FinSequence of rng f by FINSEQ_1:def 4;
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;
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;
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);
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;
a25: k11-'k21+1 in dom (f/^(k21-'1)) by A23,FINSEQ_3:25,A22;
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)) =
((fa/^(k21-'1))|(k11-'k21+1))/.(k11-'k21+1) by A22,A24,FINSEQ_4:15
.=(fa/^(k21-'1))/.(k11-'k21+1) by A25,FINSEQ_4:70
.=(f/^(k21-'1)).(k11-'k21+1) by a25,PARTFUN1:def 6
.=f.k11 by A20,A26,FINSEQ_5:27;
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,k1,k2 being Nat holds
rng mid(f,k1,k2) c= rng f
proof
let f be FinSequence,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 st 1<=len f holds mid(f,1,len f)=f
proof
let f be FinSequence;
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)
.=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<len f by A1,XXREAL_0:1;
then mid(f,len f,1)=Rev ((f/^(1-'1))|(len f-'1+1)) by Def3
.=Rev ((f/^0)|len f) by A1,A2,XREAL_1:235
.=Rev (f|len f)
.=Rev f by FINSEQ_1:58;
hence thesis;
end;
suppose
A3: len f=1;
then
A4: f|1=f by FINSEQ_1:58;
mid(f,len f,1)=(f/^(1-'1))|(1-'1+1) by A3,Def3
.=f|1 by A2;
hence thesis by A1,A4,Th110,FINSEQ_1:59;
end;
end;
theorem Th121:
for f being FinSequence, k1,k2,i being Nat st
1<=k1 & k1<=k2 & k2<=len f & 1<=i & (i<=k2-'k1+1 or i<=k2-k1+1 or i<=k2+1-k1)
holds mid(f,k1,k2).i=f.(i+k1-'1) & mid(f,k1,k2).i=f.(i-'1+k1) & mid(f,k1,k2).i=
f.(i+k1-1) & mid(f,k1,k2).i=f.(i-1+k1)
proof
let f be FinSequence, k1,k2,i be Nat;
assume that
A1: 1<=k1 and
A2: k1<=k2 and
A3: k2<=len f and
A4: 1<=i and
A5: i<=k2-'k1+1 or i<=k2-k1+1 or i<=k2+1-k1;
A6: k1<=len f by A2,A3,XXREAL_0:2;
i+k1>=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,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,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, k1,k2 being Nat
holds len mid(f,k1,k2)<=len f
proof
let f be FinSequence;
let k1, k2 be Nat;
per cases;
suppose k1 <= k2;
then A1: mid(f,k1,k2) = (f/^(k1-'1))|(k2-'k1+1) by Def3;
per cases;
suppose len (f/^(k1-'1)) <= (k2-'k1+1);
then A2: mid(f,k1,k2) = f/^(k1-'1) by A1, FINSEQ_1:58;
per cases;
suppose A3: k1-'1 <= len f;
len f - (k1-'1) <= len f - 0 by XREAL_1:10;
hence len mid(f,k1,k2) <= len f by A2, A3, RFINSEQ:def 1;
end;
suppose not (k1-'1 <= len f);
then f/^(k1-'1) = {} by RFINSEQ:def 1;
hence len mid(f,k1,k2) <= len f by A2;
end;
end;
suppose len (f/^(k1-'1)) > (k2-'k1+1);
then A5: len mid(f,k1,k2) <= len (f/^(k1-'1)) by A1, FINSEQ_1:59;
per cases;
suppose k1-'1 <= len f;
then A6: len mid(f,k1,k2) <= len f - (k1-'1) by A5, RFINSEQ:def 1;
len f - (k1-'1) <= len f - 0 by XREAL_1:10;
hence thesis by A6, XXREAL_0:2;
end;
suppose not (k1-'1 <= len f);
then f/^(k1-'1) = {} by RFINSEQ:def 1;
hence thesis by A5;
end;
end;
end;
suppose k1 > k2;
then A7: mid(f,k1,k2) = Rev ((f/^(k2-'1))|(k1-'k2+1)) by Def3;
set m = (f/^(k2-'1))|(k1-'k2+1);
len m <= len f
proof
per cases;
suppose len (f/^(k2-'1)) <= (k1-'k2+1);
then A8: m = f/^(k2-'1) by FINSEQ_1:58;
per cases;
suppose A9: k2-'1 <= len f;
len f - (k2-'1) <= len f - 0 by XREAL_1:10;
hence thesis by A8, A9, RFINSEQ:def 1;
end;
suppose not (k2-'1 <= len f);
then f/^(k2-'1) = {} by RFINSEQ:def 1;
hence thesis;
end;
end;
suppose len (f/^(k2-'1)) > (k1-'k2+1);
then A11: len m <= len (f/^(k2-'1)) by FINSEQ_1:59;
per cases;
suppose k2-'1 <= len f;
then A12: len m <= len f - (k2-'1) by A11, RFINSEQ:def 1;
len f - (k2-'1) <= len f - 0 by XREAL_1:10;
hence thesis by A12, XXREAL_0:2;
end;
suppose not (k2-'1 <= len f);
then f/^(k2-'1) = {} by RFINSEQ:def 1;
hence thesis;
end;
end;
end;
hence thesis by A7, FINSEQ_5:def 3;
end;
end;
theorem Th124:
for f being FinSequence, k being Nat, p being set holds
(<*p*>^f)|(k+1) = <*p*>^(f|k)
proof
let f be FinSequence, k be Nat, p be set;
thus (<*p*>^f)|(k+1) = (<*p*>^f)|Seg(k+len<*p*>) by FINSEQ_1:39
.= <*p*>^(f|k) by Th14;
end;
Th126:
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;
theorem
for p being FinSequence, k1,k2 being Nat
st k1 < k2 & k1 in dom p holds mid(p,k1,k2) = <*p.k1*> ^ mid(p,k1+1,k2)
proof
let p be FinSequence, k1,k2 be Nat;
assume A1: k1 < k2 & k1 in dom p;
then reconsider D = rng p as non empty set by FUNCT_1:3;
reconsider q = p as FinSequence of D by FINSEQ_1:def 4;
mid(q,k1,k2) = <*q.k1*> ^ mid(q,k1+1,k2) by A1,Th126;
hence thesis;
end;
begin :: from GRAPH_2, 2018.04.10
reserve p, q for FinSequence,
X, Y, x, y for set,
D for non empty set,
i, j, k, l, m, n, r for Nat;
theorem Th1:
for m,k,n being Nat holds m+1<=k & k<=n iff
ex i being Nat st m<=i & i<n & k=i+1
proof
let m,k,n be Nat;
hereby
reconsider a19=1 as Integer;
reconsider k9=k as Integer;
assume that
A1: m+1<=k and
A2: k<=n;
1<=m+1 by NAT_1:11;
then k9-a19 in NAT by A1,INT_1:5,XXREAL_0:2;
then reconsider i=k9-a19 as Nat;
take i;
m+1-1<=k-1 by A1,XREAL_1:9;
hence m<=i;
k<k+1 by NAT_1:13;
then k-1<k+1-1 by XREAL_1:9;
hence i<n by A2,XXREAL_0:2;
thus k=i+1;
end;
given i being Nat such that
A3: m<=i and
A4: i<n and
A5: k=i+1;
thus thesis by A3,A4,A5,NAT_1:13,XREAL_1:7;
end;
theorem
q = p|Seg n implies len q<=len p & for i st 1<=i & i<=len q holds p.i = q.i
proof
assume
A1: q = p|Seg n;
per cases;
suppose
A2: n<=len p;
hence len q<=len p by A1,FINSEQ_1:17;
let i be Nat;
assume that
A3: 1<=i and
A4: i<=len q;
len q = n by A1,A2,FINSEQ_1:17;
then i in Seg n by A3,A4;
hence thesis by A1,FUNCT_1:49;
end;
suppose
A5: len p<=n;
hence len q<=len p by A1,FINSEQ_2:20;
let i be Nat;
assume that
1<=i and
i<=len q;
thus thesis by A1,A5,FINSEQ_2:20;
end;
end;
theorem Th3:
X c= Seg k & Y c= dom Sgm X implies (Sgm X)*(Sgm Y) = Sgm rng (( Sgm X)|Y)
proof
assume that
A1: X c= Seg k and
A2: Y c= dom Sgm X;
reconsider Y9 = Y as finite set by A2;
set M = (Sgm X)*(Sgm Y);
set R = rng ((Sgm X)|Y);
Y c= Seg len Sgm X by A2,FINSEQ_1:def 3;
then
a3: Y is included_in_Seg;
then
A4: rng Sgm Y = Y by FINSEQ_1:def 14;
dom Sgm Y9 = Seg card Y9 by a3,FINSEQ_3:40;
then
A5: dom M = Seg card Y9 by A2,A4,RELAT_1:27;
a1: X is included_in_Seg by A1;
then
A6: rng Sgm X c= Seg k by A1,FINSEQ_1:def 14;
then
A7: rng Sgm X c= NAT by XBOOLE_1:1;
reconsider M as FinSequence by A5,FINSEQ_1:def 2;
rng M c= rng Sgm X by RELAT_1:26;
then rng M c= NAT by A7;
then reconsider L = (Sgm X)*(Sgm Y) as FinSequence of NAT by FINSEQ_1:def 4;
now
let y be object;
hereby
assume y in rng L;
then consider x being object such that
A8: x in dom L and
A9: y = L.x by FUNCT_1:def 3;
x in dom Sgm Y by A8,FUNCT_1:11;
then
A10: (Sgm Y).x in Y by A4,FUNCT_1:def 3;
y = (Sgm X).((Sgm Y).x) by A8,A9,FUNCT_1:12;
hence y in R by A2,A10,FUNCT_1:50;
end;
assume y in R;
then consider x being object such that
A11: x in dom ((Sgm X)|Y) and
A12: y = ((Sgm X)|Y).x by FUNCT_1:def 3;
A13: x in (dom Sgm X)/\Y by A11,RELAT_1:61;
then
A14: x in Y by XBOOLE_0:def 4;
then consider z being object such that
A15: z in dom Sgm Y and
A16: x = (Sgm Y).z by A4,FUNCT_1:def 3;
x in dom Sgm X by A13,XBOOLE_0:def 4;
then
A17: z in dom((Sgm X)*(Sgm Y)) by A15,A16,FUNCT_1:11;
y = (Sgm X).x by A12,A14,FUNCT_1:49;
then L.z = y by A16,A17,FUNCT_1:12;
hence y in rng L by A17,FUNCT_1:def 3;
end;
then
A18: rng L = R by TARSKI:2;
A19: now
let l,m be Nat;
assume that
A20: 1 <= l and
A21: l < m and
A22: m <= len L;
set k1=L.l;
set k2=L.m;
l <= len L by A21,A22,XXREAL_0:2;
then
A25: l in dom L by A20,FINSEQ_3:25;
then
A26: L.l = (Sgm X).((Sgm Y).l) by FUNCT_1:12;
1<=m by A20,A21,XXREAL_0:2;
then
A27: m in dom L by A22,FINSEQ_3:25;
then
A28: L.m = (Sgm X).((Sgm Y).m) by FUNCT_1:12;
A29: (Sgm Y).l in dom Sgm X by A25,FUNCT_1:11;
m in dom Sgm Y by A27,FUNCT_1:11;
then
A30: m<=len Sgm Y by FINSEQ_3:25;
A31: (Sgm Y).m in dom Sgm X by A27,FUNCT_1:11;
reconsider l, m as Element of NAT by ORDINAL1:def 12;
reconsider K1 = (Sgm Y).l, K2 = (Sgm Y).m as Element of NAT
by ORDINAL1:def 12;
A32: 1<=K1 by A29,FINSEQ_3:25;
A33: K2<=len Sgm X by A31,FINSEQ_3:25;
K1 < K2 by a3,A20,A21,A30,FINSEQ_1:def 14;
hence k1 < k2 by a1,A26,A28,A32,A33,FINSEQ_1:def 14;
end;
R c= rng Sgm X by RELAT_1:70;
then R c= Seg k by A6;
then R is included_in_Seg;
hence thesis by A18,A19,FINSEQ_1:def 14;
end;
Lm1: for m, n being Nat, F being finite set
st F = {k where k is Nat: m<=k & k<=m+n} holds card F = n+1
proof
let m be Nat;
defpred P[Nat] means
for F being finite set st F = {k where k is Nat: m<=k & k<= m+$1}
holds card F = $1+1;
A1: now
let n be Nat;
assume
A2: P[n];
thus P[n+1]
proof
A3: succ Segm(m+n) = {k where k is Nat: k<=m+n} by NAT_1:54;
set F1 = {k where k is Nat: m<=k & k<=m+n};
F1 c= succ Segm(m+n)
proof
let x be object;
assume x in F1;
then ex k being Nat st x=k & m<=k & k<=m+n;
hence thesis by A3;
end;
then reconsider F1 as finite set;
let F be finite set;
A4: not m+(n+1) in {k where k is Nat: m<=k & k<=m+n}
proof
assume not thesis;
then ex k being Nat
st m+(n+1) = k & m<=k & k<=m+n;
then m+n+1<=m+n+0;
hence contradiction by XREAL_1:6;
end;
assume
A5: F = {k where k is Nat: m<=k & k<=m+(n+1)};
now
let x be object;
hereby
assume x in F;
then consider k being Nat such that
A6: x=k and
A7: m<=k and
A8: k<=m+(n+1) by A5;
k<=m+n+1 by A8;
then k<=m+n or k=m+(n+1) by NAT_1:8;
then k in F1 or k in {m+(n+1)} by A7,TARSKI:def 1;
hence x in F1 \/ {m+(n+1)} by A6,XBOOLE_0:def 3;
end;
assume
A9: x in F1 \/ {m+(n+1)};
per cases by A9,XBOOLE_0:def 3;
suppose
x in F1;
then consider k being Nat such that
A10: x=k and
A11: m<=k and
A12: k<=m+n;
k<=m+n+1 by A12,NAT_1:12;
hence x in F by A5,A10,A11;
end;
suppose
A13: x in {m+(n+1)};
then reconsider k = x as Element of NAT by TARSKI:def 1;
A14: x=m+(n+1) by A13,TARSKI:def 1;
then m<=k by NAT_1:11;
hence x in F by A5,A14;
end;
end;
then
A15: F = {k where k is Nat: m<=k & k<=m+n} \/ {m+(n+1)} by TARSKI:2;
card F1 = n+1 by A2;
hence thesis by A15,A4,CARD_2:41;
end;
end;
A16: P[0]
proof
let F be finite set;
assume
A17: F = {k where k is Nat: m<=k & k<=m+0};
now
let x be object;
hereby
assume x in F;
then ex k being Nat st x = k & m<=k & k<=m+0 by A17;
hence x = m by XXREAL_0:1;
end;
assume x = m;
hence x in F by A17;
end;
then F = {m} by TARSKI:def 1;
hence thesis by CARD_1:30;
end;
for n be Nat holds P[n] from NAT_1:sch 2 (A16, A1);
hence thesis;
end;
theorem Th4:
for m, n being Nat holds
card {k where k is Nat: m<=k & k<=m+n} = n+1
proof
deffunc F(Nat) = $1;
let m, n be Nat;
defpred P[Nat] means m<=$1;
set F = {F(k) where k is Nat: k<=m+n & P[k]};
F is finite from FINSEQ_1:sch 6;
then reconsider F as finite set;
F = {F(k) where k is Nat: m<=k & k<=m+n}
proof
thus F c= {F(k) where k is Nat: m<=k & k<=m+n}
proof
let x be object;
assume x in F;
then ex k1 being Nat st x = F(k1) & k1 <= m+n & m <= k1;
then ex k1 being Nat st x = F(k1) & m <= k1 & k1 <= m+n;
hence thesis;
end;
let x be object;
assume x in {F(k) where k is Nat: m<=k & k<=m+n};
then ex k1 being Nat st x = F(k1) & m <= k1 & k1 <= m+n;
hence thesis;
end;
then reconsider G = {F(k) where k is Nat: m<=k & k<=m+n} as finite set;
card G = n+1 by Lm1;
hence thesis;
end;
theorem
for l st 1<=l & l<=n
holds Sgm {kk where kk is Nat: m+1<=kk & kk<=m+n}.l = m+l
proof
set F= Sgm {kk where kk is Nat: m+1<=kk & kk<=m+n};
defpred P[Nat] means 1<=$1 & $1<=n & F.$1 <> m+$1;
set rF = {kk where kk is Nat: m+1<=kk & kk<=m+n};
A1: rF c= Seg (m+n)
proof
let x be object;
assume x in rF;
then consider x9 being Nat such that
A2: x9=x and
A3: m+1<=x9 and
A4: x9<=m+n;
1<=m+1 by NAT_1:11;
then 1<=x9 by A3,XXREAL_0:2;
hence thesis by A2,A4;
end;
then reconsider rF as finite set;
a1: rF is included_in_Seg by A1;
assume ex l st P[l];
then
A5: ex l be Nat st P[l];
consider k be Nat such that
A6: P[k] and
A7: for nn being Nat st P[nn] holds k <= nn from NAT_1:sch 5 (A5);
reconsider k as Element of NAT by ORDINAL1:def 12;
A8: m+k<=m+n by A6,XREAL_1:7;
reconsider Fk = F.k as Element of NAT by ORDINAL1:def 12;
A9: card rF = n
proof
per cases;
suppose
A10: n = 0;
rF = {}
proof
assume rF <> {};
then consider x being object such that
A11: x in rF by XBOOLE_0:def 1;
ex x9 being Nat st x9=x & m+1<=x9 & x9<=m+n by A11;
then m+1<=m+0 by A10,XXREAL_0:2;
hence contradiction by XREAL_1:6;
end;
hence thesis by A10;
end;
suppose
0<n;
then 0+1<=n by NAT_1:13;
then 1-1<=n-1 by XREAL_1:9;
then n-'1 = n-1 by XREAL_0:def 2;
then reconsider n1 = n-1 as Element of NAT;
(m+1)+n1 = m+n;
then card rF = n1+1 by Th4;
hence thesis;
end;
end;
then
A12: len Sgm rF = n by a1,FINSEQ_3:39;
A13: rng F = rF by a1,FINSEQ_1:def 14;
now
defpred P[Nat] means for Fk be Element of NAT st 1<=$1 & $1<=n & Fk = F.$1
holds m+$1<=Fk;
A14: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A15: P[k];
A16: k<k+1 by NAT_1:13;
let Fk1 be Element of NAT;
assume that
A17: 1<=k+1 and
A18: k+1<=n and
A19: Fk1 = F.(k+1);
per cases by A17,XXREAL_0:1;
suppose
A20: 1<k+1;
reconsider Fk = F.k as Element of NAT by ORDINAL1:def 12;
A21: 1<=k by A20,NAT_1:13;
k<=n by A18,NAT_1:13;
then
A22: m+k<=Fk by A15,A21;
Fk < Fk1 by a1,A12,A18,A19,A16,A21,FINSEQ_1:def 14;
then m+k<Fk1 by A22,XXREAL_0:2;
then m+k+1<=Fk1 by NAT_1:13;
hence thesis;
end;
suppose
A23: 1=k+1;
then 1 in dom F by A12,A18,FINSEQ_3:25;
then F.1 in rng F by FUNCT_1:def 3;
then ex F1 being Nat st F1 = F.1 & m+1<=F1 & F1<=m +n
by A13;
hence thesis by A19,A23;
end;
end;
A24: P[0];
thus for k being Nat holds P[k] from NAT_1:sch 2(A24,A14);
end;
then
A25: m+k<=Fk by A6;
m+1<=m+k by A6,XREAL_1:7;
then m+k in rF by A8;
then m+k in rng Sgm rF by a1,FINSEQ_1:def 14;
then consider x being object such that
A26: x in dom Sgm rF and
A27: m+k = (Sgm rF).x by FUNCT_1:def 3;
reconsider x as Element of NAT by A26;
A28: dom Sgm rF = Seg n by a1,A9,FINSEQ_3:40;
then
A29: 1<=x by A26,FINSEQ_1:1;
A30: x<=n by A28,A26,FINSEQ_1:1;
per cases by A6,A27,XXREAL_0:1;
suppose
k < x;
hence contradiction by a1,A6,A12,A27,A25,A30,FINSEQ_1:def 14;
end;
suppose
A31: k > x;
F.x <> m+x by A6,A27,XCMPLX_1:2;
hence contradiction by A7,A29,A30,A31;
end;
end;
begin :: The cut operation
definition
let p be FinSequence, m, n be Nat;
func (m, n)-cut p -> FinSequence means :Def1:
len it +m = n+1 &
for i being Nat st i<len it holds it.(i+1)=p.(m+i) if
1<=m & m<=n & n<=len p
otherwise it = {};
consistency;
existence
proof
hereby
deffunc F(Nat) = p.(m+($1-1));
assume that
1<=m and
A1: m<=n and
n<=len p;
consider s being FinSequence such that
A2: len s = n+1-'m & for k being Nat st k in dom s holds s.k=F(k)
from FINSEQ_1:sch 2;
take s;
n <= n+1 by XREAL_1:29;
then m <= n+1 by A1,XXREAL_0:2;
then m-m <= n+1-m by XREAL_1:9;
then len s +m = n+1-m+m by A2,XREAL_0:def 2;
hence len s +m = n+1;
let k be Nat;
assume k<len s;
then
A3: k+1<=len s by NAT_1:13;
0+1<=k+1 by XREAL_1:7;
then k+1 in dom s by A3,FINSEQ_3:25;
hence s.(k+1) = p.(m+(k+1-1)) by A2
.= p.(m+k);
end;
thus thesis;
end;
uniqueness
proof
let s1, s2 be FinSequence;
hereby
assume that
1<=m and
m<=n and
n<=len p;
assume that
A4: len s1 +m = n+1 and
A5: for i being Nat st i<len s1 holds s1.(i+1) = p.(m+i);
assume that
A6: len s2 +m = n+1 and
A7: for i being Nat st i<len s2 holds s2.(i+1) = p.(m+i);
now
thus len s1 = len s1;
thus len s2 = len s1 by A4,A6;
let i be Nat;
assume
A8: i in dom s1;
A9: dom s1 = Seg len s1 by FINSEQ_1:def 3;
A10: i<=len s1 by A8,FINSEQ_3:25;
0+1<=i by A9,A8,FINSEQ_1:1;
then consider k such that
0<=k and
A11: k<len s1 and
A12: i=k+1 by A10,Th1;
thus s1.i = p.(m+k) by A5,A11,A12
.= s2.i by A4,A6,A7,A11,A12;
end;
hence s1 = s2 by FINSEQ_2:9;
end;
thus thesis;
end;
end;
Lm2: for p be FinSequence, m, n be Nat st 1<=m & m<=n+1 & n<=len p
holds len (m, n)-cut p +m = n+1 & for i being Nat st i<len (m, n)
-cut p holds ((m, n)-cut p).(i+1)=p.(m+i)
proof
let p be FinSequence, m, n be Nat such that
A1: 1<=m and
A2: m<=n+1 and
A3: n<=len p;
A4: m = n+1 or m < n+1 by A2,XXREAL_0:1;
per cases by A4,NAT_1:13;
suppose
A5: m = n+1;
then
A6: n < m by XREAL_1:29;
then (m, n)-cut p = {} by Def1;
hence len (m, n)-cut p +m = n+1 by A5;
thus thesis by A6,Def1,CARD_1:27;
end;
suppose
m<=n;
hence thesis by A1,A3,Def1;
end;
end;
theorem
1<=m & m<=len p implies (m,m)-cut p = <*p.m*>
proof
assume that
A1: 1<=m and
A2: m<=len p;
set mp = (m,m)-cut p;
A3: len mp + m = m + 1 by A1,A2,Def1;
then mp.(0+1) = p.(m+0) by A1,A2,Def1
.= p.m;
hence thesis by A3,FINSEQ_1:40;
end;
theorem Th7:
(1, len p)-cut p = p
proof
set cp = (1, len p)-cut p;
now
A1: 1<=len p +1 by NAT_1:11;
then
A2: len cp + 1 = len p + 1 by Lm2;
hence len cp = len p;
thus len p = len p;
let i be Nat;
assume
A3: i in dom cp;
A4: dom cp = Seg len p by A2,FINSEQ_1:def 3;
then
A5: i<=len p by A3,FINSEQ_1:1;
0+1<=i by A4,A3,FINSEQ_1:1;
then ex k being Nat st 0<=k & k<len cp & i=k+1 by A2,A5,Th1;
hence cp.i = p.i by A1,Lm2;
end;
hence thesis by FINSEQ_2:9;
end;
theorem Th8:
m<=n & n<=r & r<=len p implies
(m+1, n)-cut p ^ (n+1, r)-cut p = (m+1, r)-cut p
proof
assume that
A1: m<=n and
A2: n<=r and
A3: r<=len p;
set p3 = (m+1, r)-cut p;
set p2 = (n+1, r)-cut p;
set p1 = (m+1, n)-cut p;
set p12 = p1^p2;
now
reconsider n9=n as Integer;
reconsider m9=m as Integer;
thus len p12 = len p12;
A4: dom p12 = Seg len p12 by FINSEQ_1:def 3;
reconsider nm=n9-m9 as Element of NAT by A1,INT_1:5;
A5: 1<=m+1 by NAT_1:11;
m<=r by A1,A2,XXREAL_0:2;
then
A6: m+1<=r+1 by XREAL_1:6;
A7: m+1<=n+1 by A1,XREAL_1:6;
A8: n+1<=r+1 by A2,XREAL_1:6;
then m+1<=r+1 by A7,XXREAL_0:2;
then
A9: len p3 +(m+1)=r+1 by A3,A5,Lm2;
A10: n<=len p by A2,A3,XXREAL_0:2;
then
A11: len p1 +(m+1) = n+1 by A5,A7,Lm2;
A12: 1<=n+1 by NAT_1:11;
then len p2 +(n+1) = r+1 by A3,A8,Lm2;
then
A13: len p12= n-m+(r+ -n) by A11,FINSEQ_1:22
.= r-m;
hence len p3 = len p12 by A9;
let i be Nat;
assume
A14: i in dom p12;
then
A15: 1<=i by A4,FINSEQ_1:1;
A16: i<=len p12 by A4,A14,FINSEQ_1:1;
per cases by NAT_1:13;
suppose
A17: i<=nm;
0+1=1;
then consider k being Nat such that
0<=k and
A18: k<nm and
A19: i=k+1 by A15,A17,Th1;
nm<=r-m by A2,XREAL_1:9;
then
A20: k<len p3 by A9,A18,XXREAL_0:2;
i in dom p1 by A11,A15,A17,FINSEQ_3:25;
hence p12.i = p1.i by FINSEQ_1:def 7
.= p.((m+1)+k) by A5,A7,A10,A11,A18,A19,Lm2
.= p3.i by A3,A5,A6,A19,A20,Lm2;
end;
suppose
nm+1<=i;
then consider k such that
A21: nm<=k and
A22: k<len p12 and
A23: i=k+1 by A16,Th1;
reconsider k99=k as Integer;
reconsider k9=k99-nm as Element of NAT by A21,INT_1:5;
A24: 1<=k9+1 by NAT_1:11;
len p12 = len p2 + len p1 by FINSEQ_1:22;
then len p2 = len p12 - len p1;
then
A25: k9<len p2 by A11,A22,XREAL_1:9;
then k9+1<=len p2 by NAT_1:13;
then
A26: k9+1 in dom p2 by A24,FINSEQ_3:25;
A27: n+1+k9 = m+1+k;
i = nm+(k9+1) by A23;
hence p12.i = p2.(k9+1) by A11,A26,FINSEQ_1:def 7
.= p.(n+1+k9) by A3,A12,A8,A25,Lm2
.= p3.i by A3,A5,A6,A13,A9,A22,A23,A27,Lm2;
end;
end;
hence thesis by FINSEQ_2:9;
end;
theorem
m<=len p implies (1, m)-cut p ^ (m+1, len p)-cut p = p
proof
set cp1 = (1, m)-cut p;
set cpm = (m+1, len p)-cut p;
A1: 0+1=1;
assume m<=len p;
hence cp1 ^ cpm = (1, len p)-cut p by A1,Th8
.= p by Th7;
end;
theorem
m<=n & n<=len p implies
(1, m)-cut p ^ (m+1, n)-cut p ^ (n+1, len p)-cut p = p
proof
assume that
A1: m<=n and
A2: n<=len p;
set cp3 = (n+1, len p)-cut p;
set cp2 = (m+1, n)-cut p;
set cp1 = (1, m)-cut p;
A3: 0+1=1;
hence cp1^cp2^cp3 = (1, n)-cut p ^cp3 by A1,A2,Th8
.= (1, len p)-cut p by A2,A3,Th8
.= p by Th7;
end;
theorem Th11:
rng ((m,n)-cut p) c= rng p
proof
set c = ((m,n)-cut p);
A1: now
assume that
A2: 1<=m and
A3: m<=n and
A4: n<=len p;
n <= n+1 by NAT_1:11;
then
A5: m <= n+1 by A3,XXREAL_0:2;
thus thesis
proof
let x be object;
assume x in rng c;
then consider z being object such that
A6: z in dom c and
A7: x = c.z by FUNCT_1:def 3;
reconsider z as Element of NAT by A6;
A8: z<=len c by A6,FINSEQ_3:25;
0+1<=z by A6,FINSEQ_3:25;
then consider i such that
0<=i and
A9: i<len c and
A10: z=i+1 by A8,Th1;
m+i<len c +m by A9,XREAL_1:6;
then m+i<n+1 by A2,A4,A5,Lm2;
then m+i<=n by NAT_1:13;
then
A11: m+i<=len p by A4,XXREAL_0:2;
1<=m+i by A2,NAT_1:12;
then
A12: m+i in dom p by A11,FINSEQ_3:25;
c.z = p.(m+i) by A2,A4,A5,A9,A10,Lm2;
hence thesis by A7,A12,FUNCT_1:def 3;
end;
end;
now
assume not (1<=m & m<=n & n<=len p);
then c = {} by Def1;
then rng c = {};
hence thesis;
end;
hence thesis by A1;
end;
definition
let D be set, p be FinSequence of D, m, n be Nat;
redefine func (m, n)-cut p -> FinSequence of D; :: redefines -cut (FINSEQ_6, definition)
coherence
proof
A1: rng p c= D by FINSEQ_1:def 4;
rng (m,n)-cut p c= rng p by Th11;
then rng (m,n)-cut p c= D by A1;
hence thesis by FINSEQ_1:def 4;
end;
end;
theorem
1<=m & m<=n & n<=len p implies ((m,n)-cut p).1 = p.m &
((m,n)-cut p).len ((m,n)-cut p)=p.n
proof
set c = ((m,n)-cut p);
assume that
A1: 1<=m and
A2: m<=n and
A3: n<=len p;
A4: m<=n+1 by A2,NAT_1:12;
then
A5: len c +m = n+1 by A1,A3,Lm2;
A6: now
assume len c = 0;
then n+1<=n+0 by A2,A5;
hence contradiction by XREAL_1:6;
end;
then 0+1<=len c by NAT_1:13;
then consider i being Nat such that
0<=i and
A7: i<len c and
A8: len c =i+1 by Th1;
0+1=1;
hence c.1 = p.(m+0) by A1,A3,A4,A6,Lm2
.= p.m;
m+i = n by A5,A8;
hence thesis by A1,A3,A4,A7,A8,Lm2;
end;
begin :: The glueing catenation
definition
let p, q be FinSequence;
func p ^' q -> FinSequence equals
p^(2, len q)-cut q;
correctness;
end;
theorem Th13:
q<>{} implies len (p^'q) +1 = len p + len q
proof
set r = (p^'q);
set qc = (2,len q)-cut q;
assume q<>{};
then 0+1<=len q by NAT_1:13;
then 1+1<=len q +1 by XREAL_1:7;
then
A1: len qc +(1+1) = len q + 1 by Lm2;
thus len r +1 = len p + len qc + 1 by FINSEQ_1:22
.= len p + len q by A1;
end;
theorem Th14:
1<=k & k<=len p implies (p^'q).k=p.k
proof
assume that
A1: 1<=k and
A2: k<=len p;
k in dom p by A1,A2,FINSEQ_3:25;
hence thesis by FINSEQ_1:def 7;
end;
theorem Th15:
1<=k & k<len q implies (p^'q).(len p +k) = q.(k+1)
proof
set qc = (2,len q)-cut q;
assume that
A1: 1<=k and
A2: k<len q;
per cases;
suppose
q={};
hence thesis by A2;
end;
suppose
q<>{};
then 0+1<=len q by NAT_1:13;
then
A3: 1+1<=len q +1 by XREAL_1:7;
then len qc +(1+1) = len q + 1 by Lm2;
then len qc +1+1 = len q + 1;
then
A4: k<=len qc by A2,NAT_1:13;
0+1<=k by A1;
then consider i being Nat such that
0<=i and
A5: i<len qc and
A6: k=i+1 by A4,Th1;
k in dom qc by A1,A4,FINSEQ_3:25;
hence (p^'q).(len p +k) = qc.k by FINSEQ_1:def 7
.= q.(1+1+i) by A3,A5,A6,Lm2
.= q.(k+1) by A6;
end;
end;
theorem Th16:
1<len q implies (p^'q).len (p^'q) = q.len q
proof
set r = p^'q;
set qc = (2,len q)-cut q;
assume
A1: 1<len q;
then 1+1<=len q by NAT_1:13;
then
A2: 1+1-1<=len q -1 by XREAL_1:9;
q<>{} by A1;
then len r +1-1=len p +len q -1 by Th13;
then
A3: len r = len p +(len q -1);
1+1<=len q +1 by A1,XREAL_1:7;
then len qc +(1+1) = len q + 1 by Lm2;
then
A4: len qc +1+1 = len q + 1;
then len qc < len q by NAT_1:13;
hence thesis by A3,A4,A2,Th15;
end;
theorem Th17:
rng (p^'q) c= rng p \/ rng q
proof
set r = p^'q;
set qc = (2,len q)-cut q;
let x be object;
assume x in rng r;
then x in rng p \/ rng qc by FINSEQ_1:31;
then
A1: x in rng p or x in rng qc by XBOOLE_0:def 3;
rng qc c= rng q by Th11;
hence thesis by A1,XBOOLE_0:def 3;
end;
definition
let D be set, p, q be FinSequence of D;
redefine func p^'q -> FinSequence of D; :: redefines ^' (FINSEQ_6, definition)
coherence
proof
A1: rng (p^'q) c= rng p \/ rng q by Th17;
A2: rng q c= D by FINSEQ_1:def 4;
rng p c= D by FINSEQ_1:def 4;
then rng p \/ rng q c= D by A2,XBOOLE_1:8;
then rng (p^'q) c= D by A1;
hence thesis by FINSEQ_1:def 4;
end;
end;
theorem
p<>{} & q<>{} & p.len p = q.1 implies rng (p^'q) = rng p \/ rng q
proof
set r = p^'q;
set qc = (2,len q)-cut q;
assume that
A1: p<>{} and
A2: q<>{} and
A3: p.len p = q.1;
0+1<=len q by A2,NAT_1:13;
then
A4: 1+1<=len q +1 by XREAL_1:7;
then len qc +(1+1) = len q + 1 by Lm2;
then
A5: len qc +1+1 = len q + 1;
now
let x be object;
hereby
assume x in rng r;
then x in rng p \/ rng qc by FINSEQ_1:31;
then
A6: x in rng p or x in rng qc by XBOOLE_0:def 3;
rng qc c= rng q by Th11;
hence x in rng p \/ rng q by A6,XBOOLE_0:def 3;
end;
assume x in rng p \/ rng q;
then
A7: x in rng p or x in rng q by XBOOLE_0:def 3;
assume not x in rng r;
then
A8: not x in rng p \/ rng qc by FINSEQ_1:31;
then consider y being object such that
A9: y in dom q and
A10: x=q.y by A7,FUNCT_1:def 3,XBOOLE_0:def 3;
A11: not x in rng p by A8,XBOOLE_0:def 3;
reconsider y as Element of NAT by A9;
A12: 1<=y by A9,FINSEQ_3:25;
A13: y<=len q by A9,FINSEQ_3:25;
A14: not x in rng qc by A8,XBOOLE_0:def 3;
per cases by A12,XXREAL_0:1;
suppose
A15: y=1;
0+1<=len p by A1,NAT_1:13;
then len p in dom p by FINSEQ_3:25;
hence contradiction by A3,A11,A10,A15,FUNCT_1:def 3;
end;
suppose
1<y;
then 1+1<=y by NAT_1:13;
then consider i such that
A16: 1<=i and
A17: i<len q and
A18: y=i+1 by A13,Th1;
A19: i<=len qc by A5,A17,NAT_1:13;
then
A20: i in dom qc by A16,FINSEQ_3:25;
0+1<=i by A16;
then consider j such that
0<=j and
A21: j<len qc and
A22: i=j+1 by A19,Th1;
qc.(j+1) = q.(1+1+j) by A4,A21,Lm2
.= q.y by A18,A22;
hence contradiction by A14,A10,A22,A20,FUNCT_1:def 3;
end;
end;
hence thesis by TARSKI:2;
end;
begin :: Two valued alternating finsequences
definition
let f be FinSequence;
attr f is TwoValued means
card rng f = 2;
end;
Lm3: now
set p = <*1, 2*>;
2 > 1;
hence len p > 1 by FINSEQ_1:44;
thus 1 <> 2;
thus rng p = rng<*1*>\/ rng<*2*> by FINSEQ_1:31
.= {1} \/ rng <*2*> by FINSEQ_1:38
.= {1} \/ {2} by FINSEQ_1:38
.= {1, 2} by ENUMSET1:1;
end;
theorem Th19:
p is TwoValued iff len p >1 & ex x,y being object st x<>y & rng p = {x, y}
proof
hereby
assume p is TwoValued;
then card rng p = 2;
then consider x,y being object such that
A1: x<>y and
A2: rng p={x,y} by CARD_2:60;
thus len p >1
proof
set l=len p;
assume
A3: len p<=1;
per cases by A3,NAT_1:25;
suppose
l=0;
then p={};
hence contradiction by A2;
end;
suppose
A4: l=1;
then 1 in dom p by FINSEQ_3:25;
then consider z being object such that
A5: [1,z] in p by XTUPLE_0:def 12;
z=p.1 by A5,FUNCT_1:1;
then p=<*z*> by A4,FINSEQ_1:40;
then
A6: rng p = {z} by FINSEQ_1:39;
then z=x by A2,ZFMISC_1:4;
hence contradiction by A1,A2,A6,ZFMISC_1:4;
end;
end;
thus ex x,y being object st x<>y & rng p ={x, y} by A1,A2;
end;
assume len p >1;
given x, y being object such that
A7: x<>y and
A8: rng p = {x, y};
card rng p = 2 by A7,A8,CARD_2:57;
hence thesis;
end;
then
Lm4: <*1, 2*> is TwoValued by Lm3;
Lm5: now
let i be Nat;
set p = <*1, 2*>;
assume that
A1: 1<=i and
A2: (i+1)<=len p;
i+1<=1+1 by A2,FINSEQ_1:44;
then i<=1 by XREAL_1:6;
then
A3: i = 1 by A1,XXREAL_0:1;
thus p.i <> p.(i+1) by A3;
end;
definition
let f be FinSequence;
attr f is Alternating means
:Def4:
for i being Nat st 1<=i & (i+1)<=len f holds f.i <> f.(i+1);
end;
Lm6: <*1, 2*> is Alternating by Lm5;
registration
cluster TwoValued Alternating for FinSequence;
existence by Lm4,Lm6;
end;
reserve a, a1, a2 for TwoValued Alternating FinSequence;
theorem Th20:
len a1 = len a2 & rng a1 = rng a2 & a1.1 = a2.1 implies a1 = a2
proof
assume that
A1: len a1 = len a2 and
A2: rng a1 = rng a2 and
A3: a1.1 = a2.1;
defpred P[Nat] means 1<=$1 & $1<=len a1 implies a1.$1=a2.$1;
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume that
A5: 1<=k & k<=len a1 implies a1.k = a2.k;
A6: 0=k or 0<k & 0+1=1;
assume that
A7: 1<=k+1 and
A8: k+1<=len a1;
A9: k+1 in dom a1 by A7,A8,FINSEQ_3:25;
per cases by A6,NAT_1:13;
suppose
0 = k;
hence thesis by A3;
end;
suppose
A10: 1<=k;
A11: dom a2 = Seg len a2 by FINSEQ_1:def 3;
consider X, Y being object such that
X <> Y and
A12: rng a1 = { X, Y } by Th19;
a1.(k+1) in rng a1 by A9,FUNCT_1:def 3;
then
A13: a1.(k+1)=X or a1.(k+1)= Y by A12,TARSKI:def 2;
dom a1 = Seg len a1 by FINSEQ_1:def 3;
then a2.(k+1) in rng a2 by A1,A9,A11,FUNCT_1:def 3;
then
A14: a2.(k+1) = X or a2.(k+1) = Y by A2,A12,TARSKI:def 2;
k<=len a1 by A8,NAT_1:13;
then k in dom a1 by A10,FINSEQ_3:25;
then a1.k in rng a1 by FUNCT_1:def 3;
then a1.k=X or a1.k=Y by A12,TARSKI:def 2;
hence thesis by A1,A5,A8,A10,A13,A14,Def4,NAT_1:13;
end;
end;
A15: P[0];
for i being Nat holds P[i] from NAT_1:sch 2(A15, A4);
hence thesis by A1;
end;
theorem Th21:
a1<>a2 & len a1 = len a2 & rng a1 = rng a2 implies
for i st 1<=i & i<=len a1 holds a1.i<>a2.i
proof
assume that
A1: a1 <> a2 and
A2: len a1 = len a2 and
A3: rng a1 = rng a2;
defpred P[Nat] means 1<=$1 & $1<=len a1 implies a1.$1<>a2.$1;
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume that
A5: 1<=k & k<=len a1 implies a1.k <> a2.k;
A6: 0=k or 0<k & 0+1=1;
assume that
A7: 1<=k+1 and
A8: k+1<=len a1;
A9: k+1 in dom a1 by A7,A8,FINSEQ_3:25;
per cases by A6,NAT_1:13;
suppose
0 = k;
hence thesis by A1,A2,A3,Th20;
end;
suppose
A10: 1<=k;
k<=len a1 by A8,NAT_1:13;
then
A11: k in dom a1 by A10,FINSEQ_3:25;
A12: dom a2 = Seg len a2 by FINSEQ_1:def 3;
consider X, Y being object such that
X <> Y and
A13: rng a1 = { X, Y } by Th19;
a1.(k+1) in rng a1 by A9,FUNCT_1:def 3;
then
A14: a1.(k+1)=X or a1.(k+1)= Y by A13,TARSKI:def 2;
dom a1 = Seg len a1 by FINSEQ_1:def 3;
then a2.k in rng a2 by A2,A11,A12,FUNCT_1:def 3;
then
A15: a2.k=X or a2.k=Y by A3,A13,TARSKI:def 2;
a1.k in rng a1 by A11,FUNCT_1:def 3;
then a1.k=X or a1.k=Y by A13,TARSKI:def 2;
hence thesis by A2,A5,A8,A10,A15,A14,Def4,NAT_1:13;
end;
end;
A16: P[0];
thus for i holds P[i] from NAT_1:sch 2 (A16, A4);
end;
theorem
a1<>a2 & len a1 = len a2 & rng a1 = rng a2 implies
for a st len a=len a1 & rng a=rng a1 holds a=a1 or a=a2
proof
assume that
A1: a1 <> a2 and
A2: len a1 = len a2 and
A3: rng a1 = rng a2;
let a;
assume that
A4: len a = len a1 and
A5: rng a = rng a1;
assume
A6: a <> a1;
now
let i be Nat;
assume that
A7: 1<=i and
A8: i<=len a;
consider X, Y being object such that
X <> Y and
A9: rng a = { X, Y } by Th19;
A10: i in dom a by A7,A8,FINSEQ_3:25;
then a.i in rng a by FUNCT_1:def 3;
then
A11: a.i=X or a.i=Y by A9,TARSKI:def 2;
A12: dom a=Seg len a by FINSEQ_1:def 3;
dom a1=Seg len a1 by FINSEQ_1:def 3;
then a1.i in rng a1 by A4,A10,A12,FUNCT_1:def 3;
then
A13: a1.i=X or a1.i=Y by A5,A9,TARSKI:def 2;
dom a2=Seg len a2 by FINSEQ_1:def 3;
then a2.i in rng a2 by A2,A4,A10,A12,FUNCT_1:def 3;
then a2.i=X or a2.i=Y by A3,A5,A9,TARSKI:def 2;
hence a.i = a2.i by A1,A2,A3,A4,A5,A6,A7,A8,A11,A13,Th21;
end;
hence thesis by A2,A4;
end;
theorem
X <> Y & n > 1 implies ex a1 st rng a1 = {X, Y} & len a1 = n & a1.1 = X
proof
deffunc F(Nat,Nat) = 3-'$2;
assume that
A1: X <> Y and
A2: n > 1;
set p = <*X, Y*>;
A3: p.1 = X;
A4: 3-'2 =1+2-2 by XREAL_0:def 2
.=1;
A5: p.2 = Y;
consider f1 being sequence of NAT such that
A6: f1.0=2 & for n being Nat holds f1.(n+1)=F(n,f1.n)
from NAT_1:sch 12;
defpred P[Nat] means (f1.$1=1 or f1.$1=2) & f1.$1<>f1.($1+1);
A7: 3-'1=2+1-1 by XREAL_0:def 2
.=2;
A8: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A9: f1.i = 1 or f1.i = 2 and
f1.i <> f1.(i+1);
thus f1.(i+1)=1 or f1.(i+1) = 2 by A6,A4,A7,A9;
hence thesis by A6,A4,A7;
end;
A10: P[0] by A6,A4;
A11: for i being Nat holds P[i] from NAT_1:sch 2(A10, A8);
deffunc F(Nat) = p.(f1.$1);
consider p1 being FinSequence such that
A12: len p1 = n & for k be Nat st k in dom p1 holds p1.k= F(k) from
FINSEQ_1:sch 2;
A13: f1.(0+1) = 1 by A6,A4;
then
A14: f1.(1+1) = 2 by A6,A7;
A15: now
let y be object;
hereby
assume y in {X, Y};
then
A16: y = X or y = Y by TARSKI:def 2;
1 in dom p1 by A2,A12,FINSEQ_3:25;
then
A17: p1.1=X by A3,A13,A12;
A18: 1 in dom p1 by A2,A12,FINSEQ_3:25;
1+1<=n by A2,NAT_1:13;
then
A19: 2 in dom p1 by A12,FINSEQ_3:25;
then p1.2=Y by A5,A14,A12;
hence ex x being object st x in dom p1 & y = p1.x by A16,A19,A17,A18;
end;
given x being object such that
A20: x in dom p1 and
A21: y = p1.x;
x in Seg len p1 by A20,FINSEQ_1:def 3;
then consider x9 being Nat such that
A22: x9=x and
A23: 1<=x9 and
A24: x9<=len p1;
x9 in dom p1 by A23,A24,FINSEQ_3:25;
then
A25: p1.x9 = p.(f1.x9) by A12;
f1.x9 = 1 or f1.x9 = 2 by A11;
hence y in {X, Y} by A21,A22,A25,TARSKI:def 2;
end;
then rng p1 = {X, Y} by FUNCT_1:def 3;
then reconsider p1 as TwoValued FinSequence by A1,A2,A12,Th19;
now
let i be Nat;
assume that
A26: 1<=i and
A27: (i+1)<=len p1;
1<=(i+1) by A26,NAT_1:13;
then (i+1) in dom p1 by A27,FINSEQ_3:25;
then
A28: p1.(i+1)=p.(f1.(i+1)) by A12;
A29: f1.(i+1)=1 or f1.(i+1)=2 by A11;
i<=n by A12,A27,NAT_1:13;
then i in dom p1 by A12,A26,FINSEQ_3:25;
then p1.i=p.(f1.i) by A12;
hence p1.i <> p1.(i+1) by A1,A3,A5,A11,A28,A29;
end;
then reconsider p1 as TwoValued Alternating FinSequence by Def4;
take p1;
thus rng p1 = {X, Y} by A15,FUNCT_1:def 3;
thus len p1 = n by A12;
1 in dom p1 by A2,A12,FINSEQ_3:25;
hence thesis by A3,A13,A12;
end;
begin :: Finite subsequences of finite sequences
registration
let X;
let fs be FinSequence of X;
cluster -> FinSubsequence-like for Subset of fs;
coherence
proof
let IT be Subset of fs;
take len fs;
dom IT c= dom fs by RELAT_1:11;
hence thesis by FINSEQ_1:def 3;
end;
end;
theorem
for f being FinSubsequence, g, h, fg, fh, fgh being FinSequence
st rng g c= dom f & rng h c= dom f & fg=f*g & fh=f*h & fgh=f*(g^h) holds
fgh = fg^fh
proof
let f be FinSubsequence, g, h, fg, fh, fgh be FinSequence;
assume that
A1: rng g c= dom f and
A2: rng h c= dom f and
A3: fg=f*g and
A4: fh=f*h and
A5: fgh=f*(g^h);
now
rng (g^h) = rng g \/ rng h by FINSEQ_1:31;
hence len fgh = len (g^h) by A1,A2,A5,FINSEQ_2:29,XBOOLE_1:8
.= len g + len h by FINSEQ_1:22;
then
A6: dom fgh = Seg (len g +len h) by FINSEQ_1:def 3;
A7: dom fh = dom h by A2,A4,RELAT_1:27;
A8: dom fg = dom g by A1,A3,RELAT_1:27;
A9: len fg = len g by A1,A3,FINSEQ_2:29;
len fh = len h by A2,A4,FINSEQ_2:29;
hence len (fg^fh) = len g + len h by A9,FINSEQ_1:22;
let j be Nat;
assume
A10: j in dom fgh;
then
A11: 1<=j by A6,FINSEQ_1:1;
A12: j<=len g + len h by A6,A10,FINSEQ_1:1;
per cases;
suppose
j<=len g;
then
A13: j in dom g by A11,FINSEQ_3:25;
thus fgh.j = f.((g^h).j) by A5,A10,FUNCT_1:12
.= f.(g.j) by A13,FINSEQ_1:def 7
.= fg.j by A3,A13,FUNCT_1:13
.= (fg^fh).j by A8,A13,FINSEQ_1:def 7;
end;
suppose
len g < j;
then len g +1 <=j by NAT_1:13;
then
A14: 1<=j-len g by XREAL_1:19;
then j-'len g = j-len g by XREAL_0:def 2;
then reconsider j9 = j-len g as Element of NAT;
A15: j = len g + j9;
then j9<=len h by A12,XREAL_1:6;
then
A16: j9 in dom h by A14,FINSEQ_3:25;
thus fgh.j = f.((g^h).j) by A5,A10,FUNCT_1:12
.= f.(h.j9) by A15,A16,FINSEQ_1:def 7
.= fh.j9 by A4,A16,FUNCT_1:13
.= (fg^fh).j by A9,A7,A15,A16,FINSEQ_1:def 7;
end;
end;
hence thesis by FINSEQ_2:9;
end;
reserve fs, fs1, fs2 for FinSequence of X,
fss, fss2 for Subset of fs;
theorem
dom fss c= dom fs & rng fss c= rng fs by RELAT_1:11;
theorem
fs is Subset of fs
proof
fs c= fs;
hence thesis;
end;
theorem
fss|Y is Subset of fs
proof
reconsider f = fss|Y as FinSubsequence;
f c= fss by RELAT_1:59;
hence thesis by XBOOLE_1:1;
end;
theorem
for fss1 being Subset of fs1 st Seq fss = fs1 & Seq fss1 = fs2 &
fss2 = fss|rng((Sgm dom fss)|dom fss1) holds Seq fss2 = fs2
proof
let fss1 be Subset of fs1 such that
A1: Seq fss = fs1 and
A2: Seq fss1 = fs2 and
A3: fss2 = fss|rng((Sgm dom fss)|dom fss1);
consider k be Nat such that
A4: dom fs = Seg k by FINSEQ_1:def 2;
reconsider d2 = dom fss2 as finite set;
reconsider d1 = dom fss1 as finite set;
A6: dom Sgm d1 = Seg card d1 by FINSEQ_3:40;
reconsider k as Element of NAT by ORDINAL1:def 12;
A7: dom fss c= Seg k by A4,RELAT_1:11;
rng Sgm dom fss c= dom fss by FINSEQ_1:def 14;
then
A8: dom fs1 = dom Sgm dom fss by A1,RELAT_1:27;
A9: rng Sgm dom fss2 = dom fss2 by FINSEQ_1:def 14;
A10: (Sgm dom fss)|dom fss1 c= Sgm dom fss by RELAT_1:59;
then
A11: dom ((Sgm dom fss)|dom fss1) c= dom (Sgm dom fss) by RELAT_1:11;
rng ((Sgm dom fss)|dom fss1) c= rng (Sgm dom fss) by A10,RELAT_1:11;
then
rng((Sgm dom fss)|dom fss1) c= dom fss by FINSEQ_1:def 14;
then
A12: dom fss2 = rng((Sgm dom fss)|dom fss1) by A3,RELAT_1:62;
A13: dom fss1 c= dom fs1 by RELAT_1:11;
now
take Z = (Sgm dom fss)|dom fss1;
A14: dom Z = dom fss1 by A8,RELAT_1:11,62;
hereby
let x be object;
assume
A15: x in d1;
reconsider y = Z.x as object;
take y;
thus y in d2 by A12,A14,A15,FUNCT_1:def 3;
thus [x,y] in Z by A14,A15,FUNCT_1:1;
end;
hereby
let y be object;
assume y in d2;
then consider x being object such that
A16: x in dom Z and
A17: y = Z.x by A12,FUNCT_1:def 3;
reconsider x as object;
take x;
thus x in d1 & [x,y] in Z by A13,A8,A16,A17,FUNCT_1:1,RELAT_1:62;
end;
let x,y,z,u be object;
assume that
A18: [x,y] in Z and
A19: [z,u] in Z;
A20: z in dom Z by A19,FUNCT_1:1;
A21: u = Z.z by A19,FUNCT_1:1;
A22: u = (Sgm dom fss).z by A20,A21,FUNCT_1:47;
A23: y = Z.x by A18,FUNCT_1:1;
hence x=z implies y=u by A19,FUNCT_1:1;
A24: x in dom Z by A18,FUNCT_1:1;
then
A25: y = (Sgm dom fss).x by A23,FUNCT_1:47;
assume
A26: y=u;
assume
A27: x<>z;
reconsider x,z as Element of NAT by A24,A20;
A28: x<=len Sgm dom fss by A11,A24,FINSEQ_3:25;
A29: z<= len Sgm dom fss by A11,A20,FINSEQ_3:25;
A30: 1<=z by A11,A20,FINSEQ_3:25;
A31: 1<=x by A11,A24,FINSEQ_3:25;
per cases by A27,XXREAL_0:1;
suppose x < z;
hence contradiction by A25,A22,A26,A31,A29,FINSEQ_1:def 14;
end;
suppose z < x;
hence contradiction by A25,A22,A26,A28,A30,FINSEQ_1:def 14;
end;
end;
then d1,d2 are_equipotent;
then card d1 = card d2 by CARD_1:5;
then
A32: dom Sgm d2 = Seg card d1 by FINSEQ_3:40;
A33: rng Sgm dom fss1 = dom fss1 by FINSEQ_1:def 14;
now
now
let x be object;
hereby
assume x in dom fs2;
then
A34: x in dom Sgm dom fss2 by A2,A6,A32,FUNCT_1:11;
then (Sgm dom fss2).x in dom fss2 by A9,FUNCT_1:def 3;
hence x in dom Seq fss2 by A34,FUNCT_1:11;
end;
assume x in dom Seq fss2;
then
A35: x in dom Sgm dom fss1 by A6,A32,FUNCT_1:11;
then (Sgm dom fss1).x in dom fss1 by A33,FUNCT_1:def 3;
hence x in dom fs2 by A2,A35,FUNCT_1:11;
end;
hence
A36: dom fs2 = dom Seq fss2 by TARSKI:2;
thus dom fs2 = dom fs2;
let k be Nat;
assume
A37: k in dom fs2;
then
A38: (Sgm dom fss1).k in dom fss1 by A2,FUNCT_1:11;
A39: (Sgm dom fss2).k in dom fss2 by A36,A37,FUNCT_1:11;
A40: (Sgm dom fss1).k in dom fss1 by A2,A37,FUNCT_1:11;
then
A41: fss1.((Sgm dom fss1).k) = (Seq fss).((Sgm dom fss1).k) by A1,GRFUNC_1:2;
A42: (Sgm dom fss2).k = ((Sgm dom fss)*(Sgm dom fss1)).k by A7,A12,A8,Th3,
RELAT_1:11;
k in dom Sgm dom fss1 by A2,A37,FUNCT_1:11;
then k in dom ((Sgm dom fss)*(Sgm dom fss1)) by A13,A8,A38,FUNCT_1:11;
then
A43: (Sgm dom fss2).k = (Sgm dom fss).((Sgm dom fss1).k) by A42,FUNCT_1:12;
A44: fss2 c= fss by A3,RELAT_1:59;
dom fss1 c= dom Seq fss by A1,RELAT_1:11;
then
A45: (Sgm dom fss1).k in dom Sgm dom fss by A40,FUNCT_1:11;
thus (Seq fss2).k = fss2.((Sgm dom fss2).k) by A36,A37,FUNCT_1:12
.= fss.((Sgm dom fss).((Sgm dom fss1).k)) by A43,A44,A39,GRFUNC_1:2
.= fss1.((Sgm dom fss1).k) by A45,A41,FUNCT_1:13
.= fs2.k by A2,A37,FUNCT_1:12;
end;
hence thesis by FINSEQ_1:13;
end;
begin :: Addenda
:: from AMISTD_1, 2006.01.12, A.T.
theorem
for f1 being non empty FinSequence of D, f2 being FinSequence of D
holds (f1^'f2)/.1 = f1/.1
proof
let f1 be non empty FinSequence of D, f2 be FinSequence of D;
A1: 1 in dom f1 by FINSEQ_5:6;
1 in dom (f1^(2, len f2)-cut f2) by FINSEQ_5:6;
hence (f1^'f2)/.1 = (f1^(2, len f2)-cut f2).1 by PARTFUN1:def 6
.= f1.1 by A1,FINSEQ_1:def 7
.= f1/.1 by A1,PARTFUN1:def 6;
end;
theorem
for f1 being FinSequence of D, f2 being non trivial FinSequence of D
holds (f1^'f2)/.len(f1^'f2) = f2/.len f2
proof
let f1 be FinSequence of D, f2 be non trivial FinSequence of D;
A1: len (f1^'f2) + 1 = len f1 + len f2 by Th13;
2 <= len f2 by NAT_D:60;
then
A2: 1 < len f2 by XXREAL_0:2;
then 1+0 < len f1 + len f2 by XREAL_1:8;
then 1 <= len(f1^'f2) by A1,NAT_1:13;
hence (f1^'f2)/.len(f1^'f2) = (f1^'f2).len(f1^'f2) by FINSEQ_4:15
.= f2.len f2 by A2,Th16
.= f2/.len f2 by A2,FINSEQ_4:15;
end;
theorem Th55:
for f being FinSequence holds f^'{} = f
proof
let f be FinSequence;
thus f^'{} = f^{} by Def1
.= f by FINSEQ_1:34;
end;
theorem
for f being FinSequence holds f^'<*x*> = f
proof
let f be FinSequence;
len <*x*> = 1 by FINSEQ_1:39;
then (2, len <*x*>)-cut <*x*> = {} by Def1;
hence thesis by FINSEQ_1:34;
end;
theorem :: GRAPH_2:14
for f1, f2 being FinSequence of D holds 1<=n & n<=len f1 implies
(f1^'f2)/.n = f1/.n
proof
let f1, f2 be FinSequence of D;
assume that
A1: 1<=n and
A2: n<=len f1;
per cases;
suppose
f2 = {};
hence thesis by Th55;
end;
suppose
A3: f2 <> {};
then
A4: len f1 + 0 < len f1 + len f2 by XREAL_1:6;
len (f1^'f2) + 1 = len f1 + len f2 by A3,Th13;
then n < len (f1^'f2) + 1 by A2,A4,XXREAL_0:2;
then n <= len (f1^'f2) by NAT_1:13;
hence (f1^'f2)/.n = (f1^'f2).n by A1,FINSEQ_4:15
.= f1.n by A1,A2,Th14
.= f1/.n by A1,A2,FINSEQ_4:15;
end;
end;
theorem :: GRAPH_2:15
for f1, f2 being FinSequence of D holds 1<=n & n<len f2 implies
(f1^'f2)/.(len f1 + n) = f2/.(n+1)
proof
let f1, f2 be FinSequence of D;
assume that
A1: 1<=n and
A2: n<len f2;
A3: n+1 <= len f2 by A2,NAT_1:13;
A4: now
per cases;
suppose
A5: f2 <> {};
A6: len f1 + n < len f1 + len f2 by A2,XREAL_1:6;
len (f1^'f2) + 1 = len f1 + len f2 by A5,Th13;
hence len f1+n <= len (f1^'f2) by A6,NAT_1:13;
end;
suppose
f2 = {};
hence len f1+n <= len (f1^'f2) by A2;
end;
end;
A7: 0+1 <= n+1 by XREAL_1:6;
0+1 <= len f1 + n by A1,XREAL_1:7;
hence (f1^'f2)/.(len f1 + n) = (f1^'f2).(len f1 + n) by A4,FINSEQ_4:15
.= f2.(n+1) by A1,A2,Th15
.= f2/.(n+1) by A7,A3,FINSEQ_4:15;
end;
:: from SFMASTR3, 2007.07.26, A.T.
definition
let F be FinSequence of INT, m, n be Nat;
assume that
A1: 1 <= m and
A2: m <= n and
A3: n <= len F;
func min_at(F, m, n) -> Nat means :Def11:
ex X being finite non empty Subset of INT st
X = rng ((m,n)-cut F) & it+1 = (min X)..(m,n)-cut F +m;
existence
proof
set Cut = (m,n)-cut F;
set X = rng Cut;
m < n+1 by A2,NAT_1:13;
then
A4: m-m < n+1-m by XREAL_1:9;
len Cut +m = n+1 by A1,A2,A3,Def1;
then
A5: Cut is non empty by A4;
rng (Cut qua Relation of NAT, INT) is Subset of INT;
then reconsider X as finite non empty Subset of INT by A5;
set q = (min X)..Cut +m -1;
1-1 <= m-1 by A1,XREAL_1:9;
then 0+0 <= (min X)..Cut + (m-1);
then reconsider q as Element of NAT by INT_1:3;
take q, X;
thus X = rng Cut;
thus thesis;
end;
uniqueness;
end;
reserve F, F1 for FinSequence of INT,
k, m, n, ma for Nat;
theorem Th59:
1 <= m & m <= n & n <= len F implies (ma = min_at(F, m, n) iff
m <= ma & ma <= n &
(for i being Nat st m <= i & i <= n holds F.ma <= F.i) &
for i being Nat st m <= i & i < ma holds F.ma < F.i)
proof
assume that
A1: 1 <= m and
A2: m <= n and
A3: n <= len F;
set Cut = (m,n)-cut F;
A4: len Cut +m = n+1 by A1,A2,A3,Def1;
hereby
A5: n-m < n-m+1 by XREAL_1:29;
assume ma = min_at(F, m, n);
then consider X being finite non empty Subset of INT such that
A6: X = rng Cut and
A7: ma+1 = (min X)..Cut +m by A1,A2,A3,Def11;
A8: ma = (min X)..Cut-1 +m by A7;
A9: ma = (min X)..Cut +m-1 by A7;
A10: min X in X by XXREAL_2:def 7;
then
A11: 1 <= (min X)..Cut by A6,FINSEQ_4:21;
then 1-1 <= (min X)..Cut-1 by XREAL_1:9;
then reconsider i1 = (min X)..Cut-1 as Element of NAT by INT_1:3;
A12: (min X)..Cut <= len Cut by A6,A10,FINSEQ_4:21;
then i1 < len Cut by XREAL_1:146,XXREAL_0:2;
then
A13: F.ma = Cut.(i1+1) by A1,A2,A3,A8,Def1
.= Cut.(ma+1-m) by A7;
(min X)..Cut+m <= len Cut +m by A12,XREAL_1:6;
then
A14: ma <= len Cut +m-1 by A9,XREAL_1:9;
m+1 <= (min X)..Cut +m by A11,XREAL_1:6;
then m+1-1 <= ma by A9,XREAL_1:9;
hence m <= ma & ma <= n by A4,A14;
A15: Cut.((min X)..Cut) = min X by A6,A10,FINSEQ_4:19;
thus
A16: for i being Nat st m <= i & i <= n holds F.ma <= F.i
proof
let i be Nat;
assume that
A17: m <= i and
A18: i <= n;
m-m <= i-m by A17,XREAL_1:9;
then reconsider i1 = i-m as Element of NAT by INT_1:3;
A19: 0+1 <= i1+1 by XREAL_1:6;
A20: n-m < n-m+1 by XREAL_1:29;
i1 <= n-m by A18,XREAL_1:9;
then
A21: i1 < len Cut by A4,A20,XXREAL_0:2;
then i1+1 <= len Cut by NAT_1:13;
then
A22: i1+1 in dom Cut by A19,FINSEQ_3:25;
Cut.(i1+1) = F.(m+i1) by A1,A2,A3,A21,Def1;
then F.i in rng Cut by A22,FUNCT_1:def 3;
hence thesis by A6,A7,A13,A15,XXREAL_2:def 7;
end;
let i be Nat;
assume that
A23: m <= i and
A24: i < ma;
A25: i <= n by A4,A14,A24,XXREAL_0:2;
then
A26: F.ma <= F.i by A16,A23;
m-m <= i-m by A23,XREAL_1:9;
then reconsider i1 = i-m as Element of NAT by INT_1:3;
reconsider k = i1+1 as Element of NAT;
i <= len Cut -1 +m by A14,A24,XXREAL_0:2;
then i-m <= len Cut -1 by XREAL_1:20;
then
A27: k <= len Cut by XREAL_1:19;
i1 <= n-m by A25,XREAL_1:9;
then
A28: i1 < len Cut by A4,A5,XXREAL_0:2;
0+1 <= k by XREAL_1:6;
then
A29: k in dom Cut by A27,FINSEQ_3:25;
i-m < ma-m by A24,XREAL_1:9;
then
A30: k < ma-m+1 by XREAL_1:6;
F.i = F.(i1+m) .= Cut.k by A1,A2,A3,A28,Def1;
then F.i <> F.ma by A6,A7,A10,A13,A30,A29,FINSEQ_4:19,24;
hence F.ma < F.i by A26,XXREAL_0:1;
end;
set Cut = (m,n)-cut F;
A31: len Cut +m = n+1 by A1,A2,A3,Def1;
then
A32: len Cut = n+1-m;
set X = rng Cut;
A33: rng (Cut qua Relation of NAT, INT) is Subset of INT;
m < n+1 by A2,NAT_1:13;
then m-m < n+1-m by XREAL_1:9;
then Cut is non empty by A31;
then reconsider X as finite non empty Subset of INT by A33;
reconsider rX = X as finite non empty Subset of REAL by MEMBERED:3;
assume that
A34: m <= ma and
A35: ma <= n and
A36: for i being Nat st m <= i & i <= n holds F.ma <= F.i and
A37: for i being Nat st m <= i & i < ma holds F.ma < F.i;
m-m <= ma-m by A34,XREAL_1:9;
then reconsider qm = ma-m as Element of NAT by INT_1:3;
A38: qm+1 = ma+1-m;
then reconsider q1 = ma+1-m as Element of NAT;
ma+1 <= n+1 by A35,XREAL_1:6;
then
A39: q1 <= len Cut by A32,XREAL_1:9;
0+1 <= qm+1 by XREAL_1:6;
then
A40: q1 in dom Cut by A39,FINSEQ_3:25;
A41: ma = qm+m;
qm < len Cut by A38,A39,NAT_1:13;
then
A42: F.ma = Cut.(ma+1-m) by A1,A2,A3,A38,A41,Def1;
now
thus F.ma in X by A40,A42,FUNCT_1:def 3;
let k be ExtReal;
assume k in X;
then consider dk being object such that
A43: dk in dom Cut and
A44: Cut.dk = k by FUNCT_1:def 3;
reconsider dk as Element of NAT by A43;
1 <= dk by A43,FINSEQ_3:25;
then 1-1 <= dk-1 by XREAL_1:9;
then reconsider dk1 = dk-1 as Element of NAT by INT_1:3;
A45: dk <= len Cut by A43,FINSEQ_3:25;
then dk+m <= (len Cut)+m by XREAL_1:6;
then
A46: dk+m-1 <= n by A4,XREAL_1:20;
dk1 < len Cut by A45,XREAL_1:146,XXREAL_0:2;
then F.(dk1+m) = Cut.(dk1+1) by A1,A2,A3,Def1
.= Cut.dk;
hence F.ma <= k by A36,A44,A46,NAT_1:12;
end;
then
A47: F.ma = min rX by XXREAL_2:def 7;
set mX = min X;
set mXC = mX..Cut;
A48: mX in X by XXREAL_2:def 7;
then 1 <= mXC by FINSEQ_4:21;
then 1-1 <= mXC -1 by XREAL_1:9;
then reconsider mXC1 = mXC-1 as Element of NAT by INT_1:3;
set mXCm = mXC1+m;
mXC <= len Cut by A48,FINSEQ_4:21;
then
A49: mXC1 < len Cut by XREAL_1:146,XXREAL_0:2;
mXC = mXC1+1;
then
A50: F.mXCm = Cut.mXC by A1,A2,A3,A49,Def1;
A51: m <= mXCm by NAT_1:12;
A52: Cut.(mX..Cut) = mX by A48,FINSEQ_4:19;
now
assume
A53: q1 <> mXC;
per cases by A53,XXREAL_0:1;
suppose
q1 < mXC;
hence contradiction by A40,A42,A47,FINSEQ_4:24;
end;
suppose
q1 > mXC;
then mXC+m < ma+1 by XREAL_1:20;
then mXC+m-1 < ma by XREAL_1:19;
hence contradiction by A37,A52,A47,A51,A50;
end;
end;
then ma+1 = mX..Cut +m;
hence thesis by A1,A2,A3,Def11;
end;
theorem
1 <= m & m <= len F implies min_at(F, m, m) = m
proof
assume that
A1: 1 <= m and
A2: m <= len F;
A3: for i being Nat st m <= i & i < m holds F.m < F.i;
for i being Nat st m <= i & i <= m holds F.m <= F.i by XXREAL_0:1;
hence thesis by A1,A2,A3,Th59;
end;
definition
let F be FinSequence of INT, m, n be Nat;
pred F is_non_decreasing_on m, n means
for i, j being Nat st m <= i & i <= j & j <= n holds F.i <= F.j;
end;
definition
let F be FinSequence of INT, n be Nat;
pred F is_split_at n means
for i, j being Nat st 1 <= i &
i <= n & n < j & j <= len F holds F.i <= F.j;
end;
theorem
k+1 <= len F & ma = min_at(F, k+1, len F) & F is_split_at k &
F is_non_decreasing_on 1, k & F1 = F+*(k+1, F.ma)+*(ma, F.(k+1))
implies F1 is_non_decreasing_on 1, k+1
proof
assume that
A1: k+1 <= len F and
A2: ma = min_at(F, k+1, len F) and
A3: F is_split_at k and
A4: F is_non_decreasing_on 1, k and
A5: F1 = F+*(k+1, F.ma)+*(ma, F.(k+1));
A6: 1 <= k+1 by NAT_1:12;
set Fk = F+*(k+1, F.ma);
A7: dom F1 = dom Fk by A5,FUNCT_7:30;
A8: dom Fk = dom F by FUNCT_7:30;
then
A9: k+1 in dom F1 by A1,A7,A6,FINSEQ_3:25;
let i, j be Nat such that
A10: 1 <= i and
A11: i <= j and
A12: j <= k+1;
A13: j <= len F by A1,A12,XXREAL_0:2;
1 <= j by A10,A11,XXREAL_0:2;
then
A14: j in dom F1 by A7,A8,A13,FINSEQ_3:25;
per cases by A12,XXREAL_0:1;
suppose
A15: j < k+1;
then i < k+1 by A11,XXREAL_0:2;
then i <> ma by A1,A2,A6,Th59;
then
A16: F1.i = Fk.i by A5,FUNCT_7:32
.= F.i by A11,A15,FUNCT_7:32;
j <> ma by A1,A2,A6,A15,Th59;
then
A17: F1.j = Fk.j by A5,FUNCT_7:32
.= F.j by A15,FUNCT_7:32;
j <= k by A15,NAT_1:13;
hence thesis by A4,A10,A11,A16,A17;
end;
suppose
A18: j = k+1;
thus F1.i <= F1.j
proof
per cases by A11,XXREAL_0:1;
suppose
A19: i < j;
then i <> ma by A1,A2,A6,A18,Th59;
then
A20: F1.i = Fk.i by A5,FUNCT_7:32
.= F.i by A18,A19,FUNCT_7:32;
A21: i <= k by A18,A19,NAT_1:13;
A22: k < j by A18,NAT_1:13;
thus F1.i <= F1.j
proof
per cases;
suppose
k+1 = ma;
then F1.j = F.(k+1) by A5,A7,A9,A18,FUNCT_7:31;
hence thesis by A1,A3,A10,A18,A20,A21,A22;
end;
suppose
A23: k+1 <> ma;
A24: ma <= len F by A1,A2,A6,Th59;
k+1 <= ma by A1,A2,A6,Th59;
then
A25: k < ma by NAT_1:13;
F1.j = Fk.j by A5,A18,A23,FUNCT_7:32
.= F.ma by A7,A8,A14,A18,FUNCT_7:31;
hence thesis by A3,A10,A20,A21,A25,A24;
end;
end;
end;
suppose
i = j;
hence thesis;
end;
end;
end;
end;
theorem
k+1 <= len F & ma = min_at(F, k+1, len F) & F is_split_at k &
F1 = F+*(k+1, F.ma)+*(ma, F.(k+1)) implies F1 is_split_at k+1
proof
assume that
A1: k+1 <= len F and
A2: ma = min_at(F, k+1, len F) and
A3: F is_split_at k and
A4: F1 = F+*(k+1, F.ma)+*(ma, F.(k+1));
A5: dom F1 = dom (F+*(k+1, F.ma)) by A4,FUNCT_7:30;
A6: k < k+1 by NAT_1:13;
A7: 1 <= k+1 by NAT_1:12;
let i, j be Nat;
assume that
A8: 1 <= i and
A9: i <= k+1 and
A10: k+1 < j and
A11: j <= len F1;
A12: k < j by A10,NAT_1:13;
A13: dom (F+*(k+1, F.ma)) = dom F by FUNCT_7:30;
then
A14: len F1 = len F by A5,FINSEQ_3:29;
then
A15: k+1 <= len F by A10,A11,XXREAL_0:2;
i <= len F1 by A1,A14,A9,XXREAL_0:2;
then
A16: i in dom F1 by A8,FINSEQ_3:25;
1 <= j by A10,NAT_1:12;
then
A17: j in dom F1 by A11,FINSEQ_3:25;
per cases by A9,XXREAL_0:1;
suppose
A18: i < k+1;
then i <> ma by A1,A2,A7,Th59;
then
A19: F1.i = (F+*(k+1, F.ma)).i by A4,FUNCT_7:32
.= F.i by A18,FUNCT_7:32;
A20: i <= k by A18,NAT_1:13;
thus F1.i <= F1.j
proof
per cases;
suppose
j <> ma;
then F1.j = (F+*(k+1, F.ma)).j by A4,FUNCT_7:32
.= F.j by A10,FUNCT_7:32;
hence thesis by A3,A14,A8,A11,A12,A20,A19;
end;
suppose
j = ma;
then F1.j = F.(k+1) by A4,A5,A17,FUNCT_7:31;
hence thesis by A3,A6,A8,A15,A20,A19;
end;
end;
end;
suppose
A21: i = k+1;
A22: F1.i = F.ma
proof
per cases;
suppose
k+1 = ma;
hence thesis by A4,A5,A16,A21,FUNCT_7:31;
end;
suppose
k+1 <> ma;
hence F1.i = (F+*(k+1, F.ma)).i by A4,A21,FUNCT_7:32
.= F.ma by A5,A13,A16,A21,FUNCT_7:31;
end;
end;
thus thesis
proof
per cases;
suppose
j = ma;
then F1.j = F.(k+1) by A4,A5,A17,FUNCT_7:31;
hence thesis by A1,A2,A7,A22,Th59;
end;
suppose
j <> ma;
then F1.j = (F+*(k+1, F.ma)).j by A4,FUNCT_7:32
.= F.j by A10,FUNCT_7:32;
hence thesis by A1,A2,A14,A7,A10,A11,A22,Th59;
end;
end;
end;
end;
:: from SCPISORT, 2011.02.13
theorem
for f being FinSequence of INT,m,n be Nat st m >= n
holds f is_non_decreasing_on m,n
proof
let f be FinSequence of INT,m,n be Nat;
assume
A1: m>=n;
let i, j be Nat such that
A2: m <= i & i <= j and
A3: j <= n;
A4: m <= j by A2,XXREAL_0:2;
per cases by A1,XXREAL_0:1;
suppose m=n;
then j=m by A3,A4,XXREAL_0:1;
hence f.i <= f.j by A2,XXREAL_0:1;
end;
suppose m>n;
hence thesis by A3,A4,XXREAL_0:2;
end;
end;
begin :: from REVROT_1
reserve i,j,k,m,n for Nat,
D for non empty set,
p for Element of D,
f for FinSequence of D;
definition
let D be non empty set;
let f be FinSequence of D;
redefine attr f is constant means :Def1: :: redefines constant (FUNCT_1, definition)
for n,m st n in dom f & m in dom f holds f/.n=f/.m;
compatibility
proof
hereby
assume
A1: f is constant;
let n,m such that
A2: n in dom f and
A3: m in dom f;
thus f/.n = f.n by A2,PARTFUN1:def 6
.= f.m by A1,A2,A3
.= f/.m by A3,PARTFUN1:def 6;
end;
assume
A4: for n,m st n in dom f & m in dom f holds f/.n=f/.m;
let n,m such that
A5: n in dom f and
A6: m in dom f;
thus f.n = f/.n by A5,PARTFUN1:def 6
.= f/.m by A4,A5,A6
.= f.m by A6,PARTFUN1:def 6;
end;
end;
theorem Th1:
for D being non empty set, f being FinSequence of D st
f just_once_values f/.len f holds f/.len f..f = len f
proof
let D be non empty set, f be FinSequence of D;
assume
A1: f just_once_values f/.len f;
then reconsider f9 = f as non empty FinSequence of D by FINSEQ_4:5,RELAT_1:38
;
f/.len f..f + 1 = f/.len f..f + ((Rev f9)/.1)..Rev f9 by Th43
.= f/.len f..f + f/.len f..Rev f by FINSEQ_5:65
.= len f + 1 by A1,Th37;
hence thesis;
end;
theorem
for D being non empty set, f being FinSequence of D holds
f /^ len f = {} by RFINSEQ:27;
theorem Th3:
for D being non empty set, f being non empty FinSequence of D
holds f/.len f in rng f
proof
let D be non empty set, f be non empty FinSequence of D;
len f in dom f by FINSEQ_5:6;
hence thesis by PARTFUN2:2;
end;
definition
let D be non empty set, f be FinSequence of D, y be set;
redefine pred f just_once_values y means :: redefines just_once_values (FINSEQ_4, definition)
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
proof
hereby
assume f just_once_values y;
then consider x being object such that
A1: x in dom f and
A2: y = f.x and
A3: for z being object st z in dom f & z <> x holds f.z <> y by FINSEQ_4:7;
reconsider x as set by TARSKI:1;
take x;
thus x in dom f by A1;
thus y = f/.x by A1,A2,PARTFUN1:def 6;
let z be set;
assume that
A4: z in dom f and
A5: z <> x;
f.z <> y by A3,A4,A5;
hence f/.z <> y by A4,PARTFUN1:def 6;
end;
given x being set such that
A6: x in dom f and
A7: y = f/.x and
A8: for z being set st z in dom f & z <> x holds f/.z <> y;
A9: for z being object st z in dom f & z <> x holds f.z <> y
proof
let z be object;
assume that
A10: z in dom f and
A11: z <> x;
f/.z <> y by A8,A10,A11;
hence thesis by A10,PARTFUN1:def 6;
end;
y = f.x by A6,A7,PARTFUN1:def 6;
hence thesis by A6,A9,FINSEQ_4:7;
end;
end;
theorem Th4:
for D being non empty set, f being FinSequence of D st
f just_once_values f/.len f holds f-:f/.len f = f
proof
let D be non empty set, f be FinSequence of D;
assume
A1: f just_once_values f/.len f;
thus f-:f/.len f = f|(f/.len f..f) by FINSEQ_5:def 1
.= f|len f by A1,Th1
.= f by FINSEQ_1:58;
end;
theorem Th5:
for D being non empty set, f being FinSequence of D st
f just_once_values f/.len f holds f:-f/.len f = <*f/.len f*>
proof
let D be non empty set, f be FinSequence of D;
assume
A1: f just_once_values f/.len f;
thus f:-f/.len f = <*f/.len f*>^(f/^f/.len f..f) by FINSEQ_5:def 2
.= <*f/.len f*>^(f/^len f) by A1,Th1
.= <*f/.len f*>^{} by RFINSEQ:27
.= <*f/.len f*> by FINSEQ_1:34;
end;
theorem Th6:
1 <= len (f:-p)
proof
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;
hence thesis by NAT_1:11;
end;
theorem
for D being non empty set, p being Element of D,
f being FinSequence of D st p in rng f holds
len(f:-p) <= len f
proof
let D be non empty set, p be Element of D, f be FinSequence of D;
assume
A1: p in rng f;
then 1 <= p..f by FINSEQ_4:21;
then
A2: len f - 1 >= len f - p..f by XREAL_1:10;
len (f:-p) = len f - p..f + 1 by A1,FINSEQ_5:50;
then len (f:-p) - 1 = len f - p..f;
hence thesis by A2,XREAL_1:9;
end;
theorem
for D being non empty set, f being circular non empty FinSequence of D
holds Rev f is circular
proof
let D be non empty set, f be circular non empty FinSequence of D;
thus (Rev f)/.1 = f/.len f by FINSEQ_5:65
.= f/.1 by Def1A
.= (Rev f)/.len f by FINSEQ_5:65
.= (Rev f)/.len Rev f by FINSEQ_5:def 3;
end;
begin :: About Rotation
reserve D for non empty set,
p for Element of D,
f for FinSequence of D;
theorem Th9:
p in rng f & 1 <= i & i <= len(f:-p) implies (Rotate(f,p))/.i = f
/.(i -' 1 + p..f)
proof
assume that
A1: p in rng f and
A2: 1 <= i and
A3: i <= len(f:-p);
A4: i in dom(f:-p) by A2,A3,FINSEQ_3:25;
A5: i = i -' 1 + 1 by A2,XREAL_1:235;
Rotate(f,p) = (f:-p)^((f-:p)/^1) by A1,Def2;
hence (Rotate(f,p))/.i = (f:-p)/.i by A4,FINSEQ_4:68
.= f/.(i -' 1 + p..f) by A1,A5,A4,FINSEQ_5:52;
end;
theorem Th10:
p in rng f & p..f <= i & i <= len f implies
f/.i = (Rotate(f,p))/.(i+1 -' p..f)
proof
assume that
A1: p in rng f and
A2: p..f <= i and
A3: i <= len f;
A4: 1 + p..f <= i+1 by A2,XREAL_1:6;
i+1 <= len f + 1 by A3,XREAL_1:6;
then i <= i+1 & i+1 - p..f <= len f + 1 - p..f by NAT_1:11,XREAL_1:9;
then i+1 -' p..f <= len f - p..f + 1 by A2,XREAL_1:233,XXREAL_0:2;
then
A5: i+1 -' p..f <= len(f:-p) by A1,FINSEQ_5:50;
i+1 -' p..f -' 1 + p..f = i -' p..f+1 -' 1 + p..f by A2,NAT_D:38
.= i -' p..f + p..f by NAT_D:34
.= i by A2,XREAL_1:235;
hence thesis by A1,A4,A5,Th9,NAT_D:55;
end;
theorem
p in rng f implies (Rotate(f,p))/.len(f:-p) = f/.len f
proof
A1: 1 <= len (f:-p) by Th6;
assume
A2: p in rng f;
then p..f <= len f by FINSEQ_4:21;
then reconsider x = len f - p..f as Element of NAT by INT_1:5;
len (f:-p) -' 1 + p..f = x + 1 -' 1 + p..f by A2,FINSEQ_5:50
.= len f - p..f + p..f by NAT_D:34
.= len f;
hence thesis by A1,A2,Th9;
end;
NAT27: ::: proof copied from NAT_2:7
j < i implies i-'(j+1)+1 = i -' j
proof
assume
A1: j < i;
then j + 1 <= i by NAT_1:13;
hence i -' (j+1) + 1 = i - (j+1) + 1 by XREAL_1:233
.= i - j
.= i -' j by A1,XREAL_1:233;
end;
theorem Th12:
p in rng f & len(f:-p) < i & i <= len f implies
(Rotate(f,p))/.i = f/.(i + p..f -' len f)
proof
assume that
A1: p in rng f and
A2: len(f:-p) < i and
A3: i <= len f;
A4: len(f-:p) = p..f by A1,FINSEQ_5:42;
A5: i -' len(f:-p) + len(f:-p) = i & Rotate(f,p) = (f:-p)^((f-:p)/^1) by A1,A2,
Def2,XREAL_1:235;
f-:p is non empty by A1,FINSEQ_5:47;
then len(f-:p) >= 1 by NAT_1:14;
then
A6: len((f-:p)/^1) = len(f-:p)-1 by RFINSEQ:def 1;
i + p..f <= p..f + len f by A3,XREAL_1:6;
then
A7: i + p..f -' len f <= p..f by NAT_D:53;
A8: p..f <= len f by A1,FINSEQ_4:21;
then len f - p..f = len f -' p..f by XREAL_1:233;
then
A9: len(f:-p) = len f -' p..f + 1 by A1,FINSEQ_5:50;
then
A10: len f -' p..f < i by A2,NAT_1:13;
then
A11: len f < i + p..f by NAT_D:55;
then len f + 1 <= i + p..f by NAT_1:13;
then 1 <= i + p..f -' len f by NAT_D:55;
then
A12: i + p..f -' len f in Seg(p..f) by A7;
i <= p..f + (len f -' p..f) by A3,A8,XREAL_1:235;
then i -' (len f -' p..f) <= p..f by NAT_D:53;
then i -' (len f -' p..f + 1) + 1 <= p..f by A10,NAT27;
then
A13: i -' len(f:-p) <= len(f-:p)-1 by A9,A4,XREAL_1:19;
len f -' p..f + 1 + 1 <= i by A2,A9,NAT_1:13;
then
A14: 1 <= i -' (len f -' p..f + 1) by NAT_D:55;
then
A15: i -' (len f -' p..f + 1) in dom((f-:p)/^1) by A9,A6,A13,FINSEQ_3:25;
len f - p..f = len f -' p..f by A8,XREAL_1:233;
then 1 <= i -' len(f:-p) by A1,A14,FINSEQ_5:50;
then i -' len(f:-p) in dom((f-:p)/^1) by A6,A13,FINSEQ_3:25;
hence (Rotate(f,p))/.i = ((f-:p)/^1)/.(i -' (len f -' p..f + 1)) by A9,A5,
FINSEQ_4:69
.= (f-:p)/.(i -' (len f -' p..f + 1) + 1) by A15,FINSEQ_5:27
.= (f-:p)/.(i -' (len f -' p..f)) by A10,NAT27
.= (f-:p)/.(i - (len f -' p..f)) by A10,XREAL_1:233
.= (f-:p)/.(i - (len f - p..f)) by A8,XREAL_1:233
.= (f-:p)/.(i + p..f - len f)
.= (f-:p)/.(i + p..f -' len f) by A11,XREAL_1:233
.= f/.(i + p..f -' len f) by A1,A12,FINSEQ_5:43;
end;
theorem
p in rng f & 1 < i & i <= p..f implies
f/.i = (Rotate(f,p))/.(i + len f -' p..f)
proof
assume that
A1: p in rng f and
A2: 1 < i and
A3: i <= p..f;
A4: len f -' p..f <= len f -' i by A3,NAT_D:41;
A5: p..f <= len f by A1,FINSEQ_4:21;
then i <= len f by A3,XXREAL_0:2;
then len f -' p..f + i <= len f by A4,NAT_D:54;
then
A6: i + len f -' p..f <= len f by A5,NAT_D:38;
len f + 1 < i + len f by A2,XREAL_1:6;
then len f + 1 - p..f < i + len f - p..f by XREAL_1:9;
then len f - p..f + 1 < i + (len f - p..f);
then len f - p..f + 1 < i + (len f -' p..f) by A5,XREAL_1:233;
then len f - p..f + 1 < i + len f -' p..f by A5,NAT_D:38;
then
A7: len(f:-p) < i + len f -' p..f by A1,FINSEQ_5:50;
len f <= i + len f by NAT_1:11;
then i + len f -' p..f + p..f -' len f = i + len f -' len f by A5,XREAL_1:235
,XXREAL_0:2
.= i by NAT_D:34;
hence thesis by A1,A7,A6,Th12;
end;
theorem Th14:
len Rotate(f,p) = len f
proof
per cases;
suppose
not p in rng f;
hence thesis by Def2;
end;
suppose
A1: p in rng f;
then f-:p <> {} by FINSEQ_5:47;
then
A2: 1 <= len(f-:p) by NAT_1:14;
thus len Rotate(f,p) = len((f:-p)^((f-:p)/^1)) by A1,Def2
.= len(f:-p) + len((f-:p)/^1) by FINSEQ_1:22
.= len(f:-p) + (len(f-:p)-1) by A2,RFINSEQ:def 1
.= len(f:-p) + len(f-:p)-1
.= len f - p..f + 1 + len(f-:p)-1 by A1,FINSEQ_5:50
.= len f - p..f + len(f-:p)
.= len f - p..f + p..f by A1,FINSEQ_5:42
.= len f;
end;
end;
theorem Th15:
dom Rotate(f,p) = dom f
proof
len Rotate(f,p) = len f by Th14;
hence thesis by FINSEQ_3:29;
end;
theorem
for D being non empty set, f being circular FinSequence of D,
p be Element of D st for i st 1 < i & i < len f holds
f/.i <> f/.1 holds Rotate(Rotate(f,p),f/.1) = f
proof
let D be non empty set, f be circular FinSequence of D, p be Element of D
such that
A1: for i st 1 < i & i < len f holds f/.i <> f/.1;
per cases;
suppose
not p in rng f;
hence Rotate(Rotate(f,p),f/.1) = Rotate(f,f/.1) by Def2
.= f by Th89;
end;
suppose
p = f/.1;
hence Rotate(Rotate(f,p),f/.1) = Rotate(f,f/.1) by Th93
.= f by Th89;
end;
suppose that
A2: p in rng f and
A3: p <> f/.1;
A4: f/.1 = (f-:p)/.1 by A2,FINSEQ_5:44;
A5: f/.1 = f/.len f by Def1A;
then
A6: f/.1 = (f:-p)/.len(f:-p) by A2,FINSEQ_5:54;
then
A7: f/.1 in rng(f:-p) by Th3;
A8: f:-p just_once_values f/.1
proof
p..f <> 1 & p..f >= 1 by A2,A3,FINSEQ_4:21,FINSEQ_5:38;
then
A9: p..f > 1 by XXREAL_0:1;
take len(f:-p);
thus len(f:-p) in dom(f:-p) by FINSEQ_5:6;
thus f/.1 = (f:-p)/.len(f:-p) by A2,A5,FINSEQ_5:54;
let z be set;
assume
A10: z in dom(f:-p);
then reconsider k = z as Element of NAT;
k <> 0 by A10,FINSEQ_3:25;
then consider i being Nat such that
A11: k = i+1 by NAT_1:6;
assume
A12: z <> len(f:-p);
reconsider i as Element of NAT by ORDINAL1:def 12;
k <= len(f:-p) by A10,FINSEQ_3:25;
then k < len(f:-p) by A12,XXREAL_0:1;
then i + 1 < len f - p..f + 1 by A2,A11,FINSEQ_5:50;
then i < len f - p..f by XREAL_1:6;
then
A13: i + p..f < len f by XREAL_1:20;
p..f <= i+p..f by NAT_1:11;
then
A14: 1 < i+p..f by A9,XXREAL_0:2;
(f:-p)/.(i+1) = f/.(i+p..f) by A2,A10,A11,FINSEQ_5:52;
hence thesis by A1,A11,A14,A13;
end;
f/.1 in rng f by A2,Th42,RELAT_1:38;
then
A15: f/.1 in rng Rotate(f,p) by A2,Th90;
Rotate(f,p) = (f:-p)^((f-:p)/^1) by A2,Def2;
hence Rotate(Rotate(f,p),f/.1) =
((f:-p)^((f-:p)/^1)):-(f/.1)^ (((f:-p)^((f-:p)/^1)-:(f/.1))/^1)
by A15,Def2
.= (f:-p):-(f/.1)^((f-:p)/^1)^ (((f:-p)^((f-:p)/^1)-:(f/.1))/^1)
by A7,Th64
.= (f:-p):-(f/.1)^((f-:p)/^1)^ (((f:-p)-:(f/.1))/^1) by A7,Th66
.= <* f/.1 *>^((f-:p)/^1)^ (((f:-p)-:(f/.1))/^1) by A6,A8,Th5
.= (f-:p)^(((f:-p)-:(f/.1))/^1) by A2,A4,FINSEQ_5:29,47
.= (f-:p)^((f:-p)/^1) by A6,A8,Th4
.= f by A2,Th76;
end;
end;
begin :: Rotating circular
reserve f for circular FinSequence of D;
theorem Th17:
p in rng f & len(f:-p) <= i & i <= len f implies
(Rotate(f,p))/.i = f/.(i + p..f -' len f)
proof
assume that
A1: p in rng f and
A2: len(f:-p) <= i and
A3: i <= len f;
A4: p..f <= len f by A1,FINSEQ_4:21; then
A5: len f - p..f = len f -' p..f by XREAL_1:233;
per cases by A2,XXREAL_0:1;
suppose
A6: i = len(f:-p); then
A7: i = len f - p..f + 1 by A1,FINSEQ_5:50;
then i >= 1 by A5,NAT_1:11;
hence (Rotate(f,p))/.i = f/.(i -' 1 + p..f) by A1,A6,Th9
.= f/.(len f -' p..f + p..f) by A5,A7,NAT_D:34
.= f/.len f by A4,XREAL_1:235
.= f/.1 by Def1A
.= f/.(len f + 1 -' len f) by NAT_D:34
.= f/.(i + p..f -' len f) by A7;
end;
suppose
i > len(f:-p);
hence thesis by A1,A3,Th12;
end;
end;
theorem Th18:
p in rng f & 1 <= i & i <= p..f implies
f/.i = (Rotate(f,p))/.(i + len f -' p..f)
proof
assume that
A1: p in rng f and
A2: 1 <= i and
A3: i <= p..f;
A4: len f -' p..f <= len f -' i by A3,NAT_D:41;
A5: p..f <= len f by A1,FINSEQ_4:21;
then i <= len f by A3,XXREAL_0:2;
then len f -' p..f + i <= len f by A4,NAT_D:54;
then
A6: i + len f -' p..f <= len f by A5,NAT_D:38;
len f + 1 <= i + len f by A2,XREAL_1:6;
then len f + 1 - p..f <= i + len f - p..f by XREAL_1:9;
then len f - p..f + 1 <= i + (len f - p..f);
then len f - p..f + 1 <= i + (len f -' p..f) by A5,XREAL_1:233;
then len f - p..f + 1 <= i + len f -' p..f by A5,NAT_D:38;
then
A7: len(f:-p) <= i + len f -' p..f by A1,FINSEQ_5:50;
len f <= i + len f by NAT_1:11;
then i + len f -' p..f + p..f -' len f = i + len f -' len f
by A5,XREAL_1:235,XXREAL_0:2
.= i by NAT_D:34;
hence thesis by A1,A7,A6,Th17;
end;
registration
let D be non trivial set;
cluster non constant circular for FinSequence of D;
existence
proof
consider d1,d2 being Element of D such that
A1: d1 <> d2 by SUBSET_1:def 7;
take f = <*d1,d2,d1*>;
A2: f.1 = d1 & f.2 = d2;
1 in dom f & 2 in dom f by FINSEQ_1:81;
hence f is not constant by A1,A2;
A3: len f = 3 by FINSEQ_1:45;
thus f/.1 = d1 by FINSEQ_4:18
.= f/.len f by A3,FINSEQ_4:18;
end;
end;
registration
let D be non trivial set, p be Element of D;
let f be non constant circular FinSequence of D;
cluster Rotate(f,p) -> non constant;
coherence
proof
per cases;
suppose
not p in rng f;
hence thesis by Def2;
end;
suppose
A1: p in rng f;
A2: dom Rotate(f,p) = dom f by Th15;
consider n,m such that
A3: n in dom f and
A4: m in dom f and
A5: f/.n <> f/.m by Def1;
A6: n <= len f by A3,FINSEQ_3:25;
A7: m <= len f by A4,FINSEQ_3:25;
A8: 1 <= m by A4,FINSEQ_3:25;
A9: 1 <= n by A3,FINSEQ_3:25;
thus Rotate(f,p) is not constant
proof
A10: 1 <= p..f by A1,FINSEQ_4:21;
A11: p..f <= len f by A1,FINSEQ_4:21;
per cases;
suppose that
A12: n <= p..f and
A13: m <= p..f;
n <= n + (len f -' p..f) by NAT_1:11;
then 1 <= n + (len f -' p..f) by A9,XXREAL_0:2;
then
A14: 1 <= n + len f -' p..f by A11,NAT_D:38;
m <= m + (len f -' p..f) by NAT_1:11;
then 1 <= m + (len f -' p..f) by A8,XXREAL_0:2;
then
A15: 1 <= m + len f -' p..f by A11,NAT_D:38;
m + len f <= len f + p..f by A13,XREAL_1:6;
then m + len f -' p..f <= len f by NAT_D:53;
then
A16: m + len f -' p..f in dom f by A15,FINSEQ_3:25;
n + len f <= len f + p..f by A12,XREAL_1:6;
then n + len f -' p..f <= len f by NAT_D:53;
then
A17: n + len f -' p..f in dom f by A14,FINSEQ_3:25;
f/.n = (Rotate(f,p))/.(n + len f -' p..f) & f/.m = (Rotate(f,p)
)/.(m + len f -' p..f) by A1,A9,A8,A12,A13,Th18;
hence thesis by A5,A2,A17,A16;
end;
suppose that
A18: n <= p..f and
A19: m >= p..f;
1 + p..f <= m + 1 by A19,XREAL_1:6;
then
A20: 1 <= m + 1 -' p..f by NAT_D:55;
n <= n + (len f -' p..f) by NAT_1:11;
then 1 <= n + (len f -' p..f) by A9,XXREAL_0:2;
then
A21: 1 <= n + len f -' p..f by A11,NAT_D:38;
n + len f <= len f + p..f by A18,XREAL_1:6;
then n + len f -' p..f <= len f by NAT_D:53;
then
A22: n + len f -' p..f in dom f by A21,FINSEQ_3:25;
m + 1 <= len f + p..f by A7,A10,XREAL_1:7;
then m + 1 -' p..f <= len f by NAT_D:53;
then
A23: m + 1 -' p..f in dom f by A20,FINSEQ_3:25;
f/.n = (Rotate(f,p))/.(n + len f -' p..f) & f/.m = (Rotate(f,p)
)/.(m + 1 -' p..f) by A1,A9,A7,A18,A19,Th10,Th18;
hence thesis by A5,A2,A22,A23;
end;
suppose that
A24: m <= p..f and
A25: n >= p..f;
1 + p..f <= n + 1 by A25,XREAL_1:6;
then
A26: 1 <= n + 1 -' p..f by NAT_D:55;
m <= m + (len f -' p..f) by NAT_1:11;
then 1 <= m + (len f -' p..f) by A8,XXREAL_0:2;
then
A27: 1 <= m + len f -' p..f by A11,NAT_D:38;
m + len f <= len f + p..f by A24,XREAL_1:6;
then m + len f -' p..f <= len f by NAT_D:53;
then
A28: m + len f -' p..f in dom f by A27,FINSEQ_3:25;
n + 1 <= len f + p..f by A6,A10,XREAL_1:7;
then n + 1 -' p..f <= len f by NAT_D:53;
then
A29: n + 1 -' p..f in dom f by A26,FINSEQ_3:25;
f/.m = (Rotate(f,p))/.(m + len f -' p..f) & f/.n = (Rotate(f,p)
)/.(n + 1 -' p..f) by A1,A6,A8,A24,A25,Th10,Th18;
hence thesis by A5,A2,A28,A29;
end;
suppose that
A30: m >= p..f and
A31: n >= p..f;
1 + p..f <= m + 1 by A30,XREAL_1:6;
then
A32: 1 <= m + 1 -' p..f by NAT_D:55;
1 + p..f <= n + 1 by A31,XREAL_1:6;
then
A33: 1 <= n + 1 -' p..f by NAT_D:55;
n + 1 <= len f + p..f by A6,A10,XREAL_1:7;
then n + 1 -' p..f <= len f by NAT_D:53;
then
A34: n + 1 -' p..f in dom f by A33,FINSEQ_3:25;
m + 1 <= len f + p..f by A7,A10,XREAL_1:7;
then m + 1 -' p..f <= len f by NAT_D:53;
then
A35: m + 1 -' p..f in dom f by A32,FINSEQ_3:25;
f/.m = (Rotate(f,p))/.(m + 1 -' p..f) & f/.n = (Rotate(f,p))/.(
n + 1 -' p..f ) by A1,A6,A7,A30,A31,Th10;
hence thesis by A5,A2,A35,A34;
end;
end;
end;
end;
end;
begin :: Moved from JORDAN4, 2023.01.14, S.K.
reserve i, i1, i2, j, k for Nat;
reserve D for non empty set,
f1 for FinSequence of D;
theorem
for f1 st f1 is circular & 1<=len f1 holds f1.1=f1.len f1
proof
let f1;
assume that
A1: f1 is circular and
A2: 1<=len f1;
A3: f1.1=f1/.1 by A2,FINSEQ_4:15;
f1/.1=f1/.len f1 by A1;
hence thesis by A2,A3,FINSEQ_4:15;
end;
theorem
for f1,k st k<len f1 holds (f1/^k).len (f1/^k)=f1.len f1 &
(f1/^k)/.len (f1/^k)=f1/.len f1
proof
let f1,k;
assume
A1: k<len f1;
then k+1<=len f1 by NAT_1:13;
then k+1-k<=len f1-k by XREAL_1:9;
then
A2: 1<=len (f1/^k) by A1,RFINSEQ:def 1;
then len (f1/^k) in Seg len (f1/^k);
then
A3: len (f1/^k) in dom (f1/^k) by FINSEQ_1:def 3;
len (f1/^k)+k=len f1-k+k by A1,RFINSEQ:def 1
.=len f1;
hence
A4: (f1/^k).len (f1/^k)=f1.len f1 by A1,A3,RFINSEQ:def 1;
A5: (f1/^k)/.len (f1/^k)=(f1/^k).len (f1/^k) by A2,FINSEQ_4:15;
0+1<=len f1 by A1,NAT_1:13;
hence thesis by A4,A5,FINSEQ_4:15;
end;
theorem
for f1,i1,i2 st 1<=i2 & i2<=i1 & i1<=len f1 holds
len mid(f1,i2, i1)=i1-'i2+1
proof
let f1,i1,i2;
assume that
A1: 1<= i2 and
A2: i2<=i1 and
A3: i1<= len f1;
A4: i2<=len f1 by A2,A3,XXREAL_0:2;
1<=i1 by A1,A2,XXREAL_0:2;
hence thesis by A1,A2,A3,A4,Th117;
end;
theorem Th9:
for f1,i1,i2 st 1<=i2 & i2<=i1 & i1<=len f1 holds
len mid(f1,i1, i2)=i1-'i2+1
proof
let f1,i1,i2;
assume that
A1: 1<= i2 and
A2: i2<=i1 and
A3: i1<= len f1;
per cases by A2,XXREAL_0:1;
suppose
i1=i2;
hence thesis by A1,A3,Th117;
end;
suppose
A4: i2<i1;
A5: i2<=len f1 by A2,A3,XXREAL_0:2;
1<=i1 by A1,A2,XXREAL_0:2;
hence thesis by A1,A3,A4,A5,Th117;
end;
end;
theorem Th10:
for f1,i1,i2,j st 1<=i1 & i1<=i2 & i2<=len f1 holds
mid(f1,i1,i2).(len mid(f1,i1,i2))=f1.i2
proof
let f1,i1,i2,j;
assume that
A1: 1<=i1 and
A2: i1<=i2 and
A3: i2<=len f1;
A4: i1<=len f1 by A2,A3,XXREAL_0:2;
A5: 1<=i2 by A1,A2,XXREAL_0:2;
then len mid(f1,i1,i2)=i2-'i1+1 by A1,A2,A3,A4,Th117;
then 1<=len mid(f1,i1,i2) by NAT_1:11;
then
A6: mid(f1,i1,i2).(len mid(f1,i1,i2)) =f1.(len mid(f1,i1,i2)+i1-'1) by A1,A2,A3
,A5,A4,Th117
.=f1.(i2-'i1+1+i1-'1) by A1,A2,A3,A5,A4,Th117;
i2-'i1+1+i1=i2-i1+1+i1 by A2,XREAL_1:233
.=i2+1;
hence thesis by A6,NAT_D:34;
end;
theorem
for f1,i1,i2,j st 1<=i1 & i1<=len f1 & 1<=i2 & i2<=len f1 holds
mid(f1,i1,i2).(len mid(f1,i1,i2))=f1.i2
proof
let f1,i1,i2,j;
assume that
A1: 1<=i1 and
A2: i1<=len f1 and
A3: 1<=i2 and
A4: i2<=len f1;
per cases;
suppose
i1<=i2;
hence thesis by A1,A4,Th10;
end;
suppose
A5: i1>i2;
0<=i2-1 by A3,XREAL_1:48;
then i1-0>=i1-(i2-1) by XREAL_1:10;
then i1>=i1-i2+1;
then i1-'i2+1<=i1 by A5,XREAL_1:233;
then
A6: i1-'(i1-'i2+1)+1=i1-(i1-'i2+1)+1 by XREAL_1:233
.=i1-(i1-'i2)
.=i1-(i1-i2) by A5,XREAL_1:233
.=i2;
len mid(f1,i1,i2)=i1-'i2+1 by A1,A2,A3,A4,A5,Th117;
then 1<=len mid(f1,i1,i2) by NAT_1:11;
then
mid(f1,i1,i2).(len mid(f1,i1,i2)) =f1.(i1-'len mid(f1,i1,i2)+1) by A1,A2,A3
,A4,A5,Th117
.=f1.(i1-'(i1-'i2+1)+1) by A1,A2,A3,A4,A5,Th117;
hence thesis by A6;
end;
end;
theorem
for f1,i1,i2,j st 1<=i2 & i2<=i1 & i1<=len f1 & 1<=j & j<=i1-'i2+1 holds
mid(f1,i1,i2).j=f1.(i1-'j+1)
proof
let f1,i1,i2,j;
assume that
A1: 1<= i2 and
A2: i2<=i1 and
A3: i1<= len f1 and
A4: 1<=j and
A5: j<=i1-'i2+1;
A6: j<=len mid(f1,i1,i2) by A1,A2,A3,A5,Th9;
per cases by A2,XXREAL_0:1;
suppose
A7: i1=i2;
then
A8: i1-'i2+1=0+1 by XREAL_1:232
.=1;
then j+i1-'1=1+i1-'1 by A4,A5,XXREAL_0:1
.=1+i1-1 by NAT_D:37
.=i1-1+1
.=i1-'1+1 by A1,A7,XREAL_1:233
.=i1-'j+1 by A4,A5,A8,XXREAL_0:1;
hence thesis by A1,A3,A4,A6,A7,Th117;
end;
suppose
A9: i2<i1;
A10: i2<=len f1 by A2,A3,XXREAL_0:2;
1<=i1 by A1,A2,XXREAL_0:2;
hence thesis by A1,A3,A4,A6,A9,A10,Th117;
end;
end;
theorem Th13:
for f1,i1,i2 st 1<=i2 & i2<=i1 & i1<=len f1 & 1<=j & j<=i1-'i2+1 holds
mid(f1,i1,i2).j=mid(f1,i2,i1).(i1-i2+1-j+1) & i1-i2+1-j+1=i1-'i2+1-'j+1
proof
let f1,i1,i2;
assume that
A1: 1<=i2 and
A2: i2<=i1 and
A3: i1<=len f1 and
A4: 1<=j and
A5: j<=i1-'i2+1;
A6: 1<=i1 by A1,A2,XXREAL_0:2;
i2-1>=0 by A1,XREAL_1:48;
then
A7: i1-(i2-1)<=i1-0 by XREAL_1:10;
A8: i2<=len f1 by A2,A3,XXREAL_0:2;
1-j<=j-j by A4,XREAL_1:9;
then
A9: i1-'i2+(1-j)<=i1-'i2+0 by XREAL_1:7;
j-j<=i1-'i2+1-j by A5,XREAL_1:9;
then i1-'i2+1-'j<=i1-'i2 by A9,XREAL_0:def 2;
then
A10: i1-'i2+1-'j+1<=i1-'i2+1 by XREAL_1:6;
A11: 1<=(i1-'i2+1-'j+1) by NAT_1:11;
A12: (i1-'i2+1-'j+1) =i1-'i2+1-j+1 by A5,XREAL_1:233
.=i1-i2+1-j+1 by A2,XREAL_1:233;
A13: i1-'i2+1=i1-i2+1 by A2,XREAL_1:233;
now
per cases by A2,XXREAL_0:1;
case
A14: i1>i2;
len mid(f1,i2,i1)=i1-'i2+1 by A1,A2,A3,A6,A8,Th117;
then
A15: mid(f1,i2,i1).(i1-'i2+1-'j+1)=f1.((i1-'i2+1-'j+1)+i2-'1) by A1,A2,A3,A6
,A8,A10,A11,Th117;
A16: len mid(f1,i1,i2)=i1-'i2+1 by A1,A3,A6,A8,A14,Th117;
(i1-'i2+1-'j+1)+i2-'1 =(i1-'i2+1-'j+1)+i2-1 by A1,NAT_D:37
.=i1-j+1 by A12
.=i1-'j+1 by A5,A13,A7,XREAL_1:233,XXREAL_0:2;
hence thesis by A1,A3,A4,A5,A6,A8,A12,A14,A15,A16,Th117;
end;
case
A17: i1=i2;
then i1-'i2+1=0+1 by XREAL_1:232
.=1;
then i1-i2+1-j+1=0+1-1+1 by A4,A5,A17,XXREAL_0:1
.=1;
hence thesis by A12,A17;
end;
end;
hence thesis;
end;
theorem
for f1,i1,i2 st 1<=i1 & i1<=i2 & i2<=len f1 & 1<=j & j<=i2-'i1+1 holds
mid(f1,i1,i2).j=mid(f1,i2,i1).(i2-i1+1-j+1) & i2-i1+1-j+1=i2-'i1+1-'j+1
proof
let f1,i1,i2;
assume that
A1: 1<=i1 and
A2: i1<=i2 and
A3: i2<=len f1 and
A4: 1<=j and
A5: j<=i2-'i1+1;
set k=i2-'i1+1-'j+1;
i2-i1+1-j+1=i2-'i1+1-j+1 by A2,XREAL_1:233
.=i2-'i1+1-'j+1 by A5,XREAL_1:233;
then
A6: i2-i1+1-k+1=j;
j-1>=0 by A4,XREAL_1:48;
then
A7: k+0<=k+(j-1) by XREAL_1:7;
A8: 1<=k by NAT_1:11;
i2-'i1+1-j=i2-'i1+1-'j by A5,XREAL_1:233;
hence thesis by A1,A2,A3,A8,A7,A6,Th13;
end;
theorem Th15:
for f1 being FinSequence st
k in dom f1 holds mid(f1,k,k)=<*f1.k*> & len mid(f1,k,k)=1
proof
let f1 be FinSequence;
assume
A0: k in dom f1; then
A1: 1<=k by FINSEQ_3:25;
A2: k<=len f1 by A0,FINSEQ_3:25;
k-'1+1<=len f1 by A1,A2,XREAL_1:235;
then
A4: k-'1+1-(k-'1)<=len f1-(k-'1) by XREAL_1:9;
len (f1/^(k-'1))=len f1-'(k-'1) by RFINSEQ:29;
then
A5: 1<=len (f1/^(k-'1)) by A4,NAT_D:39;
k-'1+1=k by A1,XREAL_1:235;
then
A6: (f1/^(k-'1)).1=f1.k by A2,Th113;
k-'k+1=k-k+1 by XREAL_1:233
.=1;
then mid(f1,k,k)=(f1/^(k-'1))|1 by Def3
.=<*(f1/^(k-'1)).1*> by A5,CARD_1:27,FINSEQ_5:20;
hence thesis by A6,FINSEQ_1:39;
end;
theorem Th16:
for f1 being FinSequence holds mid(f1,0,0)=f1|1
proof
let f1 be FinSequence;
0-1<0;
then
A1: 0-'1=0 by XREAL_0:def 2;
0-'0+1=0-0+1 by XREAL_1:233
.=1;
then mid(f1,0,0)=(f1/^(0-'1))|1 by Def3;
hence thesis by A1;
end;
theorem Th17:
for f1 being FinSequence st len f1<k holds mid(f1,k,k)={}
proof
let f1 be FinSequence;
assume
A1: len f1<k;
then len f1+1<=k by NAT_1:13;
then
A2: len f1+1-1<=k-1 by XREAL_1:9;
0+1<=k by A1,NAT_1:13;
then len f1<=k-'1 by A2,XREAL_1:233;
then
A3: f1/^(k-'1)={} by FINSEQ_5:32;
k-'k+1=k-k+1 by XREAL_1:233
.=1;
then mid(f1,k,k)=(f1/^(k-'1))|1 by Def3;
hence thesis by A3;
end;
theorem
for f1 being FinSequence holds mid(f1,i1,i2)=Rev mid(f1,i2,i1)
proof
let f1 be FinSequence;
set k1 = i1, k2 = i2;
now
per cases;
case
A1: k1<=k2;
then
A2: mid(f1,k1,k2)=(f1/^(k1-'1))|(k2-'k1+1) by Def3;
now
per cases by A1,XXREAL_0:1;
case
k1<k2;
then mid(f1,k2,k1)=Rev mid(f1,k1,k2) by A2,Def3;
hence thesis;
end;
case
A3: k1=k2;
A4: k1=0 or 0+1<=k1 by NAT_1:13;
now
per cases by A4;
case
k1=0;
then
A5: mid(f1,k1,k2)=f1|1 by A3,Th16;
now
per cases;
case
len f1=0;
then f1={};
then f1|1={};
hence thesis by A3,A5;
end;
case
len f1<>0;
then f1 <> {};
then f1|1=<*f1.1*> by FINSEQ_5:20;
hence thesis by A3,A5,FINSEQ_5:60;
end;
end;
hence thesis;
end;
case
1<=k1 & k1<= len f1; then
k1 in dom f1 by FINSEQ_3:25;
then mid(f1,k1,k1)=<*f1.k1*> by Th15;
hence thesis by A3,FINSEQ_5:60;
end;
case
len f1<k1;
then mid(f1,k1,k1)={} by Th17;
hence thesis by A3;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
case
A6: k1>k2;
then mid(f1,k1,k2)=Rev ((f1/^(k2-'1))|(k1-'k2+1)) by Def3;
hence thesis by A6,Def3;
end;
end;
hence thesis;
end;