:: Zero Based Finite Sequences :: by Tetsuya Tsunetou , Grzegorz Bancerek and Yatsuka Nakamura :: :: Received September 28, 2001 :: Copyright (c) 2001-2017 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; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, 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; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, ORDINAL1, XBOOLE_0, RELAT_1, PARTFUN1, CARD_1, FUNCT_1; equalities ORDINAL1, FUNCOP_1, VALUED_1, NAT_1, CARD_1; expansions TARSKI, ORDINAL1, XBOOLE_0, 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; 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 ::\$CT 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; n <= n + 1 by NAT_1:11; then Segm n c= Segm(n+1) by NAT_1:39; 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 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; end; definition let p; redefine func len p -> Element of NAT; coherence proof card p = card p; hence thesis; end; end; definition let p; redefine func dom p -> Subset of NAT; coherence proof {i where i is Nat:iNat,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: iNat,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 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 by FUNCOP_1:13; 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 :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; then n in Segm len q by Lm1; hence thesis by A2; 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; k < len q by A1,Lm1; then len p + k < len p + len q by XREAL_1:8; 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 Th22: 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 Th23: 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: rng(p^q) = rng p \/ rng q proof now let x be object; assume x in rng(p^q); then consider y being object such that A1: y in dom(p^q) and A2: x=(p^q).y by FUNCT_1:def 3; reconsider k=y as Element of NAT by A1; y in Segm(len p + len q) by A1,Def3; then A3: k < len p + len q by NAT_1:44; A4: now assume A5: len p <= k; then consider m being Nat such that A6: len p + m = k by NAT_1:10; m + len p - len p < len p + len q - len p by A3,A6,XREAL_1:14; then A7: m in Segm len q by Lm1; q.(k-len p) = x by A2,A3,A5,Th16; hence x in rng q by A6,A7,FUNCT_1:3; end; now assume not len p <= k; then A8: k in dom p by Lm1; then p.k = x by A2,Def3; hence x in rng p by A8,FUNCT_1:3; end; hence x in rng p \/ rng q by A4,XBOOLE_0:def 3; end; then A9: rng(p^q) c= rng p \/ rng q; rng p c= rng(p^q) & rng q c= rng(p^q) by Th22,Th23; then (rng p \/ rng q) c= rng(p^q) by XBOOLE_1:8; hence thesis by A9; end; 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^q) .= 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; then rng(p^q) c= D by A1,XBOOLE_1:8; hence thesis; 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 :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:13,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 by Def4; 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; dom p = {0} by A1,Def4,CARD_1:49; then rng p = {p.0} by FUNCT_1:4; 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; A2: 0 in {0} by TARSKI:def 1; then A3: 0 in dom <%y%> by Def4,CARD_1:49; 0 in dom <%x%> by A2,Def4,CARD_1:49; 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 k in dom <%y%>; then A8: k in {0} by Def4,CARD_1:49; 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 in {0} by Def4,CARD_1:49; 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 A1: 0 in {0} by TARSKI:def 1; then A2: 0 in dom <%x%> by Def4,CARD_1:49; A3: 0 in dom <%z%> by A1,Def4,CARD_1:49; 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 k in {0} by Def4,CARD_1:49; 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 for XFinSequence; existence proof take n --> 0; thus card(n --> 0)= n by FUNCOP_1:13; end; end; registration let n be Nat; cluster -> total for n-element n-defined XFinSequence; coherence proof let s be n-element XFinSequence; card s = n by CARD_1:def 7; hence dom s = n; 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; then P[w] by A3,A7,A9; hence P[p] by A10,A2; 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; :: 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 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).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^q); then n>=len p+len q by Def3; then k >= len q by A1,XREAL_1:8; then Segm len q c= Segm k by NAT_1:39; 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; 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 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; k<=k+1 by NAT_1:11; then Segm k c= Segm(k+1) by NAT_1:39; 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; p = {} by A14; then A16: p = {} ^ {}; 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; nx FinSequence of D means 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); 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 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-'1r) 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 be Nat st 1<=i & i<= len q holds it.i=q.i)& for j being Nat st len q 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; 0 < len <%x%>; then 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; i-1>=0 by A7,XREAL_1:48; then A9: i-'1=i-1 by XREAL_0:def 2; i)+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) by FUNCOP_1:13; A16: for j being Nat st len q ^ (FS2XFS q)) =len (<%x%>) + len (FS2XFS q) by Def3 .=1+len q by A4,Def8; len q0 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 j-(1+len q)>=0 by XREAL_1:48; then A23: j-'(1+len q)=j-(1+len q) by XREAL_0:def 2; 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 by A24,FUNCOP_1:7; 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 .=1+len q+(n-'len q-'1) by FUNCOP_1:13 .=(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 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 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; :: following, 2010.01.11, A.T. 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; j < i by NAT_1:44,A3; hence y in dom F by A1,A2; 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; LastLoc F in dom F by VALUED_1:30; then k < card F by A1,Lm1; 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 k+1 in dom F by Lm1; then A3: k+1 <= k by A1,VALUED_1:32; 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; R = LastLoc F .--> (F.LastLoc F) by FUNCT_4:82; then A3: dom R = {LastLoc F} by FUNCOP_1:13; 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; l+card I < card I by A2,A4,Lm1; hence contradiction by NAT_1:11; 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; then m+1 >= card p by A1,XXREAL_0:2; hence thesis by Lm1; 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; 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; 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%> = len<%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; then l+(n+card I) < n+card I by A4,A6,XREAL_1:6; hence contradiction by NAT_1:11; 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; A1: len p = n by FUNCOP_1:13; A2: dom q = n+1 by FUNCOP_1:13 .= len p + len <%e%> by A1,Th31; A3: for k st k in dom p holds q.k=p.k proof let k; assume A4: k in dom p; Segm n c= Segm(n+1) by NAT_1:63; then p c= q by FUNCT_4:4; 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%>; dom<%e%> = {0} by Th30, CARD_1:49; then A6: k = 0 by A5,TARSKI:def 1; len p < n+1 by A1,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 in { 0 } by A2, Def4, CARD_1:49; then m = 0 by 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; then rng p = {y} by A3,ZFMISC_1:33; hence <%x%> +~ (x,y) = <%y%> by A1,Th30; 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;