:: Zero Based Finite Sequences
:: by Tetsuya Tsunetou , Grzegorz Bancerek and Yatsuka Nakamura
::
:: Copyright (c) 2001-2018 Association of Mizar Users

theorem :: AFINSQ_1:1
canceled;

:: Extended Segments of Natural Numbers
::$CT theorem Th1: :: AFINSQ_1:2 for n being Nat holds (Segm n) \/ {n} = Segm (n + 1) proof end; theorem Th2: :: AFINSQ_1:3 for n being Nat holds Seg n c= Segm (n + 1) proof end; theorem :: AFINSQ_1:4 for n being Nat holds n + 1 = \/ (Seg n) proof end; :: Finite ExFinSequences theorem :: AFINSQ_1:5 for r being Function holds ( ( r is finite & r is Sequence-like ) iff ex n being Nat st dom r = n ) by FINSET_1:10; definition end; registration let p be XFinSequence; coherence dom p is natural ; end; notation let p be XFinSequence; synonym len p for card p; end; registration let p be XFinSequence; identify len p with dom p; compatibility len p = dom p proof end; end; definition let p be XFinSequence; :: original: len redefine func len p -> Element of NAT ; coherence len p is Element of NAT proof end; end; definition let p be XFinSequence; :: original: dom redefine func dom p -> Subset of NAT; coherence dom p is Subset of NAT proof end; end; theorem :: AFINSQ_1:6 for f being Function st ex k being Nat st dom f c= k holds ex p being XFinSequence st f c= p proof end; scheme :: AFINSQ_1:sch 1 XSeqEx{ F1() -> Nat, P1[ object , object ] } : ex p being XFinSequence st ( dom p = F1() & ( for k being Nat st k in F1() holds P1[k,p . k] ) ) provided A1: for k being Nat st k in F1() holds ex x being object st P1[k,x] proof end; scheme :: AFINSQ_1:sch 2 XSeqLambda{ F1() -> Nat, F2( object ) -> object } : ex p being XFinSequence st ( len p = F1() & ( for k being Nat st k in F1() holds p . k = F2(k) ) ) proof end; theorem :: AFINSQ_1:7 for z being object for p being XFinSequence st z in p holds ex k being Nat st ( k in dom p & z = [k,(p . k)] ) proof end; theorem :: AFINSQ_1:8 for p, q being XFinSequence st dom p = dom q & ( for k being Nat st k in dom p holds p . k = q . k ) holds p = q ; Lm1: for k being Nat for p being XFinSequence holds ( k < len p iff k in dom p ) proof end; theorem Th8: :: AFINSQ_1:9 for p, q being XFinSequence st len p = len q & ( for k being Nat st k < len p holds p . k = q . k ) holds p = q proof end; registration let p be XFinSequence; let n be Nat; cluster p | n -> finite ; coherence p | n is finite ; end; theorem :: AFINSQ_1:10 for f being Function for p being XFinSequence st rng p c= dom f holds f * p is XFinSequence proof end; theorem Th10: :: AFINSQ_1:11 for k being Nat for p being XFinSequence st k < len p holds dom (p | k) = k proof end; :: XFinSequences of D registration let D be set ; existence ex b1 being Sequence of D st b1 is finite proof end; end; definition let D be set ; mode XFinSequence of D is finite Sequence of D; end; theorem Th11: :: AFINSQ_1:12 for D being set for f being XFinSequence of D holds f is PartFunc of NAT,D proof end; registration coherence for b1 being Function st b1 is empty holds b1 is Sequence-like ; end; registration let k be Nat; let a be object ; cluster K156((Segm k),a) -> Sequence-like finite ; coherence ( (Segm k) --> a is finite & (Segm k) --> a is Sequence-like ) ; end; theorem :: AFINSQ_1:13 canceled; ::$CT
theorem Th12: :: AFINSQ_1:14
for k being Nat
for D being non empty set ex p being XFinSequence of D st len p = k
proof end;

:: ::
:: The Empty XFinSequence ::
:: ::
theorem :: AFINSQ_1:15
for p being XFinSequence holds
( len p = 0 iff p = {} ) ;

