:: Zero Based Finite Sequences
:: by Tetsuya Tsunetou , Grzegorz Bancerek and Yatsuka Nakamura
::
:: Received September 28, 2001
:: Copyright (c) 2001-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, SUBSET_1, FUNCT_1, ARYTM_3, XXREAL_0, XBOOLE_0, TARSKI,
NAT_1, ORDINAL1, FINSEQ_1, CARD_1, FINSET_1, RELAT_1, PARTFUN1, FUNCOP_1,
ORDINAL4, ORDINAL2, ARYTM_1, REAL_1, ZFMISC_1, FUNCT_4, VALUED_0,
AFINSQ_1, PRGCOR_2, CAT_1, AMISTD_1, AMISTD_3, AMISTD_2, VALUED_1,
CONNSP_3, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
ENUMSET1, CARD_1, ORDINAL2, NUMBERS, ORDINAL4, XCMPLX_0, XREAL_0, NAT_1,
PARTFUN1, BINOP_1, FINSOP_1, NAT_D, FINSET_1, FINSEQ_1, FUNCOP_1,
FUNCT_4, FUNCT_7, XXREAL_0, VALUED_0, VALUED_1;
constructors WELLORD2, FUNCT_4, XXREAL_0, ORDINAL4, FUNCT_7, ORDINAL3,
VALUED_1, ENUMSET1, NAT_D, XXREAL_2, BINOP_1, FINSOP_1, RELSET_1, CARD_1,
NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
XXREAL_0, XREAL_0, NAT_1, CARD_1, ORDINAL2, NUMBERS, VALUED_1, XXREAL_2,
MEMBERED, FINSET_1, FUNCT_4, FINSEQ_1, INT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, ORDINAL1, XBOOLE_0, RELAT_1, PARTFUN1, CARD_1;
equalities ORDINAL1, FUNCOP_1, VALUED_1;
expansions TARSKI, ORDINAL1, RELAT_1, CARD_1, FUNCT_1;
theorems TARSKI, AXIOMS, FUNCT_1, NAT_1, ZFMISC_1, RELAT_1, RELSET_1,
ORDINAL1, CARD_1, FINSEQ_1, FUNCT_7, ORDINAL4, CARD_2, FUNCT_4, ORDINAL3,
XBOOLE_0, XBOOLE_1, FINSET_1, FUNCOP_1, XREAL_1, VALUED_0, ENUMSET1,
XXREAL_0, XREAL_0, GRFUNC_1, XXREAL_2, NAT_D, VALUED_1, XTUPLE_0,
FINSEQ_3, ORDINAL2, INT_1;
schemes FUNCT_1, SUBSET_1, NAT_1, XBOOLE_0, CLASSES1, FINSEQ_1;
begin
reserve k,n for Nat,
x,y,z,y1,y2 for object,X,Y for set,
f,g for Function;
:: Extended Segments of Natural Numbers
theorem Th0: ::: CHORD:1 moved eventually from there -> go to INT_1
for n being non zero Nat holds n-1 is Nat & 1 <= n
proof
let n be non zero Nat;
A1: 0+1 <= n by NAT_1:13;
then 0+1-1 <= n-1 by XREAL_1:9;
then n-1 in NAT by INT_1:3;
hence n-1 is Nat;
thus thesis by A1;
end;
theorem Th1:
Segm n \/ { n } = Segm(n+1)
proof
n in Segm(n+1) by NAT_1:45;
then
A1:{n} c= Segm(n+1) by ZFMISC_1:31;
Segm n c= Segm(n+1) by NAT_1:39,11;
hence Segm n \/ { n } c= Segm(n+1) by A1,XBOOLE_1:8;
let x be object;
assume
A2: x in Segm(n+1);
then reconsider x as Nat;
now
x < n+1 by A2,NAT_1:44;
then per cases by NAT_1:22;
case x < n;
hence x in Segm n by NAT_1:44;
end;
case x = n;
hence x in {n} by TARSKI:def 1;
end;
end;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th2:
Seg n c= Segm(n+1)
proof
let x be object;
assume
A1: x in Seg n;
then reconsider x as Element of NAT;
x<=n by A1,FINSEQ_1:1;
then x<n+1 by NAT_1:13;
hence thesis by NAT_1:44;
end;
theorem
n+1 = {0} \/ Seg n
proof
thus n+1 c= {0} \/ Seg n
proof
let x be object;
assume x in n+1;
then x in {j where j is Nat: j<n+1} by AXIOMS:4;
then consider j being Nat such that
A1: j=x and
A2: j<n+1;
j=0 or 1<j+1 & j<=n by A2,NAT_1:13,XREAL_1:29;
then j=0 or 1<=j & j<=n by NAT_1:13;
then x in {0} or x in Seg n by A1,FINSEQ_1:1,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
A3: Segm 1 c= Segm(n+1) by NAT_1:39,11;
Seg(n) c= Segm(n+1) by Th2;
hence thesis by A3,CARD_1:49,XBOOLE_1:8;
end;
:: Finite ExFinSequences
theorem
for r being Function holds r is finite Sequence-like iff
ex n st dom r = n by FINSET_1:10;
definition
mode XFinSequence is finite Sequence;
end;
reserve p,q,r,s,t for XFinSequence;
registration let p;
cluster dom p -> natural;
coherence;
end;
notation let p;
synonym len p for card p;
end;
registration let p;
identify len p with dom p;
compatibility
proof
thus len p = card dom p by CARD_1:62
.= dom p;
end;
identify dom p with len p;
compatibility;
end;
definition let p;
redefine func len p -> Element of NAT; :: redefines len (AFINSQ_1, synonym) → card (CARD_1, definition)
coherence
proof
card p = card p;
hence thesis;
end;
end;
definition let p;
redefine func dom p -> Subset of NAT; :: redefines dom (RELAT_1, synonym) → proj1 (XTUPLE_0, definition)
coherence
proof
{i where i is Nat:i<len p} c= NAT
proof
let x be object;
assume x in {i where i is Nat:i<len p};
then ex i being Nat st i=x & i<len p;
hence thesis by ORDINAL1:def 12;
end;
hence thesis by AXIOMS:4;
end;
end;
theorem
(ex k st dom f c= k) implies ex p st f c= p
proof
given k such that
A1: dom f c= k;
deffunc F(object) = f.$1;
consider g such that
A2: dom g = k &
for x being object st x in k holds g.x = F(x) from FUNCT_1:sch 3;
reconsider g as XFinSequence by A2,FINSET_1:10,ORDINAL1:def 7;
take g;
let y,z be object;
assume A3: [y,z] in f;
then
A4: y in dom f by XTUPLE_0:def 12;
then
A5: [y,g.y] in g by A1,A2,FUNCT_1:1;
z is set by TARSKI:1;
then f.y = z by A3,A4,FUNCT_1:def 2;
hence thesis by A1,A2,A4,A5;
end;
scheme XSeqEx{A()->Nat,P[object,object]}:
ex p st dom p = A() & for k st k in A() holds P[k,p.k]
provided
A1: for k st k in A() ex x being object st P[k,x]
proof
A2: for x being object st x in A() ex y being object st P[x,y]
proof
let x be object;
assume
A3: x in A();
A()={i where i is Nat: i<A()} by AXIOMS:4;
then ex i being Nat st i=x & i<A() by A3;
hence thesis by A1,A3;
end;
consider f being Function such that
A4: dom f = A() &
for x being object st x in A() holds P[x,f.x] from CLASSES1:sch 1(A2);
reconsider p=f as XFinSequence by A4,FINSET_1:10,ORDINAL1:def 7;
take p;
thus thesis by A4;
end;
scheme
XSeqLambda{A()->Nat,F(object) -> object}:
ex p being XFinSequence st len p = A() &
for k st k in A() holds p.k=F(k) proof
consider f being Function such that
A1: dom f = A() &
for x being object st x in A() holds f.x=F(x) from FUNCT_1:sch 3;
reconsider p=f as XFinSequence by A1,FINSET_1:10,ORDINAL1:def 7;
take p;
thus thesis by A1;
end;
theorem
z in p implies ex k st k in dom p & z = [k,p.k]
proof
assume
A1: z in p;
then consider x,y being object such that
A2: z=[x,y] by RELAT_1:def 1;
x in dom p by A1,A2,FUNCT_1:1;
then reconsider k = x as Element of NAT;
take k;
thus thesis by A1,A2,FUNCT_1:1;
end;
theorem
dom p = dom q & (for k st k in dom p holds p.k = q.k) implies p = q;
Lm1: k < len p iff k in dom p
proof
thus k < len p implies k in dom p
proof assume k < len p;
then k in Segm len p by NAT_1:44;
hence k in dom p;
end;
assume k in dom p;
then k in Segm len p;
hence k < len p by NAT_1:44;
end;
theorem Th8:
( len p = len q & for k st k < len p holds p.k=q.k ) implies p=q
proof
assume that
A1: len p = len q and
A2: for k st k<len p holds p.k = q.k;
for x being object st x in dom p holds p.x = q.x by A2,Lm1;
hence thesis by A1;
end;
registration let p,n;
cluster p|n -> finite;
coherence;
end;
theorem
rng p c= dom f implies f*p is XFinSequence
proof
assume rng p c= dom f;
then dom(f*p) = len p by RELAT_1:27;
hence thesis by ORDINAL1:def 7;
end;
theorem Th10:
k <= len p implies dom(p|k) = k
proof assume k <= len p;
then Segm k c= Segm len p by NAT_1:39;
hence dom(p|k) = k by RELAT_1:62;
end;
:: XFinSequences of D
registration let D be set;
cluster finite for Sequence of D;
existence
proof
{} is Sequence of D by ORDINAL1:30;
hence thesis;
end;
end;
definition let D be set;
mode XFinSequence of D is finite Sequence of D;
end;
theorem Th11:
for D being set, f being XFinSequence of D holds f is PartFunc of NAT,D
proof
let D be set, f be XFinSequence of D;
dom f c= NAT & rng f c= D by RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
registration
cluster empty -> Sequence-like for Function;
coherence;
end;
reserve D for set;
registration
let k be Nat, a be object;
cluster Segm k --> a -> finite Sequence-like;
coherence;
end;
::$CT
theorem Th12:
for D being non empty set ex p being XFinSequence of D st len p = k
proof
let D be non empty set;
set y = the Element of D;
set p = k --> y;
reconsider p = k --> y as XFinSequence;
reconsider p as XFinSequence of D;
take p;
thus thesis;
end;
:: ::
:: The Empty XFinSequence ::
:: ::
theorem
len p = 0 iff p = {};
theorem Th14:
for D be set holds {} is XFinSequence of D
proof
let D be set;
rng {} c= D;
hence thesis by RELAT_1:def 19;
end;
registration let D be set;
cluster empty for XFinSequence of D;
existence
proof
{} is XFinSequence of D by Th14;
hence thesis;
end;
end;
registration
let D be non empty set;
cluster non empty for XFinSequence of D;
existence
proof
set k = 1;
consider p being XFinSequence of D such that
A1: len p = k by Th12;
p <> {} by A1;
hence thesis;
end;
end;
definition let x;
func <%x%> -> set equals
0 .--> x;
coherence;
end;
registration let x;
cluster <%x%> -> non empty;
coherence;
end;
definition let D be set;
func <%>D -> XFinSequence of D equals
{};
coherence by Th14;
end;
registration
let D be set;
cluster <%>D -> empty;
coherence;
end;
definition let p,q;
redefine func p^q means :: redefines ^ (ORDINAL4, definition)
:Def3: dom it = len p + len q & (for k st k in dom p
holds it.k=p.k) & for k st k in dom q holds it.(len p + k) = q.k;
compatibility
proof
let pq be Sequence;
A1: len p +^ len q = len p + len q by CARD_2:36;
hereby
assume
A2: pq = p^q;
hence dom pq = len p + len q by A1,ORDINAL4:def 1;
thus for k st k in dom p holds pq.k=p.k by A2,ORDINAL4:def 1;
let k;
assume k in dom q;
then pq.(len p +^ k) = q.k & k in NAT by A2,ORDINAL4:def 1;
hence pq.(len p + k) = q.k by CARD_2:36;
end;
assume that
A3: dom pq = len p + len q and
A4: for k st k in dom p holds pq.k=p.k and
A5: for k st k in dom q holds pq.(len p + k) = q.k;
A6: now
let a be Ordinal;
assume
A7: a in dom q;
then reconsider k = a as Element of NAT;
thus pq.(dom p +^ a) = pq.(len p + k) by CARD_2:36
.= q.a by A5,A7;
end;
for a be Ordinal st a in dom p holds pq.a = p.a by A4;
hence thesis by A1,A3,A6,ORDINAL4:def 1;
end;
end;
registration
let p,q;
cluster p^q -> finite;
coherence
proof
dom (p^q) = (dom p)+^dom q by ORDINAL4:def 1;
hence thesis by FINSET_1:10;
end;
end;
theorem
len(p^q) = len p + len q by Def3;
theorem Th16:
len p <= k & k < len p + len q implies (p^q).k=q.(k-len p)
proof
assume that
A1: len p <= k and
A2: k < len p + len q;
consider m being Nat such that
A3: len p + m = k by A1,NAT_1:10;
k - len p < len p + len q - len p by A2,XREAL_1:14;
then m in dom q by A3,Lm1;
hence thesis by A3,Def3;
end;
theorem Th17:
len p <= k & k < len(p^q) implies (p^q).k = q.(k - len p)
proof
assume that
A1: len p <= k and
A2: k < len(p^q);
k < len p + len q by A2,Def3;
hence thesis by A1,Th16;
end;
theorem Th18:
k in dom (p^q) implies (k in dom p or ex n st n in dom q & k=len
p + n )
proof
assume k in dom(p^q);
then k in Segm(len p + len q) by Def3;
then
A1: k < len p + len q by NAT_1:44;
now
assume len p <= k;
then consider n being Nat such that
A2: k=len p + n by NAT_1:10;
n + len p - len p < len q + len p - len p by A1,A2,XREAL_1:14;
hence thesis by A2,Lm1;
end;
hence thesis by Lm1;
end;
theorem Th19:
for p,q being Sequence holds dom p c= dom(p^q)
proof
let p,q be Sequence;
dom(p^q) = (dom p)+^(dom q) by ORDINAL4:def 1;
hence thesis by ORDINAL3:24;
end;
theorem Th20:
x in dom q implies ex k st k=x & len p + k in dom(p^q)
proof
assume
A1: x in dom q;
then reconsider k=x as Element of NAT;
take k;
len p + k < len p + len q by XREAL_1:8,A1,Lm1;
then len p + k in Segm(len p + len q) by NAT_1:44;
hence thesis by Def3;
end;
theorem Th21:
k in dom q implies len p + k in dom(p^q)
proof
assume k in dom q;
then ex n st n=k & len p + n in dom(p^q) by Th20;
hence thesis;
end;
theorem
rng p c= rng(p^q)
proof
A1: dom p c= dom(p^q) by Th19;
let x be object;
assume x in rng p;
then consider y being object such that
A2: y in dom p and
A3: x=p.y by FUNCT_1:def 3;
reconsider k=y as Element of NAT by A2;
(p^q).k=p.k by A2,Def3;
hence x in rng(p^q) by A2,A3,A1,FUNCT_1:3;
end;
theorem
rng q c= rng(p^q)
proof
let x be object;
assume x in rng q;
then consider y being object such that
A1: y in dom q and
A2: x=q.y by FUNCT_1:def 3;
reconsider k=y as Element of NAT by A1;
len p + k in dom(p^q) & (p^q).(len p + k) = q.k by A1,Def3,Th21;
hence x in rng(p^q) by A2,FUNCT_1:3;
end;
theorem Th24: ::: ORDINAL4:2
rng(p^q) = rng p \/ rng q by ORDINAL4:2;
theorem Th25:
p^q^r = p^(q^r)
proof
A1: for k st k in dom p holds ((p^q)^r).k=p.k
proof
let k;
assume
A2: k in dom p;
dom p c= dom(p^q) by Th19;
hence (p^q^r).k=(p^q).k by A2,Def3
.=p.k by A2,Def3;
end;
A3: for k st k in dom(q^r) holds ((p^q)^r).(len p + k)=(q^r).k
proof
let k;
assume
A4: k in dom(q^r);
A5: now
assume not k in dom q;
then consider n such that
A6: n in dom r and
A7: k=len q + n by A4,Th18;
thus (p^q^r).(len p + k) =(p^q^r).(len p + len q + n) by A7
.=(p^q^r).(len(p^q) + n) by Def3
.=r.n by A6,Def3
.=(q^r).k by A6,A7,Def3;
end;
now
assume
A8: k in dom q;
then (len p + k) in dom(p^q) by Th21;
hence (p^q^r).(len p + k) = (p^q).(len p + k) by Def3
.=q.k by A8,Def3
.=(q^r).k by A8,Def3;
end;
hence thesis by A5;
end;
dom ((p^q)^r) = (len (p^q) + len r) by Def3
.= (len p + len q + len r) by Def3
.= (len p + (len q + len r))
.= (len p + len(q^r)) by Def3;
hence thesis by A1,A3,Def3;
end;
theorem Th26:
p^r = q^r or r^p = r^q implies p = q
proof
A1: now
assume
A2: p^r = q^r;
then len p + len r = len(q^r) by Def3;
then
A3: len p + len r = len q + len r by Def3;
for k st k in dom p holds p.k=q.k
proof
let k;
assume
A4: k in dom p;
hence p.k=(q^r).k by A2,Def3
.=q.k by A3,A4,Def3;
end;
hence thesis by A3;
end;
A5: now
assume
A6: r^p=r^q;
then
A7: len r + len p = len(r^q) by Def3
.=len r + len q by Def3;
for k st k in dom p holds p.k=q.k
proof
let k;
assume
A8: k in dom p;
hence p.k = (r^q).(len r + k) by A6,Def3
.= q.k by A7,A8,Def3;
end;
hence thesis by A7;
end;
assume p^r = q^r or r^p = r^q;
hence thesis by A1,A5;
end;
registration let p;
reduce p^{} to p;
reducibility
proof
A1: for k st k in dom p holds p.k=(p^{}).k by Def3;
dom(p^{}) = len p + len {} by Def3
.= dom p;
hence p^{} = p by A1;
end;
reduce {}^p to p;
reducibility
proof
A2: for k st k in dom p holds p.k = ({}^p).k
proof
let k;
assume
A3: k in dom p;
thus ({}^p).k =({}^p).(len {} + k)
.=p.k by A3,Def3;
end;
dom({}^p) = (len {} + len p) by Def3
.= dom p;
hence thesis by A2;
end;
end;
::$CT
theorem Th27:
p^q = {} implies p = {} & q = {}
proof
assume p^q={};
then 0 = len p + len q by Def3;
hence thesis;
end;
registration
let D be set;
let p,q be XFinSequence of D;
cluster p^q -> D-valued;
coherence
proof
A1: rng q c= D by RELAT_1:def 19;
rng(p^q) = rng p \/ rng q & rng p c= D by Th24,RELAT_1:def 19;
hence thesis by A1,XBOOLE_1:8;
end;
end;
Lm2: for x1, y1 being set holds [x,y] in {[x1,y1]} implies x = x1 & y = y1
proof
let x1, y1 be set;
assume [x,y] in {[x1,y1]};
then [x,y] = [x1,y1] by TARSKI:def 1;
hence thesis by XTUPLE_0:1;
end;
definition
let x;
redefine func <%x%> -> Function means :: redefines <% (AFINSQ_1, definition)
:Def4:
dom it = 1 & it.0 = x;
coherence;
compatibility
proof
let f be Function;
thus f = <%x%> implies dom f = 1 & f.0 = x by CARD_1:49,FUNCOP_1:72;
assume that
A1: dom f = 1 and
A2: f.0 = x;
reconsider g = { [0,f.0] } as Function;
for y,z being object holds [y,z] in f iff [y,z] in g
proof let y,z be object;
hereby
assume
A3: [y,z] in f;
then y in {0} by A1,CARD_1:49,XTUPLE_0:def 12;
then
A4: y = 0 by TARSKI:def 1;
A5: rng f = {f.0} by A1,CARD_1:49,FUNCT_1:4;
z in rng f by A3,XTUPLE_0:def 13;
then z = f.0 by A5,TARSKI:def 1;
hence [y,z] in g by A4,TARSKI:def 1;
end;
assume [y,z] in g;
then
A6: y = 0 & z = f.0 by Lm2;
0 in dom f by A1,CARD_1:49,TARSKI:def 1;
hence thesis by A6,FUNCT_1:def 2;
end;
then f = { [0,f.0] };
hence thesis by A2,FUNCT_4:82;
end;
end;
registration
let x;
cluster <%x%> -> Function-like Relation-like;
coherence;
end;
registration
let x;
cluster <%x%> -> finite Sequence-like;
coherence;
end;
theorem
p^q is XFinSequence of D implies
p is XFinSequence of D & q is XFinSequence of D
proof
assume p^q is XFinSequence of D;
then rng(p^q) c= D by RELAT_1:def 19;
then
A1: rng p \/ rng q c= D by Th24;
rng p c= rng p \/ rng q by XBOOLE_1:7;
then rng p c= D by A1;
hence p is XFinSequence of D by RELAT_1:def 19;
rng q c= rng p \/ rng q by XBOOLE_1:7;
then rng q c= D by A1;
hence thesis by RELAT_1:def 19;
end;
definition
let x,y;
func <%x,y%> -> set equals
<%x%>^<%y%>;
correctness;
let z;
func <%x,y,z%> -> set equals
<%x%>^<%y%>^<%z%>;
correctness;
end;
registration
let x,y;
cluster <%x,y%> -> Function-like Relation-like;
coherence;
let z;
cluster <%x,y,z%> -> Function-like Relation-like;
coherence;
end;
registration
let x,y;
cluster <%x,y%> -> finite Sequence-like;
coherence;
let z;
cluster <%x,y,z%> -> finite Sequence-like;
coherence;
end;
theorem
<%x%> = { [0,x] } by FUNCT_4:82;
theorem Th30:
p=<%x%> iff dom p = Segm 1 & rng p = {x}
proof
thus p = <%x%> implies dom p = Segm 1 & rng p = {x}
proof
assume
A1: p = <%x%>;
hence dom p = Segm 1 by Def4;
rng p = {p.0} by FUNCT_1:4,A1;
hence thesis by A1,Def4;
end;
assume that
A2: dom p = Segm 1 and
A3: rng p = {x};
1=0+1;
then p.0 in {x} by A2,A3,FUNCT_1:3,NAT_1:45;
then p.0 = x by TARSKI:def 1;
hence thesis by A2,Def4;
end;
theorem Th31:
p = <%x%> iff len p = 1 & p.0 = x by Def4;
registration let x;
reduce <%x%>.0 to x;
reducibility by Th31;
end;
theorem Th32:
(<%x%>^p).0 = x
proof
0 in 1 by CARD_1:49,TARSKI:def 1;
then 0 in dom <%x%> by Def4;
then (<%x%>^p).0 = <%x%>.0 by Def3;
hence thesis;
end;
theorem Th33:
(p^<%x%>).(len p) = x
proof
A1: dom <%x%> = 1 & 0 in Segm(0+1) by Def4,NAT_1:45;
len p + 0 = len p;
hence (p^<%x%>).(len p) = <%x%>.0 by A1,Def3
.=x;
end;
theorem
<%x,y,z%>=<%x%>^<%y,z%> & <%x,y,z%>=<%x,y%>^<%z%> by Th25;
theorem Th35:
p = <%x,y%> iff len p = 2 & p.0=x & p.1=y
proof
thus p = <%x,y%> implies len p = 2 & p.0=x & p.1=y
proof
assume
A1: p=<%x,y%>;
hence len p = len <%x%> + len <%y%> by Def3
.= 1 + len <%y%> by Th30
.= 1 + 1 by Th30
.=2;
0 in {0} by TARSKI:def 1;
then
A3: 0 in dom <%y%>;
0 in dom <%x%> by TARSKI:def 1;
hence p.0 = <%x%>.0 by A1,Def3
.= x;
thus p.1 = (<%x%>^<%y%>).(len <%x%> + 0) by A1,Th30
.= <%y%>.0 by A3,Def3
.= y;
end;
assume that
A4: len p = 2 and
A5: p.0=x and
A6: p.1=y;
A7: for k st k in dom <%y%> holds p.((len <%x%>)+k)=<%y%>.k
proof
let k;
assume a8: k in dom <%y%>;
thus p.((len <%x%>) + k) = p.(1+k) by Th30
.=p.(1+0) by a8,TARSKI:def 1
.=<%y%>.0 by A6
.= <%y%>.k by a8,TARSKI:def 1;
end;
A9: for k st k in dom <%x%> holds p.k=<%x%>.k
proof
let k;
assume k in dom <%x%>;
then k=0 by TARSKI:def 1;
hence thesis by A5;
end;
dom p = (1+1) by A4
.= (len <%x%> + 1) by Th30
.= (len <%x%> + len <%y%>) by Th30;
hence thesis by A9,A7,Def3;
end;
registration let x,y;
reduce <%x,y%>.0 to x;
reducibility by Th35;
reduce <%x,y%>.1 to y;
reducibility by Th35;
end;
theorem Th36:
p = <%x,y,z%> iff len p = 3 & p.0 = x & p.1 = y & p.2 = z
proof
thus p = <%x,y,z%> implies len p = 3 & p.0 = x & p.1 = y & p.2 = z
proof
A2: 0 in dom <%x%> by TARSKI:def 1;
A3: 0 in dom <%z%> by TARSKI:def 1;
assume
A4: p =<%x,y,z%>;
hence len p =len <%x,y%> + len <%z%> by Def3
.=2 + len <%z%> by Th35
.=2+1 by Th30
.=3;
thus p.0 = (<%x%>^<%y,z%>).0 by A4,Th25
.=<%x%>.0 by A2,Def3
.=x;
1 in Segm(1+1) & len <%x,y%> = 2 by Th35,NAT_1:45;
hence p.1 =<%x,y%>.1 by A4,Def3
.=y;
thus p.2 =(<%x,y%>^<%z%>).(len (<%x,y%>) + 0) by A4,Th35
.= <%z%>.0 by A3,Def3
.= z;
end;
assume that
A5: len p = 3 and
A6: p.0 = x and
A7: p.1 = y and
A8: p.2 = z;
A9: for k st k in dom <%x,y%> holds p.k=<%x,y%>.k
proof
A10: len <%x,y%> = 2 by Th35;
let k such that
A11: k in dom <%x,y%>;
A12: k=1 implies p.k=<%x,y%>.k by A7;
k=0 implies p.k=<%x,y%>.k by A6;
hence thesis by A11,A10,A12,CARD_1:50,TARSKI:def 2;
end;
A13: for k st k in dom <%z%> holds p.( (len <%x,y%>) + k) = <%z%>.k
proof
let k;
assume k in dom <%z%>;
then
A14: k = 0 by TARSKI:def 1;
hence p.( (len <%x,y%>) + k) = p.(2+0) by Th35
.=<%z%>.k by A8,A14;
end;
dom p = 2+1 by A5
.= ((len <%x,y%>) + 1) by Th35
.= ((len <%x,y%>) + len <%z%>) by Th30;
hence thesis by A9,A13,Def3;
end;
registration
let x,y,z;
reduce <%x,y,z%>.0 to x;
reducibility by Th36;
reduce <%x,y,z%>.1 to y;
reducibility by Th36;
reduce <%x,y,z%>.2 to z;
reducibility by Th36;
end;
registration
let x;
cluster <%x%> -> 1-element;
coherence by Th30;
let y;
cluster <%x,y%> -> 2-element;
coherence by Th35;
let z;
cluster <%x,y,z%> -> 3-element;
coherence by Th36;
end;
registration let n be Nat;
cluster n-element -> n-defined for XFinSequence;
coherence;
end;
registration let n be Nat, x be object;
cluster n --> x -> finite Sequence-like;
coherence;
end;
registration let n be Nat;
cluster n-element empty-yielding for XFinSequence;
existence
proof
take n --> 0;
card(n --> 0) = n;
hence thesis;
end;
end;
registration let n be Nat;
cluster -> total for n-element n-defined XFinSequence;
coherence
proof let s be n-element XFinSequence;
thus dom s = n by CARD_1:def 7;
end;
end;
theorem Th37:
p <> {} implies ex q,x st p = q^<%x%>
proof
assume p <> {};
then consider n being Nat such that
A1: len p = n+1 by NAT_1:6;
A2: dom p = Segm(n+1) by A1;
reconsider n as Element of NAT by ORDINAL1:def 12;
set q=p| n;
dom q = len p /\ n & Segm n c= Segm len p by A1,NAT_1:11,39,RELAT_1:61;
then
A3: dom q = n by XBOOLE_1:28;
A4: for x being object st x in dom p holds p.x = (q^<%p.(len p - 1)%>).x
proof
let x be object;
assume
A5: x in dom p;
then reconsider k = x as Element of NAT;
A6: now
assume
A7: k in n;
hence p.k=q.k by A3,FUNCT_1:47
.=(q^<%p.(len p - 1)%>).k by A3,A7,Def3;
end;
A8: now
0 in Segm(0+1) by NAT_1:45;
then
A9: 0 in dom <%p.(len p - 1)%> by Def4;
assume
A10: k in {n};
hence (q^<%p.(len p - 1)%>).k =(q^<%p.(len p - 1)%>).(len q + 0) by A3,
TARSKI:def 1
.=<%p.(len p - 1)%>.0 by A9,Def3
.=p.k by A1,A10,TARSKI:def 1;
end;
k in Segm n \/ {n} by A5,Th1,A2;
hence thesis by A6,A8,XBOOLE_0:def 3;
end;
take q;
take p.(len p - 1);
dom(q^<%p.(len p - 1)%>) = (len q + len <%p.(len p - 1)%>) by Def3
.= dom p by A1,A3,Th30;
hence q^<%p.(len p - 1)%>=p by A4;
end;
registration
let D be non empty set;
let d1 be Element of D;
cluster <%d1%> -> D-valued;
coherence;
let d2 be Element of D;
cluster <%d1,d2%> -> D-valued;
coherence;
let d3 be Element of D;
cluster <%d1,d2,d3%> -> D-valued;
coherence;
end;
:: Scheme of induction for extended finite sequences
scheme
IndXSeq{P[XFinSequence]}: for p holds P[p]
provided
A1: P[{}] and
A2: for p,x st P[p] holds P[p^<%x%>]
proof
defpred P1[Real] means for p st len p = $1 holds P[p];
let p;
consider X being Subset of REAL such that
A3: for x being Element of REAL holds x in X iff P1[x] from SUBSET_1:sch 3;
for k holds k in X
proof
A4: 0 in REAL by XREAL_0:def 1;
defpred R[Nat] means $1 in X;
for p st len p = 0 holds P[p]
proof
let p;
assume len p = 0;
then p = {};
hence thesis by A1;
end; then
A5: R[0] by A3,A4;
A6: for n st R[n] holds R[n+1]
proof
let n;
assume
A7: R[n];
A8: n+1 in REAL by XREAL_0:def 1;
P1[n+1]
proof
let p;
assume
A9: len p = n+1;
then p <> {};
then consider w being XFinSequence, x such that
A10: p = w^<%x%> by Th37;
len p = len w + len <%x%> by A10,Def3
.= len w+1 by Def4;
hence P[p] by A10,A2,A3,A7,A9;
end;
hence thesis by A3,A8;
end;
thus for k holds R[k] from NAT_1:sch 2(A5,A6);
end;
then len p in X;
hence thesis by A3;
end;
theorem
for p,q,r,s being XFinSequence st p^q = r^s & len p <= len r
ex t being XFinSequence st p^t = r
proof
defpred P[XFinSequence] means for p,q,s st p^q=$1^s & len p <= len $1 holds
ex t being XFinSequence st p^t=$1;
A1: for r,x st P[r] holds P[r^<%x%>]
proof
let r,x;
assume
A2: for p,q,s st p^q=r^s & len p <= len r ex t st p^t=r;
let p,q,s;
assume that
A3: p^q=(r^<%x%>)^s and
A4: len p <= len (r^<%x%>);
A5: now
assume len p <> len(r^<%x%>);
then len p <> len r + len <%x%> by Def3;
then
A6: len p <> len r + 1 by Th30;
len p <= len r + len <%x%> by A4,Def3;
then
A7: len p <= len r + 1 by Th30;
p^q=r^(<%x%>^s) by A3,Th25;
then consider t being XFinSequence such that
A8: p^t = r by A2,A6,A7,NAT_1:8;
p^(t^<%x%>) = r^<%x%> by A8,Th25;
hence thesis;
end;
now
assume
A9: len p = len(r^<%x%>);
A10: for k st k in dom p holds p.k=(r^<%x%>).k
proof
let k;
assume
A11: k in dom p;
hence p.k = (r^<%x%>^s).k by A3,Def3
.=(r^<%x%>).k by A9,A11,Def3;
end;
p^{} =r^<%x%> by A9,A10;
hence thesis;
end;
hence thesis by A5;
end;
A12: P[{}]
proof
let p,q,s;
assume that
p^q={}^s and
A13: len p <= len {};
take {};
thus p^{} = {} by A13;
end;
for r holds P[r] from IndXSeq(A12,A1);
hence thesis;
end;
definition
let D be set;
func D^omega -> set means :Def7:
x in it iff x is XFinSequence of D;
existence
proof
defpred P[object] means $1 is XFinSequence of D;
consider X such that
A1: x in X iff x in bool [:NAT,D:] & P[x] from XBOOLE_0:sch 1;
take X;
let x;
thus x in X implies x is XFinSequence of D by A1;
assume x is XFinSequence of D;
then reconsider p = x as XFinSequence of D;
reconsider p as PartFunc of NAT,D by Th11;
p c= [:NAT,D:];
hence thesis by A1;
end;
uniqueness
proof
defpred P[object] means $1 is XFinSequence of D;
thus for X1,X2 being set st
(for x being object holds x in X1 iff P[x]) &
(for x being object holds x in X2 iff P[x]) holds X1 = X2
from XBOOLE_0:sch 3;
end;
end;
registration
let D be set;
cluster D^omega -> non empty;
coherence
proof
set f = the XFinSequence of D;
f in D^omega by Def7;
hence thesis;
end;
end;
theorem
x in D^omega iff x is XFinSequence of D by Def7;
theorem
{} in D^omega
proof
{} = <%>D;
hence thesis by Def7;
end;
scheme
SepXSeq{D()->non empty set, P[XFinSequence]}:
ex X st for x holds x in X iff
ex p st p in D()^omega & P[p] & x=p
proof
defpred P1[object] means ex p st P[p] & $1=p;
consider Y such that
A1: for x being object holds x in Y iff x in D()^omega & P1[x]
from XBOOLE_0:sch 1;
take Y;
x in Y implies ex p st p in D()^omega & P[p] & x=p
proof
assume x in Y;
then x in D()^omega & ex p st P[p] & x=p by A1;
hence thesis;
end;
hence thesis by A1;
end;
notation
let p be XFinSequence;
let i,x be set;
synonym Replace(p,i,x) for p+*(i,x);
end;
registration
let p be XFinSequence;
let i,x be object;
cluster p+*(i,x) -> finite Sequence-like;
coherence
proof
dom (p+*(i,x)) = dom p by FUNCT_7:30;
hence thesis by FINSET_1:10;
end;
end;
theorem
for p being XFinSequence, i being Element of NAT, x being set holds
len Replace(p,i,x) = len p & (i < len p implies Replace(p,i,x).i = x) &
for j being Element of NAT st j <> i holds Replace(p,i,x).j = p.j
proof
let p be XFinSequence;
let i be Element of NAT, x be set;
set f = Replace(p,i,x);
thus len f = len p by FUNCT_7:30;
i < len p implies not Segm len p c= Segm i by NAT_1:39;
hence i < len p implies f.i = x by FUNCT_7:31,ORDINAL1:16;
thus thesis by FUNCT_7:32;
end;
registration
let D be non empty set;
let p be XFinSequence of D;
let i be Element of NAT, a be Element of D;
cluster Replace(p,i,a) -> D -valued;
coherence
proof
per cases;
suppose
i in dom p;
then Replace(p,i,a) = p+*(i.-->a) by FUNCT_7:def 3;
then
A1: rng Replace(p,i,a) c= rng p \/ rng (i.-->a) by FUNCT_4:17;
rng (i.-->a) = {a} by FUNCOP_1:8;
then
A2: rng (i.-->a) c= D by ZFMISC_1:31;
rng p c= D by RELAT_1:def 19;
then rng p \/ rng (i.-->a) c= D by A2,XBOOLE_1:8;
hence rng Replace(p,i,a) c= D by A1;
end;
suppose
not i in dom p;
then Replace(p,i,a) = p by FUNCT_7:def 3;
hence rng Replace(p,i,a) c= D by RELAT_1:def 19;
end;
end;
end;
:: missing, 2008.02.02, A.K.
registration
cluster -> real-valued for XFinSequence of REAL;
coherence
proof
let F be XFinSequence of REAL;
rng F c= REAL by RELAT_1:def 19;
hence thesis by VALUED_0:def 3;
end;
end;
registration
cluster -> natural-valued for XFinSequence of NAT;
coherence
proof
let F be XFinSequence of NAT;
rng F c= NAT by RELAT_1:def 19;
hence thesis by VALUED_0:def 6;
end;
end;
registration
cluster non empty natural-valued for XFinSequence;
existence
proof
<%0%> is natural-valued & <%0%> is non empty;
hence thesis;
end;
end;
:: 2009.0929, A.T.
theorem Th42:
for x1, x2, x3, x4 being set st
p = <%x1%>^<%x2%>^<%x3%>^<%x4%> holds
len p = 4 & p.0 = x1 & p.1 = x2 & p.2 = x3 & p.3 = x4
proof
let x1, x2, x3, x4 be set;
assume
A1: p = <%x1%>^<%x2%>^<%x3%>^<%x4%>;
set p13 = <%x1%>^<%x2%>^<%x3%>;
A2: p13 = <%x1, x2, x3%>;
then
A3: len p13 = 3 by Th36;
A4: p13.0 = x1 & p13.1 = x2 by A2;
A5: p13.2 = x3 by A2;
thus len p = len p13 + len <%x4%> by A1,Def3
.= 3 + 1 by A3,Th30
.= 4;
0 in 3 & 1 in 3 & 2 in 3 by CARD_1:51,ENUMSET1:def 1;
hence p.0 = x1 & p.1 = x2 & p.2 = x3 by A1,A4,A5,Def3,A3;
thus p.3 = p.len p13 by A2,Th36
.= x4 by A1,Th33;
end;
theorem Th43:
for x1, x2, x3, x4, x5 being set st
p = <%x1%>^<%x2%>^<%x3%>^<%x4%>^<%x5%>
holds len p = 5 & p.0 = x1 & p.1 = x2 & p.2 = x3 & p.3 = x4 & p.4 = x5
proof
let x1, x2, x3, x4, x5 be set;
assume
A1: p = <%x1%>^<%x2%>^<%x3%>^<%x4%>^<%x5%>;
set p14 = <%x1%>^<%x2%>^<%x3%>^<%x4%>;
A2: len p14 = 4 by Th42;
A3: p14.0 = x1 & p14.1 = x2 by Th42;
A4: p14.2 = x3 & p14.3 = x4 by Th42;
thus len p = len p14 + len <%x5%> by A1,Def3
.= 4 + 1 by A2,Th30
.= 5;
0 in 4 & ... & 3 in 4 by CARD_1:52,ENUMSET1:def 2;
hence p.0 = x1 & p.1 = x2 & p.2 = x3 & p.3 = x4 by A1,A3,A4,Def3,A2;
thus p.4 = p.len p14 by Th42
.= x5 by A1,Th33;
end;
theorem Th44:
for x1, x2, x3, x4, x5, x6 being set st
p = <%x1%>^<%x2%>^<%x3%>^<%x4%>^<%x5%>^<%x6%>
holds len p = 6 & p.0 = x1 & p.1 = x2 & p.2 = x3 & p.3 = x4 & p.4 = x5 &
p.5 = x6
proof
let x1, x2, x3, x4, x5, x6 be set;
assume
A1: p = <%x1%>^<%x2%>^<%x3%>^<%x4%>^<%x5%>^<%x6%>;
set p15 = <%x1%>^<%x2%>^<%x3%>^<%x4%>^<%x5%>;
A2: len p15 = 5 by Th43;
A3: p15.0 = x1 & p15.1 = x2 by Th43;
A4: p15.2 = x3 & p15.3 = x4 by Th43;
A5: p15.4 = x5 by Th43;
thus len p = len p15 + len <%x6%> by A1,Def3
.= 5 + 1 by A2,Th30
.= 6;
0 in 5 & ... & 4 in 5 by CARD_1:53,ENUMSET1:def 3;
hence p.0 = x1 & p.1 = x2 & p.2 = x3 & p.3 = x4 & p.4 = x5
by A1,A3,A4,A5,Def3,A2;
thus p.5 = p.len p15 by Th43
.= x6 by A1,Th33;
end;
theorem Th45:
for x1, x2, x3, x4, x5, x6, x7 being set st
p = <%x1%>^<%x2%>^<%x3%>^<%x4%>^<%x5%>^<%x6%>^<%x7%>
holds len p = 7 & p.0 = x1 & p.1 = x2 & p.2 = x3 & p.3 = x4 & p.4 = x5 &
p.5 = x6 & p.6 = x7
proof
let x1, x2, x3, x4, x5, x6, x7 be set;
assume
A1: p = <%x1%>^<%x2%>^<%x3%>^<%x4%>^<%x5%>^<%x6%>^<%x7%>;
set p16 = <%x1%>^<%x2%>^<%x3%>^<%x4%>^<%x5%>^<%x6%>;
A2: len p16 = 6 by Th44;
A3: p16.0 = x1 & p16.1 = x2 by Th44;
A4: p16.2 = x3 & p16.3 = x4 by Th44;
A5: p16.4 = x5 & p16.5 = x6 by Th44;
thus len p = len p16 + len <%x7%> by A1,Def3
.= 6 + 1 by A2,Th30
.= 7;
0 in 6 & ... & 5 in 6 by CARD_1:54,ENUMSET1:def 4;
hence p.0 = x1 & p.1 = x2 & p.2 = x3 & p.3 = x4 & p.4 = x5 & p.5 = x6
by A1,A3,A4,A5,Def3,A2;
thus p.6 = p.len p16 by Th44
.= x7 by A1,Th33;
end;
theorem Th46:
for x1,x2,x3,x4, x5, x6, x7, x8 being set st
p = <%x1%>^<%x2%>^<%x3%>^<%x4%>^<%x5%>^<%x6%>^<%x7%>^<%x8%>
holds len p = 8 & p.0 = x1 & p.1 = x2 & p.2 = x3 & p.3 = x4 & p.4 = x5 &
p.5 = x6 & p.6 = x7 & p.7 = x8
proof
let x1, x2, x3, x4, x5, x6, x7, x8 be set;
assume
A1: p = <%x1%>^<%x2%>^<%x3%>^<%x4%>^<%x5%>^<%x6%>^<%x7%>^<%x8%>;
set p17 = <%x1%>^<%x2%>^<%x3%>^<%x4%>^<%x5%>^<%x6%>^<%x7%>;
A2: len p17 = 7 by Th45;
A3: p17.0 = x1 & p17.1 = x2 by Th45;
A4: p17.2 = x3 & p17.3 = x4 by Th45;
A5: p17.4 = x5 & p17.5 = x6 by Th45;
A6: p17.6 = x7 by Th45;
thus len p = len p17 + len <%x8%> by A1,Def3
.= 7 + 1 by A2,Th30
.= 8;
0 in 7 & ... & 6 in 7 by CARD_1:55,ENUMSET1:def 5;
hence p.0 = x1 & p.1 = x2 & p.2 = x3 & p.3 = x4 & p.4 = x5 & p.5 = x6 &
p.6 = x7 by A1,A3,A4,A5,A6,Def3,A2;
thus p.7 = p.len p17 by Th45
.= x8 by A1,Th33;
end;
theorem
for x1,x2,x3,x4,x5,x6,x7, x8, x9 being set st
p = <%x1%>^<%x2%>^<%x3%>^<%x4%>^<%x5%>^<%x6%>^<%x7%>^<%x8%>^<%x9%>
holds len p = 9 & p.0 = x1 & p.1 = x2 & p.2 = x3 & p.3 = x4 & p.4 = x5 &
p.5 = x6 & p.6 = x7 & p.7 = x8 & p.8 = x9
proof
let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set;
assume
A1: p = <%x1%>^<%x2%>^<%x3%>^<%x4%>^<%x5%>^<%x6%>^<%x7%>^<%x8%>^<%x9%>;
set p17 = <%x1%>^<%x2%>^<%x3%>^<%x4%>^<%x5%>^<%x6%>^<%x7%>^<%x8%>;
A2: len p17 = 8 by Th46;
A3: p17.0 = x1 & p17.1 = x2 by Th46;
A4: p17.2 = x3 & p17.3 = x4 by Th46;
A5: p17.4 = x5 & p17.5 = x6 by Th46;
A6: p17.6 = x7 & p17.7 = x8 by Th46;
thus len p = len p17 + len <%x9%> by A1,Def3
.= 8 + 1 by A2,Th30
.= 9;
0 in 8 & ... & 7 in 8 by CARD_1:56,ENUMSET1:def 6;
hence p.0 = x1 & p.1 = x2 & p.2 = x3 & p.3 = x4 & p.4 = x5 & p.5 = x6 &
p.6 = x7 & p.7 = x8 by A1,A3,A4,A5,A6,Def3,A2;
thus p.8 = p.len p17 by Th46
.= x9 by A1,Th33;
end;
:: K.P. 12.2009
theorem :: FINSEQ_2:7
n <len p implies (p^q).n=p.n
proof
assume n <len p;
then n in dom p by Lm1;
hence thesis by Def3;
end;
theorem :: FINSEQ_2:10
len p <= n implies (p|n) = p
proof
assume len p<=n;
then Segm len p c= Segm n by NAT_1:39;
hence thesis by RELAT_1:68;
end;
theorem Th50: :: FINSEQ_1:11
n <=len p & k in n implies
(p|n).k = p.k & k in dom p
proof
assume that
A1: n <=len p and
A2: k in n;
A3: Segm n c= Segm len p by A1,NAT_1:39;
then n = dom p /\ n by XBOOLE_1:28
.= dom(p|n) by RELAT_1:61;
hence thesis by A2,A3,FUNCT_1:47;
end;
theorem Th51: :: FINSEQ_1:12
n <= len p implies len(p|n) = n
proof
assume n <= len p;
then Segm n c= Segm len p by NAT_1:39;
hence thesis by RELAT_1:62;
end;
theorem :: FINSEQ_1:13
len(p|n) <= n
proof
Segm len(p|n) c= Segm n by RELAT_1:58;
hence thesis by NAT_1:39;
end;
theorem Th53: :: FINSEQ_1:14
len p = n+1 implies p = (p|n) ^ <% p.n %>
proof
set pn = p|n;
set x=p.n;
assume
A1: len p = n+1;
then A2: n < len p by NAT_1:13;
then A3: len pn = n by Th51;
A4: now
let m be Nat;
assume m in dom p;
then m<len p by Lm1;
then
A5: m <= len pn by A1,A3,NAT_1:13;
now
per cases;
case
m = len pn;
hence p.m = (pn^<%x%>).m by A3,Th33;
end;
case
m <> len pn;
then m< len pn by A5,XXREAL_0:1;
then
A6: m in dom pn by Lm1;
hence (pn^<%x%>).m = pn.m by Def3
.= p.m by A2,A3,A6,Th50;
end;
end;
hence p.m = (pn^<%x%>).m;
end;
len (pn^<%x%>) = n + len <%x%> by A3,Def3
.= len p by A1,Def4;
hence thesis by A4;
end;
theorem Th54: :: CATALAN2:1
(p^q)|dom p = p
proof
set r=(p^q)|(dom p);
A1: now
let k such that
A2: k < len p;
A3: k in dom p by A2,Lm1;
then
A4: (p^q).k=p.k by Def3;
k+0<len p+len q by A2,XREAL_1:8;
then k in Segm(len p+len q) by NAT_1:44;
then k in dom (p^q) by Def3;
then k in dom (p^q)/\ dom p by A3,XBOOLE_0:def 4;
hence r.k=p.k by A4,FUNCT_1:48;
end;
dom p c= dom (p^q) by Th19;
then len r= len p by RELAT_1:62;
hence thesis by A1,Th8;
end;
theorem :: CATALAN2:2
n <= dom p implies (p^q)|n = p|n
proof
assume n <= dom p;
then Segm n c= Segm len p by NAT_1:39;
then ((p^q)|dom p)|n=(p^q)|n by RELAT_1:74;
hence thesis by Th54;
end;
theorem :: CATALAN2:3
n = dom p + k implies (p^q)|n = p^(q|k)
proof
assume
A1: n = dom p + k;
now
per cases;
suppose
A2: n>=len (p^q);
then n>=len p+len q by Def3;
then Segm len q c= Segm k by NAT_1:39,A1,XREAL_1:8;
then
A3: q|k = q by RELAT_1:68;
Segm len(p^q) c= Segm n by A2,NAT_1:39;
hence thesis by A3,RELAT_1:68;
end;
suppose
A4: n<len (p^q);
then
A5: len ((p^q)|n)=n by Th10;
n<len p+len q by A4,Def3;
then k < len q by A1,XREAL_1:6;
then len (q|k)=k by Th10;
then
A6: len (p^(q|k))=len p + k by Def3;
now
let m be Nat such that
A7: m in dom ((p^q)|n);
A8: m < len ((p^q)|n) by A7,Lm1;then
m <len (p^q) by A4,A5,XXREAL_0:2;
then
A9: m in len (p^q) by Lm1;
m in n by A4,Th10,A7;
then
A10: m in dom (p^q) /\ n by A9,XBOOLE_0:def 4;
then
A11: ((p^q)|n).m=(p^q).m by FUNCT_1:48;
now
per cases;
suppose
m<len p;
then m in dom p by Lm1;
then (p^(q|k)).m=p.m & (p^q).m=p.m by Def3;
hence ((p^q)|n).m=(p^(q|k)).m by A10,FUNCT_1:48;
end;
suppose
A12: m>=len p;
m < len (p^q) by A4,A5,A8,XXREAL_0:2;
then
A13: q.(m-len p)=(p^q).m by A12,Th17;
A14: m-len p+len p< len (p^q) by A4,A5,A8,XXREAL_0:2;
A15: m-len p is Nat by A12,NAT_1:21;
len (p^q)=len p+len q by Def3;
then m-len p<len q by A14,XREAL_1:6;
then
A16: m-len p in len q by A15,Lm1;
m-len p < k by A1,A5,A14,A8,XREAL_1:6;
then m-len p in Segm k by A15,NAT_1:44;
then
A17: m-len p in k/\dom q by A16,XBOOLE_0:def 4;
(p^(q|k)).m=(q|k).(m-len p) by A1,A6,A5,A12,A8,Th17;
hence ((p^q)|n).m=(p^(q|k)).m by A11,A13,A17,FUNCT_1:48;
end;
end;
hence ((p^q)|n).m=(p^(q|k)).m;
end;
hence thesis by A6,A1,A4,Th10;
end;
end;
hence thesis;
end;
theorem :: CATALAN2:4
ex q st p = (p|n)^q
proof
now
per cases;
suppose
n > len p;
then Segm len p c= Segm n by NAT_1:39;
then
A1: p|n=p by RELAT_1:68;
p^{}=p;
hence thesis by A1;
end;
suppose
n <= len p;
then reconsider n1=len p-n as Element of NAT by NAT_1:21;
defpred P[Nat] means for k st k= len p-$1 holds ex q st p=(p|k)^q;
A2: for m be Nat st P[m] holds P[m+1]
proof
let m be Nat such that
A3: P[m];
let k such that
A4: k = len p-(m+1);
consider q such that
A5: p = (p|(k+1))^q by A3,A4;
Segm k c= Segm(k+1) by NAT_1:39,11;
then
A6: (p|(k+1))|k =p|k by RELAT_1:74;
len p-m<=len p-0 by XREAL_1:10;
then len (p | (k+1)) = k+1 by Th51,A4;
then p|(k+1)=(p|(k+1))|k^<%(p|(k+1)).k%> by Th53;
then p=(p|k)^(<%(p|(k+1)).k%>^q) by A5,A6,Th25;
hence thesis;
end;
p|(len p-0)=p & p^{}=p;
then
A7: P[0];
A8: for m be Nat holds P[m] from NAT_1:sch 2(A7,A2);
n = len p-n1;
hence thesis by A8;
end;
end;
hence thesis;
end;
theorem :: FLANG_1:10
len p = n + k implies
ex q1, q2 being XFinSequence st
len q1 = n & len q2 = k & p = q1 ^ q2
proof
defpred P[Nat] means for p being XFinSequence, i, j be Nat
st len p = $1 & len p =
i + j ex q1, q2 being XFinSequence st len q1 = i & len q2 = j & p = q1 ^ q2;
A1: now
let n;
assume
A2: P[n];
thus P[n + 1]
proof
let p be XFinSequence;
let i, j be Nat;
assume that
A3: len p = n + 1 and
A4: len p = i + j;
per cases;
suppose
A5: j = 0;
take q1 = p;
take q2 = {};
thus thesis by A4,A5;
end;
suppose
j > 0;
then consider k such that
A6: j = k + 1 by NAT_1:6;
p <> {} by A3;
then consider q being XFinSequence, x such that
A7: p = q ^ <%x%> by Th37;
A8: n + 1 = len q + len <%x%> by A3,A7,Def3
.= len q + 1 by Th30;
n = i + k by A3,A4,A6;
then consider q1, q2 being XFinSequence such that
A9: len q1 = i and
A10: len q2 = k and
A11: q = q1 ^ q2 by A2,A8;
A12: len (q2 ^ <%x%>) = len q2 + len <%x%> by Def3
.= j by A6,A10,Th30;
p = q1 ^ (q2 ^ <%x%>) by A7,A11,Th25;
hence thesis by A9,A12;
end;
end;
end;
A13: P[0]
proof
let p be XFinSequence;
let i, j be Nat;
assume that
A14: len p = 0 and
A15: len p = i + j;
A16: p = {} ^ {} by A14;
len {} = i by A14,A15;
hence thesis by A15,A16;
end;
for n holds P[n] from NAT_1:sch 2(A13, A1);
hence thesis;
end;
theorem :: FSM_3:6
<%x%>^p = <%y%>^q implies x = y & p = q
proof
assume A1: <%x%>^p = <%y%>^q;
(<%x%>^p).0 = x by Th32;
then x = y by A1,Th32;
hence thesis by A1,Th26;
end;
definition
let D be set,q be FinSequence of D;
func FS2XFS q -> XFinSequence of D means :Def8:
len it = len q & for i being Nat st i < len q holds q.(i+1) = it.i;
existence
proof
deffunc F(Nat) =q.($1 +1);
ex p being XFinSequence st len p = len q & for k be Nat
st k in len q holds p.k=F(k) from XSeqLambda;
then consider p being XFinSequence such that
A1: len p = len q and
A2: for k be Nat st k in Segm len q holds p.k=F(k);
rng p c= D
proof
let y be object;
A3: rng q c= D by FINSEQ_1:def 4;
assume y in rng p;
then consider x being object such that
A4: x in dom p and
A5: y=p.x by FUNCT_1:def 3;
reconsider nx=x as Element of NAT by A4;
A6: nx+1<=len q by NAT_1:13,A1,A4,Lm1;
0+1<=nx+1 by NAT_1:13;
then nx+1 in Seg len q by A6,FINSEQ_1:1;
then nx+1 in dom q by FINSEQ_1:def 3;
then
A7: q.(nx+1) in rng q by FUNCT_1:def 3;
p.nx= q.(nx +1) by A1,A2,A4;
hence thesis by A5,A7,A3;
end;
then
A8: p is XFinSequence of D by RELAT_1:def 19;
for i being Nat st i<len q holds q.(i+1)=p.i by A2,NAT_1:44;
hence thesis by A1,A8;
end;
uniqueness
proof
thus for p1,p2 being XFinSequence of D st
(len p1=len q & for i be Nat st i<len q holds
q.(i+1)=p1.i)& (len p2=len q & for i be Nat
st i<len q holds q.(i+1)=p2.i) holds
p1=p2
proof
let p1,p2 be XFinSequence of D;
assume that
A9: len p1=len q and
A10: for i be Nat st i<len q holds q.(i+1)=p1.i and
A11: len p2=len q and
A12: for i be Nat st i<len q holds q.(i+1)=p2.i;
for i be Nat st i<len p1 holds p1.i=p2.i
proof
let i be Nat;
assume
A13: i<len p1;
then q.(i+1)=p1.i by A9,A10;
hence thesis by A9,A12,A13;
end;
hence thesis by A9,A11,Th8;
end;
end;
end;
reserve i for Nat;
definition
let q be XFinSequence;
func XFS2FS q -> FinSequence means :Def9A:
len it = len q & for i be Nat st 1 <= i & i <= len q holds q.(i-1) = it.i;
existence
proof
deffunc F(Nat) = q.($1-1);
ex p being FinSequence st len p = len q &
for k being Nat st k in dom p holds p.k=F(k) from FINSEQ_1:sch 2;
then consider p being FinSequence such that
A1: len p = len q and
A2: for k being Nat st k in dom p holds p.k=F(k);
A11: dom p = Seg len q by A1,FINSEQ_1:def 3;
for i be Nat st 1<=i & i<=len q holds q.(i-1)=p.i by A2,A11,FINSEQ_1:1;
hence thesis by A1;
end;
uniqueness
proof
let p1,p2 be FinSequence;
assume that
A12: len p1=len q and
A13: for i st 1<=i & i<=len q holds q.(i-1)=p1.i and
A14: len p2=len q and
A15: for i st 1<=i & i<=len q holds q.(i-1)=p2.i;
for i be Nat st 1<=i & i<=len p1 holds p1.i=p2.i
proof
let i be Nat;
assume
A16: 1<=i & i<=len p1;
then q.(i-1)=p1.i by A12,A13;
hence thesis by A12,A15,A16;
end;
hence thesis by A12,A14,FINSEQ_1:14;
end;
end;
definition
let D be set, q be XFinSequence of D;
redefine func XFS2FS q -> FinSequence of D; :: redefines XFS2FS (AFINSQ_1, definition)
coherence
proof
set p = XFS2FS q;
A1: len p = len q by Def9A;
rng p c= D
proof
let y be object;
A3: rng q c= D by RELAT_1:def 19;
assume y in rng p;
then consider x being object such that
A4: x in dom p and
A5: y=p.x by FUNCT_1:def 3;
reconsider nx=x as Element of NAT by A4;
A6: nx in Seg len q by A1,A4,FINSEQ_1:def 3;
then f: 1<=nx by FINSEQ_1:1;
then nx-1>=0 by XREAL_1:48; then
A7: nx-1=nx-'1 by XREAL_0:def 2;
A8: nx-1<nx-1+1 by A7,NAT_1:13;
F: nx<=len q by A6,FINSEQ_1:1;
then nx-1<len q by A8,XXREAL_0:2;
then a9: nx-1 in dom q by A7,Lm1;
AA: 1<=nx & nx<=len q by F,f;
A9: q.(nx-1) in rng q by FUNCT_1:def 3,a9;
p.nx = q.(nx -1) by Def9A,AA;
hence thesis by A5,A9,A3;
end;
hence thesis by FINSEQ_1:def 4;
end;
end;
theorem
for D being set, n being Nat, r being set st r in D holds
n-->r is XFinSequence of D;
definition
let D be non empty set;
let q be FinSequence of D, n be Nat;
assume that
A1: n > len q and
A2: NAT c= D;
func FS2XFS*(q,n) -> non empty XFinSequence of D means
len q = it.0 &
len it = n &
(for i being Nat st 1 <= i & i <= len q holds it.i = q.i) &
for j being Nat st len q < j & j < n holds it.j = 0;
existence
proof
reconsider x=len q as Element of D by A2;
reconsider r=0 as Element of D by A2;
reconsider q5= ((n-'len q-'1)-->r) as XFinSequence of D;
<%x%> ^ (FS2XFS q) <>{} by Th27;
then reconsider
p0=<%x%> ^ (FS2XFS q)^q5 as non empty XFinSequence of D by Th27;
A3: 0 in dom (<%x%>) by Lm1;
A4: len <%x%>=1 by Def4;
0 in Segm(len <%x%> + len (FS2XFS q)) by NAT_1:44;
then 0 in len (<%x%> ^ (FS2XFS q)) by Def3;
then
A5: p0.0=(<%x%> ^ (FS2XFS q)).0 by Def3
.=(<%x%>).0 by A3,Def3
.=x;
A6: for i st 1<=i & i<= len q holds p0.i=q.i
proof
let i;
assume that
A7: 1<=i and
A8: i<= len q;
A9: i-'1=i-1 by XREAL_0:def 2,A7,XREAL_1:48;
i<i+1 by NAT_1:13;
then i-1<i+1-1 by XREAL_1:9;
then
A10: i-'1 <len q by A8,A9,XXREAL_0:2;
then i-'1 in Segm len q by NAT_1:44;
then
A11: i-'1 in len (FS2XFS q) by Def8;
i<1+len q by A8,NAT_1:13;
then i< (len (<%x%>)+len (FS2XFS q)) by A4,Def8;
then i in Segm(len (<%x%>)+len (FS2XFS q)) by NAT_1:44;
then i in len (<%x%> ^ (FS2XFS q)) by Def3;
then p0.i =(<%x%>^(FS2XFS q)).(1+(i-'1)) by A9,Def3
.=(FS2XFS q).(i-'1) by A4,A11,Def3
.=q.(i-'1+1) by A10,Def8
.=q.i by A9;
hence thesis;
end;
A12: n-len q>0 by A1,XREAL_1:50;
then
A13: n-'len q=n-len q by XREAL_0:def 2;
then n-'len q>=0+1 by A12,NAT_1:13;
then
A14: n-'len q -1>=0 by XREAL_1:48;
A15: len q5=(n-'len q-'1);
A16: for j being Nat st len q<j & j<n holds p0.j=0
proof
let j be Nat;
assume that
A17: len q<j and
A18: j<n;
A19: len (<%x%> ^ (FS2XFS q)) =len (<%x%>) + len (FS2XFS q) by Def3
.=1+len q by A4,Def8;
len q<n by A17,A18,XXREAL_0:2;
then
A20: n-len q>0 by XREAL_1:50;
then
A21: n-'len q=n-len q by XREAL_0:def 2;
then n-len q>=0+1 by A20,NAT_1:13;
then n-'len q-1>=0 by A21,XREAL_1:48;
then
A22: n-'len q-'1 =n-(len q+1) by A21,XREAL_0:def 2;
1+len q<=j by A17,NAT_1:13; then
A23: j-'(1+len q)=j-(1+len q) by XREAL_0:def 2,XREAL_1:48;
j-(len q+1)< n-(len q+1) by A18,XREAL_1:9;
then
A24: j-'len (<%x%> ^ (FS2XFS q)) in Segm(n-'len q-'1) by A19,A23,A22,NAT_1:44;
j =len (<%x%> ^ (FS2XFS q))+(j-'len (<%x%> ^ (FS2XFS q))) by A19,A23;
then p0.j=q5.(j-'len (<%x%> ^ (FS2XFS q))) by A15,A24,Def3
.=0;
hence thesis;
end;
len p0=len (<%x%> ^ (FS2XFS q)) + len q5 by Def3
.=len <%x%> + len (FS2XFS q) + len q5 by Def3
.= 1 + len (FS2XFS q) + len q5 by Th30
.=1 + len q + len q5 by Def8
.=(n-(len q+1))+(len q+1) by A13,A14,XREAL_0:def 2
.=n;
hence thesis by A5,A6,A16;
end;
uniqueness
proof
let p1,p2 be non empty XFinSequence of D;
assume that
A25: len q = (p1.0) and
A26: len p1=n and
A27: for i st 1<=i & i<= len q holds p1.i=q.i and
A28: for j being Nat st len q<j & j<n holds p1.j=0 and
A29: len q = (p2.0) and
A30: len p2=n and
A31: for i st 1<=i & i<= len q holds p2.i=q.i and
A32: for j being Nat st len q<j & j<n holds p2.j=0;
for i be Nat st i<n holds p1.i=p2.i
proof
let i be Nat;
assume i<n; then
A33: i<0+1 or 1<=i & i<=len q or len q<i & i<n;
now
per cases by A33,NAT_1:13;
case i=0;
hence thesis by A25,A29;
end;
case
A34: 1<=i & i<=len q;
then p1.i=q.i by A27;
hence thesis by A31,A34;
end;
case
A35: len q<i & i<n;
then p1.i=0 by A28;
hence thesis by A32,A35;
end;
end;
hence thesis;
end;
hence thesis by A26,A30,Th8;
end;
end;
reserve m for Nat,
D for non empty set;
definition
let D be non empty set;
let p be XFinSequence of D;
assume that
A1: p.0 is Nat and
A2: p.0 in len p;
func XFS2FS*(p) -> FinSequence of D means :Def11:
for m be Nat st m = p.0 holds
len it =m & for i st 1<=i & i<= m holds it.i=p.i;
existence
proof
reconsider m0=p.0 as Element of NAT by A1,ORDINAL1:def 12;
deffunc F(set)= p.$1;
ex q being FinSequence st len q = m0 & for k being Nat st k in dom q
holds q.k=F(k) from FINSEQ_1:sch 2;
then consider q being FinSequence such that
A3: len q = m0 and
A4: for k being Nat st k in dom q holds q.k=F(k);
rng q c= D
proof
A5: m0 < len p by A2,Lm1;
let y be object;
assume y in rng q;
then consider x being object such that
A6: x in dom q and
A7: y=q.x by FUNCT_1:def 3;
reconsider k0=x as Element of NAT by A6;
k0 in Seg m0 by A3,A6,FINSEQ_1:def 3;
then k0<=m0 by FINSEQ_1:1;
then k0 < len p by A5,XXREAL_0:2;
then
A8: k0 in dom p by Lm1;
y=p.k0 by A4,A6,A7;
then rng p c= D & y in rng p by A8,FUNCT_1:def 3,RELAT_1:def 19;
hence thesis;
end;
then reconsider q0=q as FinSequence of D by FINSEQ_1:def 4;
A9: dom q = Seg m0 by A3,FINSEQ_1:def 3;
for m be Nat st
m = (p.0) holds len q0 =m & for i st 1<=i & i<= m holds q0.i =p.i
by A4,A9,FINSEQ_1:1,A3;
hence thesis;
end;
uniqueness
proof
reconsider m2=p.0 as Nat by A1;
let g1,g2 be FinSequence of D;
assume that
A10: for m st m = p.0 holds len g1 =m & for i st 1<=i & i<= m holds g1
.i=p. i and
A11: for m st m = p.0 holds len g2 =m & for i st 1<=i & i<= m holds g2
. i=p.i;
A12: len g1=m2 by A10;
A13: for i be Nat st 1<=i & i<=len g1 holds g1.i=g2.i
proof
let i be Nat;
assume
A14: 1<=i & i<=len g1;
then g1.i=p.i by A10,A12;
hence thesis by A11,A12,A14;
end;
len g2=m2 by A11;
hence thesis by A10,A13,FINSEQ_1:14;
end;
end;
theorem
for p being XFinSequence of D st p.0=0 & 0<len p holds
XFS2FS*(p)={}
proof
let p be XFinSequence of D;
assume that
A1: p.0=0 and
A2: 0<len p;
set q= XFS2FS*(p);
0 in len p by A2,Lm1;
then len q=0 by A1,Def11;
hence thesis;
end;
:: from EXTPRO_1, 2010.01.11, A.T.
definition
let F be Function;
attr F is initial means
:Def12:
for m,n being Nat st n in dom F & m < n holds m in dom F;
end;
registration
cluster empty -> initial for Function;
coherence;
end;
registration
cluster -> initial for XFinSequence;
coherence
proof
let p be XFinSequence;
let m,n being Nat such that
A1: n in dom p;
assume m < n;
then m in Segm n by NAT_1:44;
hence m in dom p by A1,ORDINAL1:10;
end;
end;
registration
cluster -> NAT-defined for XFinSequence;
coherence
proof let f be XFinSequence;
thus dom f c= NAT;
end;
end;
theorem Th62:
for F being non empty initial NAT-defined Function holds 0 in dom F
proof
let F be non empty initial NAT-defined Function;
consider x being object such that
A1: x in dom F by XBOOLE_0:def 1;
dom F c= NAT by RELAT_1:def 18;
then reconsider x as Element of NAT by A1;
x = 0 or 0 < x;
hence 0 in dom F by A1,Def12;
end;
registration
cluster initial finite NAT-defined -> Sequence-like for Function;
coherence
proof let F be Function;
assume
A1: F is initial finite NAT-defined;
thus dom F is epsilon-transitive
proof let x be set;
assume
A2: x in dom F;
then reconsider i = x as Nat by A1;
let y be object;
assume y in x; then
A3: y in Segm i;
then reconsider j = y as Nat;
thus y in dom F by A1,A2,NAT_1:44,A3;
end;
let x,y be set;
assume x in dom F & y in dom F;
then reconsider x,y as Ordinal by A1;
x in y or x = y or y in x by ORDINAL1:14;
hence thesis;
end;
end;
theorem
for F being finite initial NAT-defined Function
for n being Nat holds
n in dom F iff n < card F by Lm1;
:: from AMISTD_2, 2010.04.16, A.T.
theorem
for F being initial NAT-defined Function,
G being NAT-defined Function st dom F = dom G holds G is initial by Def12;
theorem
for F being initial NAT-defined finite Function
holds dom F = { k where k is Element of NAT: k < card F }
proof
let F be initial NAT-defined finite Function;
hereby
let x be object;
assume
A1: x in dom F;
then reconsider f = x as Element of NAT;
f < card F by A1,Lm1;
hence x in { k where k is Element of NAT: k < card F };
end;
let x be object;
assume x in { k where k is Element of NAT: k < card F };
then ex k being Element of NAT st x = k & k < card F;
hence thesis by Lm1;
end;
theorem
for F being non empty XFinSequence,
G be non empty NAT-defined finite Function
st F c= G & LastLoc F = LastLoc G
holds F = G
proof
let F be initial non empty NAT-defined finite Function, G be non empty NAT
-defined finite Function such that
A1: F c= G and
A2: LastLoc F = LastLoc G;
dom F = dom G
proof
thus dom F c= dom G by A1,GRFUNC_1:2;
let x be object;
assume
A3: x in dom G;
dom G c= NAT by RELAT_1:def 18;
then reconsider x as Element of NAT by A3;
A4: LastLoc F in dom F by VALUED_1:30;
x <= LastLoc F by A2,A3,VALUED_1:32;
then x < LastLoc F or x = LastLoc F by XXREAL_0:1;
hence thesis by A4,Def12;
end;
hence thesis by A1,GRFUNC_1:3;
end;
theorem Th67:
for F being non empty XFinSequence holds LastLoc F = card F -' 1
proof
let F be initial non empty NAT-defined finite Function;
consider k being Nat such that
A1: LastLoc F = k;
reconsider k as Element of NAT by ORDINAL1:def 12;
k < card F by A1,Lm1,VALUED_1:30;
then
A2: k <= card F -' 1 by NAT_D:49;
per cases by A2,XXREAL_0:1;
suppose
k < card F -' 1;
then k+1 < card F -' 1 + 1 by XREAL_1:6;
then k+1 < card F by NAT_1:14,XREAL_1:235;
then
A3: k+1 <= k by A1,VALUED_1:32,Lm1;
k <= k+1 by NAT_1:11;
then k+0 = k+1 by A3,XXREAL_0:1;
hence thesis;
end;
suppose
k = card F -' 1;
hence thesis by A1;
end;
end;
theorem
for F being initial non empty NAT-defined finite Function holds
FirstLoc F = 0 by Th62,VALUED_1:35;
registration
let F be initial non empty NAT-defined finite Function;
cluster CutLastLoc F -> initial;
coherence
proof
set G = CutLastLoc F;
per cases;
suppose G is empty;
then reconsider H = G as empty finite Function;
H is initial;
hence thesis;
end;
suppose G is non empty;
then reconsider G as non empty finite Function;
G is initial
proof
let m,l be Nat such that
A1: l in dom G and
A2: m < l;
set M = dom F;
reconsider R = {[LastLoc F, F.LastLoc F]} as Relation;
a3: R = LastLoc F .--> (F.LastLoc F) by FUNCT_4:82; then
A4: dom F \ dom R = dom G by VALUED_1:36; then
l in dom F by A1,XBOOLE_0:def 5; then
A5: m in dom F by A2,Def12;
l in M by A4,A1,XBOOLE_0:def 5;
then m <> LastLoc F by A2,XXREAL_2:def 8;
then not m in {LastLoc F} by TARSKI:def 1;
hence thesis by a3,A4,A5,XBOOLE_0:def 5;
end;
hence thesis;
end;
end;
end;
reserve l for Nat;
theorem
for I being finite initial NAT-defined Function, J being Function
holds dom I misses dom Shift(J,card I)
proof let I be finite initial NAT-defined Function, J be Function;
assume
A1: dom I meets dom Shift(J,card I);
dom Shift(J,card I) = { l+card I: l in dom J } by VALUED_1:def 12;
then consider x being object such that
A2: x in dom I and
A3: x in { l+card I: l in dom J } by A1,XBOOLE_0:3;
consider l such that
A4: x = l+card I and
l in dom J by A3;
thus contradiction by NAT_1:11,A2,A4,Lm1;
end;
:: from SCMPDS_4, 2010.05.14, A.T.
theorem
not m in dom p implies not m+1 in dom p
proof
assume not m in dom p; then
A1: m >= card p by Lm1;
m+1 >= m by NAT_1:11;
hence thesis by Lm1,A1,XXREAL_0:2;
end;
:: from SCM_COMP, 2010.05.16, A.T.
registration let D be set;
cluster D^omega -> functional;
coherence by Def7;
end;
registration let D be set;
cluster -> finite Sequence-like for Element of D^omega;
coherence by Def7;
end;
definition let D be set;
let f be XFinSequence of D;
func Down f -> Element of D^omega equals
f;
coherence by Def7;
end;
definition let D be set;
let f be XFinSequence of D, g be Element of D^omega;
redefine func f^g -> Element of D^omega; :: redefines ^ (AFINSQ_1, redefinition) → ^ (ORDINAL4, definition)
coherence
proof
reconsider g as XFinSequence of D by Def7;
f^g is XFinSequence of D;
hence thesis by Def7;
end;
end;
definition let D be set;
let f, g be Element of D^omega;
redefine func f^g -> Element of D^omega; :: redefines ^ (AFINSQ_1, redefinition) → ^ (ORDINAL4, definition)
coherence
proof
reconsider f,g as XFinSequence of D by Def7;
f^g is XFinSequence of D;
hence thesis by Def7;
end;
end;
:: missing, 2010.05.15, A.T.
theorem Th71:
p c= p^q
proof
A1: dom p c= dom(p^q) by Th19;
for x being object st x in dom p holds (p^q).x = p.x by Def3;
hence thesis by A1,GRFUNC_1:2;
end;
theorem Th72:
len(p^<%x%>) = len p + 1
proof
thus len(p^<%x%>) = len p + len<%x%> by Def3
.= len p + 1 by Th30;
end;
theorem
<%x,y%> = (0,1) --> (x,y)
proof
A1: dom<%x,y%> = {0,1} by Th35,CARD_1:50;
A2: <%x,y%>.0 = x;
<%x,y%>.1 = y;
hence <%x,y%> = (0,1) --> (x,y) by A1,A2,FUNCT_4:66;
end;
reserve M for Nat;
theorem Th74:
p^q = p +* Shift(q, card p)
proof
A1: dom Shift(q, card p) = { M+card p:M in dom q } by VALUED_1:def 12;
for x being object
holds x in dom(p^q) iff x in dom p or x in dom Shift(q, card p)
proof let x be object;
thus x in dom(p^q) implies x in dom p or x in dom Shift(q, card p)
proof assume
A2: x in dom(p^q);
then reconsider k = x as Nat;
per cases by A2,Th18;
suppose k in dom p;
hence x in dom p or x in dom Shift(q, card p);
end;
suppose ex n st n in dom q & k=len p + n;
hence x in dom p or x in dom Shift(q, card p) by A1;
end;
end;
assume
A3: x in dom p or x in dom Shift(q, card p);
per cases by A3;
suppose
A4: x in dom p;
dom p c= dom(p^q) by Th19;
hence x in dom(p^q) by A4;
end;
suppose x in dom Shift(q, card p);
then ex M st x = M+card p & M in dom q by A1;
hence x in dom(p^q) by Th21;
end;
end;
then
A5: dom(p^q) = dom p \/ dom Shift(q, card p) by XBOOLE_0:def 3;
for x being object st x in dom p \/ dom Shift(q, card p)
holds (x in dom Shift(q, card p) implies (p^q).x = Shift(q, card p).x) &
(not x in dom Shift(q, card p) implies (p^q).x = p.x)
proof let x be object such that
A6: x in dom p \/ dom Shift(q, card p);
hereby assume
A7: x in dom Shift(q, card p);
then reconsider k = x as Nat;
consider M such that
A8: x = M+card p and
A9: M in dom q by A7,A1;
set m = k -' len p;
A10: len p + m = k by A8,NAT_D:34;
hence (p^q).x = q.m by A8,A9,Def3
.= Shift(q, card p).x by A8,A9,A10,VALUED_1:def 12;
end;
assume not x in dom Shift(q, card p);
then x in dom p by A6,XBOOLE_0:def 3;
hence (p^q).x = p.x by Def3;
end;
hence p^q = p +* Shift(q, card p) by A5,FUNCT_4:def 1;
end;
theorem
p +* (p ^ q) = p ^ q & (p ^ q) +* p = p ^ q by Th71,FUNCT_4:97,98;
reserve m,n for Nat;
theorem Th76:
for I being finite initial NAT-defined Function, J being Function
holds dom Shift(I,n) misses dom Shift(J,n+card I)
proof let I be finite initial NAT-defined Function, J be Function;
assume
A1: dom Shift(I,n) meets dom Shift(J,n+card I);
dom Shift(J,n+card I) = { l+(n+card I): l in dom J } by VALUED_1:def 12;
then consider x being object such that
A2: x in dom Shift(I,n) and
A3: x in { l+(n+card I): l in dom J } by A1,XBOOLE_0:3;
dom Shift(I,n) = { m+n:m in dom I } by VALUED_1:def 12;
then consider m such that
A4: x = m+n and
A5: m in dom I by A2;
consider l such that
A6: x = l+(n+card I) and
l in dom J by A3;
m < card I by A5,Lm1;
hence contradiction by NAT_1:11,A4,A6,XREAL_1:6;
end;
theorem Th77:
Shift(p,n) c= Shift(p^q,n)
proof
p^q = p +* Shift(q, card p) by Th74;
then
A1: Shift(p^q,n) = Shift(p,n) +* Shift(Shift(q,card p),n) by VALUED_1:23;
Shift(Shift(q,card p),n) = Shift(q,n+card p) by VALUED_1:21;
then dom Shift(p,n) misses dom Shift(Shift(q,card p),n) by Th76;
hence Shift(p,n) c= Shift(p^q,n) by A1,FUNCT_4:32;
end;
theorem Th78:
Shift(q,n+card p) c= Shift(p^q,n)
proof
A1: Shift(Shift(q,card p),n) = Shift(q,n+card p) by VALUED_1:21;
p^q = p +* Shift(q, card p) by Th74;
then Shift(p^q,n) = Shift(p,n) +* Shift(Shift(q,card p),n) by VALUED_1:23;
hence thesis by A1,FUNCT_4:25;
end;
theorem
Shift(p^q,n) c= X implies Shift(p,n) c= X
proof assume
A1: Shift(p^q,n) c= X;
Shift(p,n) c= Shift(p^q,n) by Th77;
hence Shift(p,n) c= X by A1;
end;
theorem
Shift(p^q,n) c= X implies Shift(q,n+card p) c= X
proof assume
A1: Shift(p^q,n) c= X;
Shift(q,n+card p) c= Shift(p^q,n) by Th78;
hence thesis by A1;
end;
registration let F be initial non empty NAT-defined finite Function;
cluster CutLastLoc F -> initial;
coherence;
end;
definition let x1,x2,x3,x4 be object;
func <%x1,x2,x3,x4%> -> set equals
<%x1%>^<%x2%>^<%x3%>^<%x4%>;
coherence;
end;
registration let x1,x2,x3,x4 be object;
cluster <%x1,x2,x3,x4%> -> Function-like Relation-like;
coherence;
end;
registration let x1,x2,x3,x4 be object;
cluster <%x1,x2,x3,x4%> -> finite Sequence-like;
coherence;
end;
reserve x1,x2,x3,x4 for object;
theorem
len<%x1,x2,x3,x4%> = 4
proof
thus len<%x1,x2,x3,x4%>
= len<%x1,x2,x3%> + 1 by Th72
.= 3 + 1 by Th36
.= 4;
end;
Lm3:
<%x1,x2,x3,x4%>.1 = x2 &
<%x1,x2,x3,x4%>.2 = x3 &
<%x1,x2,x3,x4%>.3 = x4
proof
A1: len<%x1,x2,x3%> = 3 by Th36;
then
A2: 1 in dom<%x1,x2,x3%> by Lm1;
thus <%x1,x2,x3,x4%>.1
=<%x1,x2,x3%>.1 by A2,Def3
.= x2;
A3: 2 in dom<%x1,x2,x3%> by A1,Lm1;
thus <%x1,x2,x3,x4%>.2
=<%x1,x2,x3%>.2 by A3,Def3
.= x3;
thus <%x1,x2,x3,x4%>.3 = x4 by A1,Th33;
end;
registration
let x1,x2,x3,x4 be object;
reduce <%x1,x2,x3,x4%>.0 to x1;
reducibility
proof
thus <%x1,x2,x3,x4%>.0
=(<%x1%>^<%x2,x3%>^<%x4%>).0 by Th25
.=(<%x1%>^<%x2,x3,x4%>).0 by Th25
.= x1 by Th32;
end;
reduce <%x1,x2,x3,x4%>.1 to x2;
reducibility by Lm3;
reduce <%x1,x2,x3,x4%>.2 to x3;
reducibility by Lm3;
reduce <%x1,x2,x3,x4%>.3 to x4;
reducibility by Lm3;
end;
::$CT
theorem
k < len p iff k in dom p by Lm1;
reserve e,u for object;
theorem
Segm(n+1) --> e = (Segm n --> e)^<%e%>
proof
set p = Segm n --> e, q = Segm(n+1) --> e;
A2: dom q = len p + len <%e%> by Th31;
A3: for k st k in dom p holds q.k=p.k
proof let k;
assume
A4: k in dom p;
p c= q by FUNCT_4:4,NAT_1:63;
hence q.k=p.k by A4,GRFUNC_1:2;
end;
for k st k in dom<%e%> holds q.(len p + k) = <%e%>.k
proof let k such that
A5: k in dom<%e%>;
A6: k = 0 by A5,TARSKI:def 1;
len p < n+1 by NAT_1:13;
then len p + 0 in Segm(n+1) by NAT_1:44;
hence q.(len p + k) = <%e%>.k by A6,FUNCOP_1:7;
end;
hence thesis by A2,A3,Def3;
end;
theorem Th84:
dom Shift(<%e%>,card p) = {card p}
proof
for u holds u in dom Shift(<%e%>,card p) iff u = card p
proof let u;
thus u in dom Shift(<%e%>,card p) implies u = card p
proof
assume u in dom Shift(<%e%>,card p);
then u in { m+card p where m is Nat:m in dom <%e%> } by VALUED_1:def 12;
then consider m being Nat such that
A1: u = m+card p and
A2: m in dom <%e%>;
m = 0 by A2,TARSKI:def 1;
hence u = card p by A1;
end;
0 in 1 by CARD_1:49,TARSKI:def 1;
then 0 in dom <%e%> by Def4;
then 0+card p in dom Shift(<%e%>,card p) by VALUED_1:24;
hence thesis;
end;
hence thesis by TARSKI:def 1;
end;
theorem
dom(p^<%e%>) = dom p \/ {card p}
proof
thus dom(p^<%e%>) = dom(p +* Shift(<%e%>, card p)) by Th74
.= dom p \/ dom Shift(<%e%>,card p) by FUNCT_4:def 1
.= dom p \/ {card p} by Th84;
end;
theorem
<%x%> +~ (x,y) = <%y%>
proof
A1: dom(<%x%> +~ (x,y)) = dom<%x%> by FUNCT_4:99
.= Segm 1 by Th30;
then <%x%> +~ (x,y) is finite by FINSET_1:10;
then reconsider p = <%x%> +~ (x,y) as XFinSequence by A1,ORDINAL1:def 7;
A2: rng<%x%> = {x} by Th30;
then rng p c= {x} \ {x} \/ {y} by FUNCT_4:104;
then rng p c= {} \/ {y} by XBOOLE_1:37;
then
A3: rng p c= {y};
x in rng <%x%> by A2,TARSKI:def 1;
then y in rng p by FUNCT_4:101;
hence <%x%> +~ (x,y) = <%y%> by A1,Th30,A3,ZFMISC_1:33;
end;
theorem
for I being non empty XFinSequence
holds LastLoc I = card I - 1
proof let I be non empty XFinSequence;
A1: card I >= 0+1 by NAT_1:13;
thus LastLoc I = card I -' 1 by Th67
.= card I - 1 by A1,XREAL_1:233;
end;
begin ::: Addenda by Sebastian Koch
:: this holds more basically for any Sequence A, but since
:: the properties of Sequences of the form A ^ <%x%> are not in Mizar yet
:: I have no desire to formally introduce everything of that here, too
theorem
for p being XFinSequence, x being object holds last(p^<%x%>) = x
proof
let p be XFinSequence, x be object;
dom(p^<%x%>) = len p + 1 by Th72
.= len p +^ 1 by CARD_2:36
.= succ len p by ORDINAL2:31;
hence last(p^<%x%>) = (p^<%x%>).len p by ORDINAL2:6
.= x by Th33;
end;
:: the mirror theorem of BALLOT_1:5, but also for empty D
theorem Th12A:
for D being set, p being XFinSequence of D holds FS2XFS (XFS2FS p) = p
proof
let D be set, p be XFinSequence of D;
A1: len p = len XFS2FS p by Def9A;
A2: len XFS2FS p = len FS2XFS (XFS2FS p) by Def8;
for k being Nat st k < len p holds p.k = (FS2XFS (XFS2FS p)).k
proof
let k be Nat;
assume A3: k < len p;
then 0+1 <= k+1 & k+1 < len p +1 by XREAL_1:6;
then A4: 1 <= k+1 & k+1 <= len p by NAT_1:13;
thus p.k = p.(k+1-1)
.= (XFS2FS p).(k+1) by A4, Def9A
.= (FS2XFS (XFS2FS p)).k by A1, A3, Def8;
end;
hence thesis by A1, A2, Th8;
end;
registration
let D be set, f be XFinSequence of D;
reduce FS2XFS XFS2FS f to f;
reducibility by Th12A;
end;
theorem Th13:
for D being set, p being FinSequence of D, n being Nat
holds n+1 in dom p iff n in dom FS2XFS p
proof
let D be set, p be FinSequence of D, n be Nat;
hereby
assume n+1 in dom p;
then n+1 <= len p by FINSEQ_3:25;
then n+1-1 < len p-0 by XREAL_1:15;
then n < len FS2XFS p by Def8;
then n in Segm dom FS2XFS p by NAT_1:44;
hence n in dom FS2XFS p;
end;
assume n in dom FS2XFS p;
then n in Segm dom FS2XFS p;
then 0 <= n & n < len FS2XFS p by NAT_1:44;
then 0+1 <= n+1 & n < len p by Def8, XREAL_1:6;
then 1 <= n+1 & n+1 <= len p by NAT_1:13;
hence n+1 in dom p by FINSEQ_3:25;
end;
theorem Th14:
for D being set, p being XFinSequence of D, n being Nat
holds n in dom p iff n+1 in dom XFS2FS p
proof
let D be set, p be XFinSequence of D, n be Nat;
hereby
assume n in dom p;
then n in dom FS2XFS (XFS2FS p);
hence n+1 in dom XFS2FS p by Th13;
end;
assume n+1 in dom XFS2FS p;
then n in dom FS2XFS (XFS2FS p) by Th13;
hence thesis;
end;
registration
let D be set, p be one-to-one FinSequence of D;
cluster FS2XFS p -> one-to-one;
coherence
proof
now
let x1, x2 be object;
assume that
A1: x1 in dom FS2XFS p & x2 in dom FS2XFS p and
A2: (FS2XFS p).x1 = (FS2XFS p).x2;
reconsider n1 = x1, n2 = x2 as Nat by A1;
A3: n1 + 1 in dom p & n2 + 1 in dom p by A1, Th13;
then n1 + 1 <= len p & n2 + 1 <= len p by FINSEQ_3:25;
then A4: n1 < len p & n2 < len p by NAT_1:13;
p.(n1+1) = (FS2XFS p).n1 by A4, Def8
.= p.(n2+1) by A2, A4, Def8;
then n1 + 1 = n2 + 1 by A3, FUNCT_1:def 4;
hence x1 = x2;
end;
hence thesis;
end;
end;
registration
let D be set, p be one-to-one XFinSequence of D;
cluster XFS2FS p -> one-to-one;
coherence
proof
now
let x1, x2 be object;
assume that
A1: x1 in dom XFS2FS p & x2 in dom XFS2FS p and
A2: (XFS2FS p).x1 = (XFS2FS p).x2;
reconsider n1 = x1, n2 = x2 as Nat by A1;
1 <= n1 & n1 <= len XFS2FS p & 1 <= n2 & n2 <= len XFS2FS p
by A1, FINSEQ_3:25;
then A3: 1 <= n1 & n1 <= len p & 1 <= n2 & n2 <= len p by Def9A;
then A4: p.(n1-1)= (XFS2FS p).n1 & p.(n2-1)= (XFS2FS p).n2
by Def9A;
A5: n1-'1+1 = n1 & n2-'1+1 = n2 by A3, XREAL_1:235;
then n1-'1 in dom p & n2-'1 in dom p by A1, Th14;
hence x1 = x2 by A2, A4, A5, FUNCT_1:def 4;
end;
hence thesis;
end;
end;
theorem Th15:
for D being set, p being FinSequence of D holds rng p = rng FS2XFS p
proof
let D be set, p be FinSequence of D;
for y being object
holds y in rng FS2XFS p iff ex x being object st x in dom p & p.x = y
proof
let y be object;
thus y in rng FS2XFS p implies ex x being object st x in dom p & p.x = y
proof
assume y in rng FS2XFS p;
then consider n being object such that
A1: n in dom FS2XFS p & (FS2XFS p).n = y by FUNCT_1:def 3;
reconsider n as Nat by A1;
take n+1;
thus n+1 in dom p by A1, Th13;
n < len FS2XFS p by A1, Lm1;
then n < len p by Def8;
hence p.(n+1) = y by A1, Def8;
end;
given x being object such that
A2: x in dom p & p.x = y;
reconsider n1 = x as Nat by A2;
A3: 1 <= n1 & n1 <= len p by A2, FINSEQ_3:25;
then reconsider n = n1-1 as Nat by Th0;
n < len p - 0 by A3, XREAL_1:15;
then A4: p.(n+1) = (FS2XFS p).n by Def8;
n+1 in dom p by A2;
then n in dom FS2XFS p by Th13;
hence thesis by A2, A4, FUNCT_1:3;
end;
hence thesis by FUNCT_1:def 3;
end;
:: generalizes BALLOT_1:2 to empty D
theorem Th97:
for D being set, p being XFinSequence of D holds rng p = rng XFS2FS p
proof
let D be set, p be XFinSequence of D;
thus rng p = rng FS2XFS XFS2FS p
.= rng XFS2FS p by Th15;
end;
registration
let D be set, p be empty XFinSequence of D;
cluster XFS2FS p -> empty;
coherence
proof
len p = {};
then len XFS2FS p = {} by Def9A;
hence thesis;
end;
end;
registration
let D be set, p be empty FinSequence of D;
cluster FS2XFS p -> empty;
coherence
proof
len p = {};
then len FS2XFS p = {} by Def8;
hence thesis;
end;
end;
:: from COUNTERS, 14.11.2024
theorem
for x, y being object holds
dom <% x, y %> = {0,1} & rng <% x, y %> = {x,y}
proof
let x,y be object;
thus A1: dom <% x, y %> = {0,1} by Th35, CARD_1:50;
now
let b be object;
hereby
assume b in rng <% x, y %>;
then consider a being object such that
A2: a in dom <% x, y %> & <% x, y %>.a = b by FUNCT_1:def 3;
per cases by A1, A2, TARSKI:def 2;
suppose a = 0;
hence b in {x,y} by A2, TARSKI:def 2;
end;
suppose a = 1;
hence b in {x,y} by A2, TARSKI:def 2;
end;
end;
assume b in {x, y};
then per cases by TARSKI:def 2;
suppose b = x;
then 0 in dom <% x, y %> & <% x, y %>.0 = b
by A1, TARSKI:def 2;
hence b in rng <% x, y %> by FUNCT_1:3;
end;
suppose b = y;
then 1 in dom <% x, y %> & <% x, y %>.1 = b
by A1, TARSKI:def 2;
hence b in rng <% x, y %> by FUNCT_1:3;
end;
end;
hence thesis by TARSKI:2;
end;
theorem
for x,y,z being object holds
dom <% x,y,z %> = {0,1,2} & rng <% x,y,z %> = {x,y,z}
proof
let x,y,z be object;
thus A1: dom <% x, y, z %> = {0,1,2} by CARD_1:51, Th36;
now
let b be object;
hereby
assume b in rng <% x, y, z %>;
then consider a being object such that
A2: a in dom <% x, y, z %> & <% x, y, z %>.a = b by FUNCT_1:def 3;
per cases by A1, A2, ENUMSET1:def 1;
suppose a = 0;
hence b in {x,y,z} by A2, ENUMSET1:def 1;
end;
suppose a = 1;
hence b in {x,y,z} by A2, ENUMSET1:def 1;
end;
suppose a = 2;
hence b in {x,y,z} by A2, ENUMSET1:def 1;
end;
end;
assume b in {x, y, z};
then per cases by ENUMSET1:def 1;
suppose b = x;
then 0 in dom <% x, y, z %> & <% x, y, z %>.0 = b
by A1, ENUMSET1:def 1;
hence b in rng <% x, y, z %> by FUNCT_1:3;
end;
suppose b = y;
then 1 in dom <% x, y, z %> & <% x, y, z %>.1 = b
by A1, ENUMSET1:def 1;
hence b in rng <% x, y, z %> by FUNCT_1:3;
end;
suppose b = z;
then 2 in dom <% x, y, z %> & <% x, y, z %>.2 = b
by A1, ENUMSET1:def 1;
hence b in rng <% x, y, z %> by FUNCT_1:3;
end;
end;
hence thesis by TARSKI:2;
end;
registration let n be Nat;
reduce <%0%>.n to 0;
reducibility;
end;
registration let D be non empty set;
cluster empty-yielding for XFinSequence of D;
existence
proof
take f = <%>D;
thus thesis;
end;
end;
registration let D be non empty set;
let f be empty-yielding XFinSequence of D;
cluster XFS2FS f -> empty-yielding;
coherence
proof
rng XFS2FS f = rng f by Th97;
hence thesis by RELAT_1:def 15;
end;
end;
registration
let n be Nat, f be n-element XFinSequence, c be Complex;
reduce (f^<%c%>).n to c;
reducibility
proof
dom f = n by CARD_1:def 7;
hence thesis by Th33;
end;
end;
registration
let D be non empty set;
let n be Nat;
cluster n-element D-valued for XFinSequence of D;
existence
proof
consider p be XFinSequence of D such that
A1: len p = n by Th12;
p is n-element by A1;
hence thesis;
end;
end;