:: Zero Based Finite Sequences
:: 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

theorem Th0: :: AFINSQ_1:1

for n being non zero Nat holds
( n - 1 is Nat & 1 <= n )

proof end;

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 = {0} \/ (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

mode XFinSequence is finite Sequence;

end;

registration

let p be XFinSequence;

cluster dom p -> natural ;

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;

identify dom p with len p;

compatibility
dom p = len p ;

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{ F₁() -> Nat, P₁[ object , object ] } :

ex p being XFinSequence st
( dom p = F₁() & ( for k being Nat st k in F₁() holds
P₁[k,p . k] ) )

provided

A1: for k being Nat st k in F₁() holds
ex x being object st P₁[k,x]

proof end;

scheme :: AFINSQ_1:sch 2
XSeqLambda{ F₁() -> Nat, F₂( object ) -> object } :

ex p being XFinSequence st
( len p = F₁() & ( for k being Nat st k in F₁() holds
p . k = F₂(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 ;

cluster Relation-like D -valued Sequence-like Function-like finite for set ;

existence
ex b₁ being Sequence of D st b₁ 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

cluster Relation-like Function-like empty -> Sequence-like for set ;

coherence
for b₁ being Function st b₁ is empty holds
b₁ is Sequence-like ;

end;

registration

let k be Nat;
let a be object ;

cluster (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 ;

cluster Relation-like D -valued Sequence-like Function-like empty finite for set ;

existence
ex b₁ being XFinSequence of D st b₁ is empty

proof end;

end;

registration

let D be non empty set ;

cluster Relation-like D -valued Sequence-like Function-like non empty finite for set ;

existence
not for b₁ being XFinSequence of D holds b₁ 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 b₁ being set holds
( b₁ = p ^ q iff ( dom b₁ = (len p) + (len q) & ( for k being Nat st k in dom p holds
b₁ . k = p . k ) & ( for k being Nat st k in dom q holds
b₁ . ((len p) + k) = q . k ) ) )

proof end;

end;

:: deftheorem Def3 defines ^ AFINSQ_1:def 3 :
for p, q being XFinSequence
for b₃ being set holds
( b₃ = p ^ q iff ( dom b₃ = (len p) + (len q) & ( for k being Nat st k in dom p holds
b₃ . k = p . k ) & ( for k being Nat st k in dom q holds
b₃ . ((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 :: AFINSQ_1:24

for p, q being XFinSequence holds rng p c= rng (p ^ q)

proof end;

theorem :: 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) by ORDINAL4:2;

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 b₁ being Function holds
( b₁ = <%x%> iff ( dom b₁ = 1 & b₁ . 0 = x ) )

proof end;

end;

:: deftheorem Def4 defines <% AFINSQ_1:def 4 :
for x being object
for b₂ being Function holds
( b₂ = <%x%> iff ( dom b₂ = 1 & b₂ . 0 = x ) );

registration

let x be object ;

cluster <%x%> -> Relation-like Function-like ;

coherence
( <%x%> is Function-like & <%x%> is Relation-like ) ;

end;

registration

let x be object ;

cluster <%x%> -> Sequence-like finite ;

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
(<%x%> ^ <%y%>) ^ <%z%>;

correctness
coherence
(<%x%> ^ <%y%>) ^ <%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%> = (<%x%> ^ <%y%>) ^ <%z%>;

registration

let x, y be object ;

cluster <%x,y%> -> Relation-like Function-like ;

coherence
( <%x,y%> is Function-like & <%x,y%> is Relation-like ) ;
let z be object ;

cluster <%x,y,z%> -> Relation-like Function-like ;

coherence
( <%x,y,z%> is Function-like & <%x,y,z%> is Relation-like ) ;

end;

registration

let x, y be object ;

cluster <%x,y%> -> Sequence-like finite ;

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;

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

coherence
for b₁ being XFinSequence st b₁ is n -element holds
b₁ is n -defined ;

end;

registration

let n be Nat;
let x be object ;

cluster n --> x -> Sequence-like finite ;

coherence
( n --> x is finite & n --> x is Sequence-like ) ;

end;

registration

let n be Nat;

cluster Relation-like Sequence-like Function-like finite n -element for set ;

existence
ex b₁ being XFinSequence st b₁ is n -element

proof end;

end;

registration

let n be Nat;

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

coherence
for b₁ being n -defined n -element XFinSequence holds b₁ 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{ P₁[ XFinSequence] } :

for p being XFinSequence holds P₁[p]

provided

A1: P₁[ {} ] and
A2: for p being XFinSequence
for x being object st P₁[p] holds
P₁[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 b₁ being set st
for x being object holds
( x in b₁ iff x is XFinSequence of D )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff x is XFinSequence of D ) ) & ( for x being object holds
( x in b₂ iff x is XFinSequence of D ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines ^omega AFINSQ_1:def 7 :
for D, b₂ being set holds
( b₂ = D ^omega iff for x being object holds
( x in b₂ 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{ F₁() -> non empty set , P₁[ XFinSequence] } :

ex X being set st
for x being object holds
( x in X iff ex p being XFinSequence st
( p in F₁() ^omega & P₁[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 Replace (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

cluster Relation-like REAL -valued Sequence-like Function-like finite -> real-valued for set ;

coherence
for b₁ being XFinSequence of REAL holds b₁ is real-valued

proof end;

end;

registration

cluster Relation-like NAT -valued Sequence-like Function-like finite -> natural-valued for set ;

coherence
for b₁ being XFinSequence of NAT holds b₁ is natural-valued

proof end;

end;

registration

cluster Relation-like Sequence-like Function-like non empty finite natural-valued for set ;

existence
ex b₁ being XFinSequence st
( not b₁ is empty & b₁ 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 b₁ being XFinSequence of D st
( len b₁ = len q & ( for i being Nat st i < len q holds
q . (i + 1) = b₁ . i ) )

proof end;

uniqueness
for b₁, b₂ being XFinSequence of D st len b₁ = len q & ( for i being Nat st i < len q holds
q . (i + 1) = b₁ . i ) & len b₂ = len q & ( for i being Nat st i < len q holds
q . (i + 1) = b₂ . i ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines FS2XFS AFINSQ_1:def 8 :
for D being set
for q being FinSequence of D
for b₃ being XFinSequence of D holds
( b₃ = FS2XFS q iff ( len b₃ = len q & ( for i being Nat st i < len q holds
q . (i + 1) = b₃ . i ) ) );

definition

let q be XFinSequence;

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
ex b₁ being FinSequence st
( len b₁ = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = b₁ . i ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence st len b₁ = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = b₁ . i ) & len b₂ = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = b₂ . i ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9A defines XFS2FS AFINSQ_1:def 9 :
for q being XFinSequence
for b₂ being FinSequence holds
( b₂ = XFS2FS q iff ( len b₂ = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = b₂ . i ) ) );

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

proof end;

end;

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 b₁ being non empty XFinSequence of D st
( len q = b₁ . 0 & len b₁ = n & ( for i being Nat st 1 <= i & i <= len q holds
b₁ . i = q . i ) & ( for j being Nat st len q < j & j < n holds
b₁ . j = 0 ) )

proof end;

uniqueness
for b₁, b₂ being non empty XFinSequence of D st len q = b₁ . 0 & len b₁ = n & ( for i being Nat st 1 <= i & i <= len q holds
b₁ . i = q . i ) & ( for j being Nat st len q < j & j < n holds
b₁ . j = 0 ) & len q = b₂ . 0 & len b₂ = n & ( for i being Nat st 1 <= i & i <= len q holds
b₂ . i = q . i ) & ( for j being Nat st len q < j & j < n holds
b₂ . j = 0 ) holds
b₁ = b₂

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 b₄ being non empty XFinSequence of D holds
( b₄ = FS2XFS* (q,n) iff ( len q = b₄ . 0 & len b₄ = n & ( for i being Nat st 1 <= i & i <= len q holds
b₄ . i = q . i ) & ( for j being Nat st len q < j & j < n holds
b₄ . 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 b₁ being FinSequence of D st
for m being Nat st m = p . 0 holds
( len b₁ = m & ( for i being Nat st 1 <= i & i <= m holds
b₁ . i = p . i ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of D st ( for m being Nat st m = p . 0 holds
( len b₁ = m & ( for i being Nat st 1 <= i & i <= m holds
b₁ . i = p . i ) ) ) & ( for m being Nat st m = p . 0 holds
( len b₂ = m & ( for i being Nat st 1 <= i & i <= m holds
b₂ . i = p . i ) ) ) holds
b₁ = b₂

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 b₃ being FinSequence of D holds
( b₃ = XFS2FS* p iff for m being Nat st m = p . 0 holds
( len b₃ = m & ( for i being Nat st 1 <= i & i <= m holds
b₃ . 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

cluster Relation-like Function-like empty -> initial for set ;

coherence
for b₁ being Function st b₁ is empty holds
b₁ is initial ;

end;

registration

cluster Relation-like Sequence-like Function-like finite -> initial for set ;

coherence
for b₁ being XFinSequence holds b₁ is initial

proof end;

end;

:: following, 2010.01.11, A.T.

registration

cluster Relation-like Sequence-like Function-like finite -> NAT -defined for set ;

coherence
for b₁ being XFinSequence holds b₁ 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

cluster Relation-like NAT -defined Function-like finite initial -> Sequence-like for set ;

coherence
for b₁ being Function st b₁ is initial & b₁ is finite & b₁ is NAT -defined holds
b₁ 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 Th62, VALUED_1:35;

registration

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

cluster CutLastLoc F -> initial ;

coherence
CutLastLoc F is initial

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 ;

cluster D ^omega -> functional ;

coherence
D ^omega is functional by Def7;

end;

registration

let D be set ;

cluster -> Sequence-like finite for Element of D ^omega ;

coherence
for b₁ being Element of D ^omega holds
( b₁ is finite & b₁ 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 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))))

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;

cluster CutLastLoc F -> initial ;

coherence
CutLastLoc F is initial ;

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;

:: this holds more basically for any Sequence A, but since
:: the properties of Sequences of the form A ^ <%x%> are not in Mizar yet
:: I have no desire to formally introduce everything of that here, too

theorem :: AFINSQ_1:92

for p being XFinSequence
for x being object holds last (p ^ <%x%>) = x

proof end;

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

theorem Th12: :: AFINSQ_1:93

for D being set
for p being XFinSequence of D holds FS2XFS (XFS2FS p) = p

proof end;

registration

let D be set ;
let f be XFinSequence of D;

reduce FS2XFS (XFS2FS f) to f;

reducibility
FS2XFS (XFS2FS f) = f by Th12;

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

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

proof end;

registration

let D be set ;
let p be one-to-one FinSequence of D;

cluster FS2XFS p -> one-to-one ;

coherence
FS2XFS p is one-to-one

proof end;

end;

registration

let D be set ;
let p be one-to-one XFinSequence of D;

cluster XFS2FS p -> one-to-one ;

coherence
XFS2FS p is one-to-one

proof end;

end;

theorem Th15: :: AFINSQ_1:96

for D being set
for p being FinSequence of D holds rng p = rng (FS2XFS p)

proof end;

:: generalizes BALLOT_1:2 to empty D

theorem :: AFINSQ_1:97

for D being set
for p being XFinSequence of D holds rng p = rng (XFS2FS p)

proof end;

registration

let D be set ;
let p be empty XFinSequence of D;

cluster XFS2FS p -> empty ;

coherence
XFS2FS p is empty

proof end;

end;

registration

let D be set ;
let p be empty FinSequence of D;

cluster FS2XFS p -> empty ;

coherence
FS2XFS p is empty

proof end;

end;