theorem Th14: :: AFINSQ_1:16
for D being set holds {} is XFinSequence of D
proof end;

registration
let D be set ;
existence
ex b1 being XFinSequence of D st b1 is empty
proof end;
end;

registration
let D be non empty set ;
existence
not for b1 being XFinSequence of D holds b1 is empty
proof end;
end;

definition
let x be object ;
func <%x%> -> set equals :: AFINSQ_1:def 1
0 .--> x;
coherence
0 .--> x is set
;
end;

:: deftheorem defines <% AFINSQ_1:def 1 :
for x being object holds <%x%> = 0 .--> x;

registration
let x be object ;
cluster <%x%> -> non empty ;
coherence
not <%x%> is empty
;
end;

definition
let D be set ;
func <%> D -> XFinSequence of D equals :: AFINSQ_1:def 2
{} ;
coherence
{} is XFinSequence of D
by Th14;
end;

:: deftheorem defines <%> AFINSQ_1:def 2 :
for D being set holds <%> D = {} ;

registration
let D be set ;
cluster <%> D -> empty ;
coherence
<%> D is empty
;
end;

definition
let p, q be XFinSequence;
redefine func p ^ q means :Def3: :: AFINSQ_1:def 3
( dom it = (len p) + (len q) & ( for k being Nat st k in dom p holds
it . k = p . k ) & ( for k being Nat st k in dom q holds
it . ((len p) + k) = q . k ) );
compatibility
for b1 being set holds
( b1 = p ^ q iff ( dom b1 = (len p) + (len q) & ( for k being Nat st k in dom p holds
b1 . k = p . k ) & ( for k being Nat st k in dom q holds
b1 . ((len p) + k) = q . k ) ) )
proof end;
end;

:: deftheorem Def3 defines ^ AFINSQ_1:def 3 :
for p, q being XFinSequence
for b3 being set holds
( b3 = p ^ q iff ( dom b3 = (len p) + (len q) & ( for k being Nat st k in dom p holds
b3 . k = p . k ) & ( for k being Nat st k in dom q holds
b3 . ((len p) + k) = q . k ) ) );

registration
let p, q be XFinSequence;
cluster p ^ q -> finite ;
coherence
p ^ q is finite
proof end;
end;

theorem :: AFINSQ_1:17
for p, q being XFinSequence holds len (p ^ q) = (len p) + (len q) by Def3;

theorem Th16: :: AFINSQ_1:18
for k being Nat
for p, q being XFinSequence st len p <= k & k < (len p) + (len q) holds
(p ^ q) . k = q . (k - (len p))
proof end;

theorem Th17: :: AFINSQ_1:19
for k being Nat
for p, q being XFinSequence st len p <= k & k < len (p ^ q) holds
(p ^ q) . k = q . (k - (len p))
proof end;

