:: by Tetsuya Tsunetou , Grzegorz Bancerek and Yatsuka Nakamura

::

:: Received September 28, 2001

:: Copyright (c) 2001-2021 Association of Mizar Users

:: Extended Segments of Natural Numbers

:: 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;

( ( r is finite & r is Sequence-like ) iff ex n being Nat st dom r = n ) by FINSET_1:10;

registration
end;

definition

let p be XFinSequence;

:: original: len

redefine func len p -> Element of NAT ;

coherence

len p is Element of NAT

end;
:: original: len

redefine func len p -> Element of NAT ;

coherence

len p is Element of NAT

proof end;

definition

let p be XFinSequence;

:: original: dom

redefine func dom p -> Subset of NAT;

coherence

dom p is Subset of NAT

end;
:: original: dom

redefine func dom p -> Subset of NAT;

coherence

dom p is Subset of NAT

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)] )

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

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

p . k = q . k ) holds

p = q

proof end;

registration
end;

:: XFinSequences of D

registration
end;

registration
end;

registration

let k be Nat;

let a be object ;

coherence

( (Segm k) --> a is finite & (Segm k) --> a is Sequence-like ) ;

end;
let a be object ;

coherence

( (Segm k) --> a is finite & (Segm k) --> a is Sequence-like ) ;

::$CT

:: ::

:: The Empty XFinSequence ::

:: ::

:: The Empty XFinSequence ::

:: ::

registration
end;

registration

let D be non empty set ;

existence

not for b_{1} being XFinSequence of D holds b_{1} is empty

end;
existence

not for b

proof end;

definition
end;

definition

let p, q be XFinSequence;

for b_{1} being set holds

( b_{1} = p ^ q iff ( dom b_{1} = (len p) + (len q) & ( for k being Nat st k in dom p holds

b_{1} . k = p . k ) & ( for k being Nat st k in dom q holds

b_{1} . ((len p) + k) = q . k ) ) )

end;
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 ( 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 ) );

for b

( b

b

b

proof end;

:: deftheorem Def3 defines ^ AFINSQ_1:def 3 :

for p, q being XFinSequence

for b_{3} being set holds

( b_{3} = p ^ q iff ( dom b_{3} = (len p) + (len q) & ( for k being Nat st k in dom p holds

b_{3} . k = p . k ) & ( for k being Nat st k in dom q holds

b_{3} . ((len p) + k) = q . k ) ) );

for p, q being XFinSequence

for b

( b

b

b

registration
end;

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))

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))

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 ) )

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 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) )

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;

registration
end;

::$CT

registration
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 ;

<%x%> is Function ;

compatibility

for b_{1} being Function holds

( b_{1} = <%x%> iff ( dom b_{1} = 1 & b_{1} . 0 = x ) )

end;
:: original: <%

redefine func <%x%> -> Function means :Def4: :: AFINSQ_1:def 4

( dom it = 1 & it . 0 = x );

coherence redefine func <%x%> -> Function means :Def4: :: AFINSQ_1:def 4

( dom it = 1 & it . 0 = x );

<%x%> is Function ;

compatibility

for b

( b

proof end;

:: deftheorem Def4 defines <% AFINSQ_1:def 4 :

for x being object

for b_{2} being Function holds

( b_{2} = <%x%> iff ( dom b_{2} = 1 & b_{2} . 0 = x ) );

for x being object

for b

( b

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 )

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 ;

correctness

coherence

<%x%> ^ <%y%> is set ;

;

let z be object ;

correctness

coherence

(<%x%> ^ <%y%>) ^ <%z%> is set ;

;

end;
correctness

coherence

<%x%> ^ <%y%> is set ;

;

let z be object ;

correctness

coherence

(<%x%> ^ <%y%>) ^ <%z%> is set ;

;

:: deftheorem defines <% AFINSQ_1:def 6 :

for x, y, z being object holds <%x,y,z%> = (<%x%> ^ <%y%>) ^ <%z%>;

for x, y, z being object holds <%x,y,z%> = (<%x%> ^ <%y%>) ^ <%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;
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 ) ;

registration

let x, y be object ;

coherence

( <%x,y%> is finite & <%x,y%> is Sequence-like ) ;

let z be object ;

coherence

( <%x,y,z%> is finite & <%x,y,z%> is Sequence-like ) ;

end;
coherence

( <%x,y%> is finite & <%x,y%> is Sequence-like ) ;

let z be object ;

coherence

( <%x,y,z%> is finite & <%x,y,z%> is Sequence-like ) ;

theorem Th30: :: AFINSQ_1:33

for x being object

for p being XFinSequence holds

( p = <%x%> iff ( dom p = Segm 1 & rng p = {x} ) )

for p being XFinSequence holds