theorem Th18: :: AFINSQ_1:20
for k being Nat
for p, q being XFinSequence holds
( not k in dom (p ^ q) or k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
proof end;

theorem Th19: :: AFINSQ_1:21
for p, q being Sequence holds dom p c= dom (p ^ q)
proof end;

theorem Th20: :: AFINSQ_1:22
for x being object
for p, q being XFinSequence st x in dom q holds
ex k being Nat st
( k = x & (len p) + k in dom (p ^ q) )
proof end;

theorem Th21: :: AFINSQ_1:23
for k being Nat
for p, q being XFinSequence st k in dom q holds
(len p) + k in dom (p ^ q)
proof end;

theorem Th22: :: AFINSQ_1:24
for p, q being XFinSequence holds rng p c= rng (p ^ q)
proof end;

theorem Th23: :: AFINSQ_1:25
for p, q being XFinSequence holds rng q c= rng (p ^ q)
proof end;

theorem Th24: :: AFINSQ_1:26
for p, q being XFinSequence holds rng (p ^ q) = (rng p) \/ (rng q)
proof end;

theorem Th25: :: AFINSQ_1:27
for p, q, r being XFinSequence holds (p ^ q) ^ r = p ^ (q ^ r)
proof end;

theorem Th26: :: AFINSQ_1:28
for p, q, r being XFinSequence st ( p ^ r = q ^ r or r ^ p = r ^ q ) holds
p = q
proof end;

registration
let p be XFinSequence;
reduce p ^ {} to p;
reducibility
p ^ {} = p
proof end;
reduce {} ^ p to p;
reducibility
{} ^ p = p
proof end;
end;

theorem :: AFINSQ_1:29
canceled;

::$CT theorem Th27: :: AFINSQ_1:30 for p, q being XFinSequence st p ^ q = {} holds ( p = {} & q = {} ) proof end; registration let D be set ; let p, q be XFinSequence of D; cluster p ^ q -> D -valued ; coherence p ^ q is D -valued proof end; end; Lm2: for x, y being object for x1, y1 being set st [x,y] in {[x1,y1]} holds ( x = x1 & y = y1 ) proof end; definition let x be object ; :: original: <% redefine func <%x%> -> Function means :Def4: :: AFINSQ_1:def 4 ( dom it = 1 & it . 0 = x ); coherence <%x%> is Function ; compatibility for b1 being Function holds ( b1 = <%x%> iff ( dom b1 = 1 & b1 . 0 = x ) ) proof end; end; :: deftheorem Def4 defines <% AFINSQ_1:def 4 : for x being object for b2 being Function holds ( b2 = <%x%> iff ( dom b2 = 1 & b2 . 0 = x ) ); registration let x be object ; coherence ( <%x%> is Function-like & <%x%> is Relation-like ) ; end; registration let x be object ; coherence ( <%x%> is finite & <%x%> is Sequence-like ) by Def4; end; theorem :: AFINSQ_1:31 for p, q being XFinSequence for D being set st p ^ q is XFinSequence of D holds ( p is XFinSequence of D & q is XFinSequence of D ) proof end; definition let x, y be object ; func <%x,y%> -> set equals :: AFINSQ_1:def 5 <%x%> ^ <%y%>; correctness coherence <%x%> ^ <%y%> is set ; ; let z be object ; func <%x,y,z%> -> set equals :: AFINSQ_1:def 6 () ^ <%z%>; correctness coherence () ^ <%z%> is set ; ; end; :: deftheorem defines <% AFINSQ_1:def 5 : for x, y being object holds <%x,y%> = <%x%> ^ <%y%>; :: deftheorem defines <% AFINSQ_1:def 6 : for x, y, z being object holds <%x,y,z%> = () ^ <%z%>; registration let x, y be object ; coherence ( <%x,y%> is Function-like & <%x,y%> is Relation-like ) ; let z be object ; coherence ( <%x,y,z%> is Function-like & <%x,y,z%> is Relation-like ) ; end; registration let x, y be object ; coherence ( <%x,y%> is finite & <%x,y%> is Sequence-like ) ; let z be object ; cluster <%x,y,z%> -> Sequence-like finite ; coherence ( <%x,y,z%> is finite & <%x,y,z%> is Sequence-like ) ; end; theorem :: AFINSQ_1:32 for x being object holds <%x%> = {[0,x]} by FUNCT_4:82; theorem Th30: :: AFINSQ_1:33 for x being object for p being XFinSequence holds ( p = <%x%> iff ( dom p = Segm 1 & rng p = {x} ) ) proof end; theorem Th31: :: AFINSQ_1:34 for x being object for p being XFinSequence holds ( p = <%x%> iff ( len p = 1 & p . 0 = x ) ) by Def4; registration let x be object ; reduce <%x%> . 0 to x; reducibility <%x%> . 0 = x by Th31; end; theorem Th32: :: AFINSQ_1:35 for x being object for p being XFinSequence holds (<%x%> ^ p) . 0 = x proof end; theorem Th33: :: AFINSQ_1:36 for x being object for p being XFinSequence holds (p ^ <%x%>) . (len p) = x proof end; theorem :: AFINSQ_1:37 for x, y, z being object holds ( <%x,y,z%> = <%x%> ^ <%y,z%> & <%x,y,z%> = <%x,y%> ^ <%z%> ) by Th25; theorem Th35: :: AFINSQ_1:38 for x, y being object for p being XFinSequence holds ( p = <%x,y%> iff ( len p = 2 & p . 0 = x & p . 1 = y ) ) proof end; registration let x, y be object ; reduce <%x,y%> . 0 to x; reducibility <%x,y%> . 0 = x by Th35; reduce <%x,y%> . 1 to y; reducibility <%x,y%> . 1 = y by Th35; end; theorem Th36: :: AFINSQ_1:39 for x, y, z being object for p being XFinSequence holds ( p = <%x,y,z%> iff ( len p = 3 & p . 0 = x & p . 1 = y & p . 2 = z ) ) proof end; registration let x, y, z be object ; reduce <%x,y,z%> . 0 to x; reducibility <%x,y,z%> . 0 = x by Th36; reduce <%x,y,z%> . 1 to y; reducibility <%x,y,z%> . 1 = y by Th36; reduce <%x,y,z%> . 2 to z; reducibility <%x,y,z%> . 2 = z by Th36; end; registration let x be object ; cluster (x) -> 1 -element ; coherence <%x%> is 1 -element by Th30; let y be object ; cluster <%x,y%> -> 2 -element ; coherence <%x,y%> is 2 -element by Th35; let z be object ; cluster <%x,y,z%> -> 3 -element ; coherence <%x,y,z%> is 3 -element by Th36; end; registration let n be Nat; coherence for b1 being XFinSequence st b1 is n -element holds b1 is n -defined ; end; registration let n be Nat; let x be object ; cluster K156(n,x) -> Sequence-like finite ; coherence ( n --> x is finite & n --> x is Sequence-like ) ; end; registration let n be Nat; existence ex b1 being XFinSequence st b1 is n -element proof end; end; registration let n be Nat; coherence for b1 being n -defined n -element XFinSequence holds b1 is total proof end; end; theorem Th37: :: AFINSQ_1:40 for p being XFinSequence st p <> {} holds ex q being XFinSequence ex x being object st p = q ^ <%x%> proof end; registration let D be non empty set ; let d1 be Element of D; cluster (d1) -> D -valued ; coherence <%d1%> is D -valued ; let d2 be Element of D; cluster <%d1,d2%> -> D -valued ; coherence <%d1,d2%> is D -valued ; let d3 be Element of D; cluster <%d1,d2,d3%> -> D -valued ; coherence <%d1,d2,d3%> is D -valued ; end; :: Scheme of induction for extended finite sequences scheme :: AFINSQ_1:sch 3 IndXSeq{ P1[ XFinSequence] } : for p being XFinSequence holds P1[p] provided A1: P1[ {} ] and A2: for p being XFinSequence for x being object st P1[p] holds P1[p ^ <%x%>] proof end; theorem :: AFINSQ_1:41 for p, q, r, s being XFinSequence st p ^ q = r ^ s & len p <= len r holds ex t being XFinSequence st p ^ t = r proof end; definition let D be set ; func D ^omega -> set means :Def7: :: AFINSQ_1:def 7 for x being object holds ( x in it iff x is XFinSequence of D ); existence ex b1 being set st for x being object holds ( x in b1 iff x is XFinSequence of D ) proof end; uniqueness for b1, b2 being set st ( for x being object holds ( x in b1 iff x is XFinSequence of D ) ) & ( for x being object holds ( x in b2 iff x is XFinSequence of D ) ) holds b1 = b2 proof end; end; :: deftheorem Def7 defines ^omega AFINSQ_1:def 7 : for D, b2 being set holds ( b2 = D ^omega iff for x being object holds ( x in b2 iff x is XFinSequence of D ) ); registration let D be set ; cluster D ^omega -> non empty ; coherence not D ^omega is empty proof end; end; theorem :: AFINSQ_1:42 for x being object for D being set holds ( x in D ^omega iff x is XFinSequence of D ) by Def7; theorem :: AFINSQ_1:43 for D being set holds {} in D ^omega proof end; scheme :: AFINSQ_1:sch 4 SepXSeq{ F1() -> non empty set , P1[ XFinSequence] } : ex X being set st for x being object holds ( x in X iff ex p being XFinSequence st ( p in F1() ^omega & P1[p] & x = p ) ) proof 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) -> Sequence-like finite ; coherence ( p +* (i,x) is finite & p +* (i,x) is Sequence-like ) proof end; end; theorem :: AFINSQ_1:44 for p being XFinSequence for i being Element of NAT for 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 end; registration let D be non empty set ; let p be XFinSequence of D; let i be Element of NAT ; let a be Element of D; cluster Replace (p,i,a) -> D -valued ; coherence Replace (p,i,a) is D -valued proof end; end; :: missing, 2008.02.02, A.K. registration coherence for b1 being XFinSequence of REAL holds b1 is real-valued proof end; end; registration coherence for b1 being XFinSequence of NAT holds b1 is natural-valued proof end; end; :: 2009.0929, A.T. theorem Th42: :: AFINSQ_1:45 for p being XFinSequence 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 end; theorem Th43: :: AFINSQ_1:46 for p being XFinSequence 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 end; theorem Th44: :: AFINSQ_1:47 for p being XFinSequence 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 end; theorem Th45: :: AFINSQ_1:48 for p being XFinSequence 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 end; theorem Th46: :: AFINSQ_1:49 for p being XFinSequence 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 end; theorem :: AFINSQ_1:50 for p being XFinSequence 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 end; :: K.P. 12.2009 theorem :: AFINSQ_1:51 for n being Nat for p, q being XFinSequence st n < len p holds (p ^ q) . n = p . n proof end; theorem :: AFINSQ_1:52 for n being Nat for p being XFinSequence st len p <= n holds p | n = p proof end; theorem Th50: :: AFINSQ_1:53 for k, n being Nat for p being XFinSequence st n <= len p & k in n holds ( (p | n) . k = p . k & k in dom p ) proof end; theorem Th51: :: AFINSQ_1:54 for n being Nat for p being XFinSequence st n <= len p holds len (p | n) = n proof end; theorem :: AFINSQ_1:55 for n being Nat for p being XFinSequence holds len (p | n) <= n proof end; theorem Th53: :: AFINSQ_1:56 for n being Nat for p being XFinSequence st len p = n + 1 holds p = (p | n) ^ <%(p . n)%> proof end; theorem Th54: :: AFINSQ_1:57 for p, q being XFinSequence holds (p ^ q) | (dom p) = p proof end; theorem :: AFINSQ_1:58 for n being Nat for p, q being XFinSequence st n <= dom p holds (p ^ q) | n = p | n proof end; theorem :: AFINSQ_1:59 for k, n being Nat for p, q being XFinSequence st n = (dom p) + k holds (p ^ q) | n = p ^ (q | k) proof end; theorem :: AFINSQ_1:60 for n being Nat for p being XFinSequence ex q being XFinSequence st p = (p | n) ^ q proof end; theorem :: AFINSQ_1:61 for k, n being Nat for p being XFinSequence st len p = n + k holds ex q1, q2 being XFinSequence st ( len q1 = n & len q2 = k & p = q1 ^ q2 ) proof end; theorem :: AFINSQ_1:62 for x, y being object for p, q being XFinSequence st <%x%> ^ p = <%y%> ^ q holds ( x = y & p = q ) proof end; definition let D be set ; let q be FinSequence of D; func FS2XFS q -> XFinSequence of D means :Def8: :: AFINSQ_1:def 8 ( len it = len q & ( for i being Nat st i < len q holds q . (i + 1) = it . i ) ); existence ex b1 being XFinSequence of D st ( len b1 = len q & ( for i being Nat st i < len q holds q . (i + 1) = b1 . i ) ) proof end; uniqueness for b1, b2 being XFinSequence of D st len b1 = len q & ( for i being Nat st i < len q holds q . (i + 1) = b1 . i ) & len b2 = len q & ( for i being Nat st i < len q holds q . (i + 1) = b2 . i ) holds b1 = b2 proof end; end; :: deftheorem Def8 defines FS2XFS AFINSQ_1:def 8 : for D being set for q being FinSequence of D for b3 being XFinSequence of D holds ( b3 = FS2XFS q iff ( len b3 = len q & ( for i being Nat st i < len q holds q . (i + 1) = b3 . i ) ) ); definition let D be set ; let q be XFinSequence of D; func XFS2FS q -> FinSequence of D means :: AFINSQ_1:def 9 ( len it = len q & ( for i being Nat st 1 <= i & i <= len q holds q . (i -' 1) = it . i ) ); existence ex b1 being FinSequence of D st ( len b1 = len q & ( for i being Nat st 1 <= i & i <= len q holds q . (i -' 1) = b1 . i ) ) proof end; uniqueness for b1, b2 being FinSequence of D st len b1 = len q & ( for i being Nat st 1 <= i & i <= len q holds q . (i -' 1) = b1 . i ) & len b2 = len q & ( for i being Nat st 1 <= i & i <= len q holds q . (i -' 1) = b2 . i ) holds b1 = b2 proof end; end; :: deftheorem defines XFS2FS AFINSQ_1:def 9 : for D being set for q being XFinSequence of D for b3 being FinSequence of D holds ( b3 = XFS2FS q iff ( len b3 = len q & ( for i being Nat st 1 <= i & i <= len q holds q . (i -' 1) = b3 . i ) ) ); theorem :: AFINSQ_1:63 for D being set for n being Nat for 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; let n be Nat; assume that A1: n > len q and A2: NAT c= D ; func FS2XFS* (q,n) -> non empty XFinSequence of D means :: AFINSQ_1:def 10 ( 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 ex b1 being non empty XFinSequence of D st ( len q = b1 . 0 & len b1 = n & ( for i being Nat st 1 <= i & i <= len q holds b1 . i = q . i ) & ( for j being Nat st len q < j & j < n holds b1 . j = 0 ) ) proof end; uniqueness for b1, b2 being non empty XFinSequence of D st len q = b1 . 0 & len b1 = n & ( for i being Nat st 1 <= i & i <= len q holds b1 . i = q . i ) & ( for j being Nat st len q < j & j < n holds b1 . j = 0 ) & len q = b2 . 0 & len b2 = n & ( for i being Nat st 1 <= i & i <= len q holds b2 . i = q . i ) & ( for j being Nat st len q < j & j < n holds b2 . j = 0 ) holds b1 = b2 proof end; end; :: deftheorem defines FS2XFS* AFINSQ_1:def 10 : for D being non empty set for q being FinSequence of D for n being Nat st n > len q & NAT c= D holds for b4 being non empty XFinSequence of D holds ( b4 = FS2XFS* (q,n) iff ( len q = b4 . 0 & len b4 = n & ( for i being Nat st 1 <= i & i <= len q holds b4 . i = q . i ) & ( for j being Nat st len q < j & j < n holds b4 . j = 0 ) ) ); 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: :: AFINSQ_1:def 11 for m being Nat st m = p . 0 holds ( len it = m & ( for i being Nat st 1 <= i & i <= m holds it . i = p . i ) ); existence ex b1 being FinSequence of D st for m being Nat st m = p . 0 holds ( len b1 = m & ( for i being Nat st 1 <= i & i <= m holds b1 . i = p . i ) ) proof end; uniqueness for b1, b2 being FinSequence of D st ( for m being Nat st m = p . 0 holds ( len b1 = m & ( for i being Nat st 1 <= i & i <= m holds b1 . i = p . i ) ) ) & ( for m being Nat st m = p . 0 holds ( len b2 = m & ( for i being Nat st 1 <= i & i <= m holds b2 . i = p . i ) ) ) holds b1 = b2 proof end; end; :: deftheorem Def11 defines XFS2FS* AFINSQ_1:def 11 : for D being non empty set for p being XFinSequence of D st p . 0 is Nat & p . 0 in len p holds for b3 being FinSequence of D holds ( b3 = XFS2FS* p iff for m being Nat st m = p . 0 holds ( len b3 = m & ( for i being Nat st 1 <= i & i <= m holds b3 . i = p . i ) ) ); theorem :: AFINSQ_1:64 for D being non empty set for p being XFinSequence of D st p . 0 = 0 & 0 < len p holds XFS2FS* p = {} proof end; :: from EXTPRO_1, 2010.01.11, A.T. definition let F be Function; attr F is initial means :Def12: :: AFINSQ_1:def 12 for m, n being Nat st n in dom F & m < n holds m in dom F; end; :: deftheorem Def12 defines initial AFINSQ_1:def 12 : for F being Function holds ( F is initial iff for m, n being Nat st n in dom F & m < n holds m in dom F ); registration coherence for b1 being Function st b1 is empty holds b1 is initial ; end; registration coherence for b1 being XFinSequence holds b1 is initial proof end; end; :: following, 2010.01.11, A.T. registration coherence for b1 being XFinSequence holds b1 is NAT -defined proof end; end; theorem Th62: :: AFINSQ_1:65 for F being NAT -defined non empty initial Function holds 0 in dom F proof end; registration coherence for b1 being Function st b1 is initial & b1 is finite & b1 is NAT -defined holds b1 is Sequence-like proof end; end; theorem :: AFINSQ_1:66 for F being NAT -defined finite initial 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 :: AFINSQ_1:67 for F being NAT -defined initial Function for G being NAT -defined Function st dom F = dom G holds G is initial by Def12; theorem :: AFINSQ_1:68 for F being NAT -defined finite initial Function holds dom F = { k where k is Element of NAT : k < card F } proof end; theorem :: AFINSQ_1:69 for F being non empty XFinSequence for G being NAT -defined non empty finite Function st F c= G & LastLoc F = LastLoc G holds F = G proof end; theorem Th67: :: AFINSQ_1:70 for F being non empty XFinSequence holds LastLoc F = (card F) -' 1 proof end; theorem :: AFINSQ_1:71 for F being NAT -defined non empty finite initial Function holds FirstLoc F = 0 by ; registration let F be NAT -defined non empty finite initial Function; coherence proof end; end; theorem :: AFINSQ_1:72 for I being NAT -defined finite initial Function for J being Function holds dom I misses dom (Shift (J,(card I))) proof end; :: from SCMPDS_4, 2010.05.14, A.T. theorem :: AFINSQ_1:73 for p being XFinSequence for m being Nat st not m in dom p holds not m + 1 in dom p proof end; :: from SCM_COMP, 2010.05.16, A.T. registration let D be set ; coherence by Def7; end; registration let D be set ; coherence for b1 being Element of D ^omega holds ( b1 is finite & b1 is Sequence-like ) by Def7; end; definition let D be set ; let f be XFinSequence of D; func Down f -> Element of D ^omega equals :: AFINSQ_1:def 13 f; coherence f is Element of D ^omega by Def7; end; :: deftheorem defines Down AFINSQ_1:def 13 : for D being set for f being XFinSequence of D holds Down f = f; definition let D be set ; let f be XFinSequence of D; let g be Element of D ^omega ; :: original: ^ redefine func f ^ g -> Element of D ^omega ; coherence f ^ g is Element of D ^omega proof end; end; definition let D be set ; let f, g be Element of D ^omega ; :: original: ^ redefine func f ^ g -> Element of D ^omega ; coherence f ^ g is Element of D ^omega proof end; end; :: missing, 2010.05.15, A.T. theorem Th71: :: AFINSQ_1:74 for p, q being XFinSequence holds p c= p ^ q proof end; theorem Th72: :: AFINSQ_1:75 for x being object for p being XFinSequence holds len (p ^ <%x%>) = (len p) + 1 proof end; theorem :: AFINSQ_1:76 for x, y being object holds <%x,y%> = (0,1) --> (x,y) proof end; theorem Th74: :: AFINSQ_1:77 for p, q being XFinSequence holds p ^ q = p +* (Shift (q,(card p))) proof end; theorem :: AFINSQ_1:78 for p, q being XFinSequence holds ( p +* (p ^ q) = p ^ q & (p ^ q) +* p = p ^ q ) by ; theorem Th76: :: AFINSQ_1:79 for n being Nat for I being NAT -defined finite initial Function for J being Function holds dom (Shift (I,n)) misses dom (Shift (J,(n + (card I)))) proof end; theorem Th77: :: AFINSQ_1:80 for p, q being XFinSequence for n being Nat holds Shift (p,n) c= Shift ((p ^ q),n) proof end; theorem Th78: :: AFINSQ_1:81 for p, q being XFinSequence for n being Nat holds Shift (q,(n + (card p))) c= Shift ((p ^ q),n) proof end; theorem :: AFINSQ_1:82 for X being set for p, q being XFinSequence for n being Nat st Shift ((p ^ q),n) c= X holds Shift (p,n) c= X proof end; theorem :: AFINSQ_1:83 for X being set for p, q being XFinSequence for n being Nat st Shift ((p ^ q),n) c= X holds Shift (q,(n + (card p))) c= X proof end; registration let F be NAT -defined non empty finite initial Function; coherence ; end; definition let x1, x2, x3, x4 be object ; func <%x1,x2,x3,x4%> -> set equals :: AFINSQ_1:def 14 ((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>; coherence ((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%> is set ; end; :: deftheorem defines <% AFINSQ_1:def 14 : for x1, x2, x3, x4 being object holds <%x1,x2,x3,x4%> = ((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>; registration let x1, x2, x3, x4 be object ; cluster <%x1,x2,x3,x4%> -> Relation-like Function-like ; coherence ( <%x1,x2,x3,x4%> is Function-like & <%x1,x2,x3,x4%> is Relation-like ) ; end; registration let x1, x2, x3, x4 be object ; cluster <%x1,x2,x3,x4%> -> Sequence-like finite ; coherence ( <%x1,x2,x3,x4%> is finite & <%x1,x2,x3,x4%> is Sequence-like ) ; end; theorem :: AFINSQ_1:84 for x1, x2, x3, x4 being object holds len <%x1,x2,x3,x4%> = 4 proof end; Lm3: for x1, x2, x3, x4 being object holds ( <%x1,x2,x3,x4%> . 1 = x2 & <%x1,x2,x3,x4%> . 2 = x3 & <%x1,x2,x3,x4%> . 3 = x4 ) proof end; registration let x1, x2, x3, x4 be object ; reduce <%x1,x2,x3,x4%> . 0 to x1; reducibility <%x1,x2,x3,x4%> . 0 = x1 proof end; reduce <%x1,x2,x3,x4%> . 1 to x2; reducibility <%x1,x2,x3,x4%> . 1 = x2 by Lm3; reduce <%x1,x2,x3,x4%> . 2 to x3; reducibility <%x1,x2,x3,x4%> . 2 = x3 by Lm3; reduce <%x1,x2,x3,x4%> . 3 to x4; reducibility <%x1,x2,x3,x4%> . 3 = x4 by Lm3; end; theorem :: AFINSQ_1:85 canceled; ::$CT
theorem :: AFINSQ_1:86
for k being Nat
for p being XFinSequence holds
( k < len p iff k in dom p ) by Lm1;

theorem :: AFINSQ_1:87
for n being Nat
for e being object holds (Segm (n + 1)) --> e = ((Segm n) --> e) ^ <%e%>
proof end;

theorem Th84: :: AFINSQ_1:88
for p being XFinSequence
for e being object holds dom (Shift (<%e%>,(card p))) = {(card p)}
proof end;

theorem :: AFINSQ_1:89
for p being XFinSequence
for e being object holds dom (p ^ <%e%>) = (dom p) \/ {(card p)}
proof end;

theorem :: AFINSQ_1:90
for x, y being object holds <%x%> +~ (x,y) = <%y%>
proof end;

theorem :: AFINSQ_1:91
for I being non empty XFinSequence holds LastLoc I = (card I) - 1
proof end;