( p = <%x%> iff ( dom p = Segm 1 & rng p = {x} ) )

proof end;

theorem :: AFINSQ_1:37

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 ) )

for p being XFinSequence holds

( p = <%x,y%> iff ( len p = 2 & p . 0 = x & p . 1 = y ) )

proof end;

registration
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 ) )

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 ;

reducibility

<%x,y,z%> . 0 = x by Th36;

reducibility

<%x,y,z%> . 1 = y by Th36;

reducibility

<%x,y,z%> . 2 = z by Th36;

end;
reducibility

<%x,y,z%> . 0 = x by Th36;

reducibility

<%x,y,z%> . 1 = y by Th36;

reducibility

<%x,y,z%> . 2 = z by Th36;

registration

let x be object ;

coherence

<%x%> is 1 -element by Th30;

let y be object ;

coherence

<%x,y%> is 2 -element by Th35;

let z be object ;

coherence

<%x,y,z%> is 3 -element by Th36;

end;
coherence

<%x%> is 1 -element by Th30;

let y be object ;

coherence

<%x,y%> is 2 -element by Th35;

let z be object ;

coherence

<%x,y,z%> is 3 -element by Th36;

registration

let n be Nat;

coherence

for b_{1} being XFinSequence st b_{1} is n -element holds

b_{1} is n -defined
;

end;
coherence

for b

b

registration
end;

registration
end;

registration

let n be Nat;

for b_{1} being n -defined n -element XFinSequence holds b_{1} is total

end;
cluster Relation-like n -defined Sequence-like Function-like finite n -element -> n -defined total n -element for set ;

coherence for b

proof 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%>

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;

coherence

<%d1%> is D -valued ;

let d2 be Element of D;

coherence

<%d1,d2%> is D -valued ;

let d3 be Element of D;

coherence

<%d1,d2,d3%> is D -valued ;

end;
let d1 be Element of D;

coherence

<%d1%> is D -valued ;

let d2 be Element of D;

coherence

<%d1,d2%> is D -valued ;

let d3 be Element of D;

coherence

<%d1,d2,d3%> is D -valued ;

:: Scheme of induction for extended finite sequences

scheme :: AFINSQ_1:sch 3

IndXSeq{ P_{1}[ XFinSequence] } :

provided

IndXSeq{ P

provided

A1:
P_{1}[ {} ]
and

A2: for p being XFinSequence

for x being object st P_{1}[p] holds

P_{1}[p ^ <%x%>]

A2: for p being XFinSequence

for x being object st P

P

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

ex t being XFinSequence st p ^ t = r

proof end;

definition

let D be set ;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff x is XFinSequence of D )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff x is XFinSequence of D ) ) & ( for x being object holds

( x in b_{2} iff x is XFinSequence of D ) ) holds

b_{1} = b_{2}

end;
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 for x being object holds

( x in it iff x is XFinSequence of D );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def7 defines ^omega AFINSQ_1:def 7 :

for D, b_{2} being set holds

( b_{2} = D ^omega iff for x being object holds

( x in b_{2} iff x is XFinSequence of D ) );

for D, b

( b

( x in b

registration
end;

theorem :: AFINSQ_1:42

scheme :: AFINSQ_1:sch 4

SepXSeq{ F_{1}() -> non empty set , P_{1}[ XFinSequence] } :

SepXSeq{ F

ex X being set st

for x being object holds

( x in X iff ex p being XFinSequence st

( p in F_{1}() ^omega & P_{1}[p] & x = p ) )

for x being object holds

( x in X iff ex p being XFinSequence st

( p in F

proof end;

registration

let p be XFinSequence;

let i, x be object ;

coherence

( p +* (i,x) is finite & p +* (i,x) is Sequence-like )

end;
let i, x be object ;

coherence

( p +* (i,x) is finite & p +* (i,x) is Sequence-like )

proof 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 ) )

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;

coherence

Replace (p,i,a) is D -valued

end;
let p be XFinSequence of D;

let i be Element of NAT ;

let a be Element of D;

coherence

Replace (p,i,a) is D -valued

proof end;

:: missing, 2008.02.02, A.K.

registration
end;

registration
end;

registration

existence

ex b_{1} being XFinSequence st

( not b_{1} is empty & b_{1} is natural-valued )

end;
ex b

( not b

proof 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 )

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 )

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 )

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 )

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 )

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 )

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 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 )

for p being XFinSequence st n <= len p & k in n holds

( (p | n) . k = p . k & k in dom p )

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 )

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;

definition

let D be set ;

let q be FinSequence of D;

ex b_{1} being XFinSequence of D st

( len b_{1} = len q & ( for i being Nat st i < len q holds

q . (i + 1) = b_{1} . i ) )

for b_{1}, b_{2} being XFinSequence of D st len b_{1} = len q & ( for i being Nat st i < len q holds

q . (i + 1) = b_{1} . i ) & len b_{2} = len q & ( for i being Nat st i < len q holds

q . (i + 1) = b_{2} . i ) holds

b_{1} = b_{2}

end;
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 ( len it = len q & ( for i being Nat st i < len q holds

q . (i + 1) = it . i ) );

ex b

( len b

q . (i + 1) = b

proof end;

uniqueness for b

q . (i + 1) = b

q . (i + 1) = b

b

proof end;

:: deftheorem Def8 defines FS2XFS AFINSQ_1:def 8 :

for D being set

for q being FinSequence of D

for b_{3} being XFinSequence of D holds

( b_{3} = FS2XFS q iff ( len b_{3} = len q & ( for i being Nat st i < len q holds

q . (i + 1) = b_{3} . i ) ) );

for D being set

for q being FinSequence of D

for b

( b

q . (i + 1) = b

definition

let q be XFinSequence;

ex b_{1} being FinSequence st

( len b_{1} = len q & ( for i being Nat st 1 <= i & i <= len q holds

q . (i -' 1) = b_{1} . i ) )

for b_{1}, b_{2} being FinSequence st len b_{1} = len q & ( for i being Nat st 1 <= i & i <= len q holds

q . (i -' 1) = b_{1} . i ) & len b_{2} = len q & ( for i being Nat st 1 <= i & i <= len q holds

q . (i -' 1) = b_{2} . i ) holds

b_{1} = b_{2}

end;
func XFS2FS q -> FinSequence means :Def9A: :: 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 ( len it = len q & ( for i being Nat st 1 <= i & i <= len q holds

q . (i -' 1) = it . i ) );

ex b

( len b

q . (i -' 1) = b

proof end;

uniqueness for b

q . (i -' 1) = b

q . (i -' 1) = b

b

proof end;

:: deftheorem Def9A defines XFS2FS AFINSQ_1:def 9 :

for q being XFinSequence

for b_{2} being FinSequence holds

( b_{2} = XFS2FS q iff ( len b_{2} = len q & ( for i being Nat st 1 <= i & i <= len q holds

q . (i -' 1) = b_{2} . i ) ) );

for q being XFinSequence

for b

( b

q . (i -' 1) = b

definition

let D be set ;

let q be XFinSequence of D;

:: original: XFS2FS

redefine func XFS2FS q -> FinSequence of D;

coherence

XFS2FS q is FinSequence of D

end;
let q be XFinSequence of D;

:: original: XFS2FS

redefine func XFS2FS q -> FinSequence of D;

coherence

XFS2FS q is FinSequence of D

proof end;

theorem :: AFINSQ_1:63

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 ;

ex b_{1} being non empty XFinSequence of D st

( len q = b_{1} . 0 & len b_{1} = n & ( for i being Nat st 1 <= i & i <= len q holds

b_{1} . i = q . i ) & ( for j being Nat st len q < j & j < n holds

b_{1} . j = 0 ) )

for b_{1}, b_{2} being non empty XFinSequence of D st len q = b_{1} . 0 & len b_{1} = n & ( for i being Nat st 1 <= i & i <= len q holds

b_{1} . i = q . i ) & ( for j being Nat st len q < j & j < n holds

b_{1} . j = 0 ) & len q = b_{2} . 0 & len b_{2} = n & ( for i being Nat st 1 <= i & i <= len q holds

b_{2} . i = q . i ) & ( for j being Nat st len q < j & j < n holds

b_{2} . j = 0 ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( len q = b

b

b

proof end;

uniqueness for b

b

b

b

b

b

proof 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 b_{4} being non empty XFinSequence of D holds

( b_{4} = FS2XFS* (q,n) iff ( len q = b_{4} . 0 & len b_{4} = n & ( for i being Nat st 1 <= i & i <= len q holds

b_{4} . i = q . i ) & ( for j being Nat st len q < j & j < n holds

b_{4} . j = 0 ) ) );

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 b

( b

b

b

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 ;

ex b_{1} being FinSequence of D st

for m being Nat st m = p . 0 holds

( len b_{1} = m & ( for i being Nat st 1 <= i & i <= m holds

b_{1} . i = p . i ) )

for b_{1}, b_{2} being FinSequence of D st ( for m being Nat st m = p . 0 holds

( len b_{1} = m & ( for i being Nat st 1 <= i & i <= m holds

b_{1} . i = p . i ) ) ) & ( for m being Nat st m = p . 0 holds

( len b_{2} = m & ( for i being Nat st 1 <= i & i <= m holds

b_{2} . i = p . i ) ) ) holds

b_{1} = b_{2}

end;
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 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 ) );

ex b

for m being Nat st m = p . 0 holds

( len b

b

proof end;

uniqueness for b

( len b

b

( len b

b

b

proof 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 b_{3} being FinSequence of D holds

( b_{3} = XFS2FS* p iff for m being Nat st m = p . 0 holds

( len b_{3} = m & ( for i being Nat st 1 <= i & i <= m holds

b_{3} . i = p . i ) ) );

for D being non empty set

for p being XFinSequence of D st p . 0 is Nat & p . 0 in len p holds

for b

( b

( len b

b

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 = {}

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.

:: 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 );

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 );

:: following, 2010.01.11, A.T.

registration

coherence

for b_{1} being Function st b_{1} is initial & b_{1} is finite & b_{1} is NAT -defined holds

b_{1} is Sequence-like

end;
for b

b

proof end;

theorem :: AFINSQ_1:66

:: from AMISTD_2, 2010.04.16, A.T.

theorem :: AFINSQ_1:67

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

for G being NAT -defined non empty finite Function st F c= G & LastLoc F = LastLoc G holds

F = G

proof end;

theorem :: AFINSQ_1:71

registration

let F be NAT -defined non empty finite initial Function;

coherence

CutLastLoc F is initial

end;
coherence

CutLastLoc F is initial

proof 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)))

for J being Function holds dom I misses dom (Shift (J,(card I)))

proof end;

:: from SCMPDS_4, 2010.05.14, A.T.

:: from SCM_COMP, 2010.05.16, A.T.

registration
end;

registration

let D be set ;

coherence

for b_{1} being Element of D ^omega holds

( b_{1} is finite & b_{1} is Sequence-like )
by Def7;

end;
coherence

for b

( b

definition
end;

:: deftheorem defines Down AFINSQ_1:def 13 :

for D being set

for f being XFinSequence of D holds Down f = f;

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

end;
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;

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

end;
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;

:: missing, 2010.05.15, A.T.

theorem :: AFINSQ_1:78

for p, q being XFinSequence holds

( p +* (p ^ q) = p ^ q & (p ^ q) +* p = p ^ q ) by Th71, FUNCT_4:97, FUNCT_4:98;

( p +* (p ^ q) = p ^ q & (p ^ q) +* p = p ^ q ) by Th71, FUNCT_4:97, FUNCT_4:98;

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))))

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 :: 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

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

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
end;

definition
end;

:: deftheorem defines <% AFINSQ_1:def 14 :

for x1, x2, x3, x4 being object holds <%x1,x2,x3,x4%> = ((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>;

for x1, x2, x3, x4 being object holds <%x1,x2,x3,x4%> = ((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>;

registration

let x1, x2, x3, x4 be object ;

coherence

( <%x1,x2,x3,x4%> is Function-like & <%x1,x2,x3,x4%> is Relation-like ) ;

end;
coherence

( <%x1,x2,x3,x4%> is Function-like & <%x1,x2,x3,x4%> is Relation-like ) ;

registration

let x1, x2, x3, x4 be object ;

coherence

( <%x1,x2,x3,x4%> is finite & <%x1,x2,x3,x4%> is Sequence-like ) ;

end;
coherence

( <%x1,x2,x3,x4%> is finite & <%x1,x2,x3,x4%> is Sequence-like ) ;

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 ;

reducibility

<%x1,x2,x3,x4%> . 0 = x1

<%x1,x2,x3,x4%> . 1 = x2 by Lm3;

reducibility

<%x1,x2,x3,x4%> . 2 = x3 by Lm3;

reducibility

<%x1,x2,x3,x4%> . 3 = x4 by Lm3;

end;
reducibility

<%x1,x2,x3,x4%> . 0 = x1

proof end;

reducibility <%x1,x2,x3,x4%> . 1 = x2 by Lm3;

reducibility

<%x1,x2,x3,x4%> . 2 = x3 by Lm3;

reducibility

<%x1,x2,x3,x4%> . 3 = x4 by Lm3;

::$CT

theorem :: AFINSQ_1:86

:: 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

:: 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

:: the mirror theorem of BALLOT_1:5, but also for empty D

registration
end;

theorem Th13: :: AFINSQ_1:94

for D being set

for p being FinSequence of D

for n being Nat holds

( n + 1 in dom p iff n in dom (FS2XFS p) )

for p being FinSequence of D

for n being Nat holds

( n + 1 in dom p iff n in dom (FS2XFS p) )

proof end;

theorem Th14: :: AFINSQ_1:95

for D being set

for p being XFinSequence of D

for n being Nat holds

( n in dom p iff n + 1 in dom (XFS2FS p) )

for p being XFinSequence of D

for n being Nat holds

( n in dom p iff n + 1 in dom (XFS2FS p) )

proof end;

registration
end;

registration
end;

:: generalizes BALLOT_1:2 to empty D

registration
end;

registration
end;