:: Recursive Definitions
:: by Krzysztof Hryniewiecki
::
:: Received September 4, 1989
:: Copyright (c) 1990-2011 Association of Mizar Users


begin

Lm1: for n being Element of NAT
for D being non empty set
for p being FinSequence of D st 1 <= n & n <= len p holds
p . n is Element of D
proof end;

definition
let p be natural-valued Function;
let n be set ;
:: original: .
redefine func p . n -> Element of NAT ;
coherence
p . n is Element of NAT by ORDINAL1:def 13;
end;

scheme :: RECDEF_1:sch 1
RecEx{ F1() -> set , P1[ set , set , set ] } :
ex f being Function st
( dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) )
provided
A1: for n being Element of NAT
for x being set ex y being set st P1[n,x,y]
proof end;

scheme :: RECDEF_1:sch 2
RecExD{ F1() -> non empty set , F2() -> Element of F1(), P1[ set , set , set ] } :
ex f being Function of NAT,F1() st
( f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) )
provided
A1: for n being Element of NAT
for x being Element of F1() ex y being Element of F1() st P1[n,x,y]
proof end;

scheme :: RECDEF_1:sch 3
FinRecEx{ F1() -> set , F2() -> Nat, P1[ set , set , set ] } :
ex p being FinSequence st
( len p = F2() & ( p . 1 = F1() or F2() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F2() holds
P1[n,p . n,p . (n + 1)] ) )
provided
A1: for n being Element of NAT st 1 <= n & n < F2() holds
for x being set ex y being set st P1[n,x,y]
proof end;

scheme :: RECDEF_1:sch 4
FinRecExD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Nat, P1[ set , set , set ] } :
ex p being FinSequence of F1() st
( len p = F3() & ( p . 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F3() holds
P1[n,p . n,p . (n + 1)] ) )
provided
A1: for n being Element of NAT st 1 <= n & n < F3() holds
for x being Element of F1() ex y being Element of F1() st P1[n,x,y]
proof end;

scheme :: RECDEF_1:sch 5
SeqBinOpEx{ F1() -> FinSequence, P1[ set , set , set ] } :
ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) )
provided
A1: for k being Element of NAT
for x being set st 1 <= k & k < len F1() holds
ex y being set st P1[F1() . (k + 1),x,y]
proof end;

scheme :: RECDEF_1:sch 6
LambdaSeqBinOpEx{ F1() -> FinSequence, F2( set , set ) -> set } :
ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) )
proof end;

scheme :: RECDEF_1:sch 7
FinRecUn{ F1() -> set , F2() -> Nat, F3() -> FinSequence, F4() -> FinSequence, P1[ set , set , set ] } :
F3() = F4()
provided
A1: for n being Element of NAT st 1 <= n & n < F2() holds
for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2 and
A2: ( len F3() = F2() & ( F3() . 1 = F1() or F2() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F2() holds
P1[n,F3() . n,F3() . (n + 1)] ) ) and
A3: ( len F4() = F2() & ( F4() . 1 = F1() or F2() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F2() holds
P1[n,F4() . n,F4() . (n + 1)] ) )
proof end;

scheme :: RECDEF_1:sch 8
FinRecUnD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Nat, F4() -> FinSequence of F1(), F5() -> FinSequence of F1(), P1[ set , set , set ] } :
F4() = F5()
provided
A1: for n being Element of NAT st 1 <= n & n < F3() holds
for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2 and
A2: ( len F4() = F3() & ( F4() . 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F3() holds
P1[n,F4() . n,F4() . (n + 1)] ) ) and
A3: ( len F5() = F3() & ( F5() . 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F3() holds
P1[n,F5() . n,F5() . (n + 1)] ) )
proof end;

scheme :: RECDEF_1:sch 9
SeqBinOpUn{ F1() -> FinSequence, P1[ set , set , set ], F2() -> set , F3() -> set } :
F2() = F3()
provided
A1: for k being Element of NAT
for x, y1, y2, z being set st 1 <= k & k < len F1() & z = F1() . (k + 1) & P1[z,x,y1] & P1[z,x,y2] holds
y1 = y2 and
A2: ex p being FinSequence st
( F2() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) and
A3: ex p being FinSequence st
( F3() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) )
proof end;

scheme :: RECDEF_1:sch 10
LambdaSeqBinOpUn{ F1() -> FinSequence, F2( set , set ) -> set , F3() -> set , F4() -> set } :
F3() = F4()
provided
A1: ex p being FinSequence st
( F3() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) and
A2: ex p being FinSequence st
( F4() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) )
proof end;

scheme :: RECDEF_1:sch 11
DefRec{ F1() -> set , F2() -> Nat, P1[ set , set , set ] } :
( ex y being set ex f being Function st
( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being set st ex f being Function st
( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function st
( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) holds
y1 = y2 ) )
provided
A1: for n being Element of NAT
for x being set ex y being set st P1[n,x,y] and
A2: for n being Element of NAT
for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
proof end;

scheme :: RECDEF_1:sch 12
LambdaDefRec{ F1() -> set , F2() -> Nat, F3( set , set ) -> set } :
( ex y being set ex f being Function st
( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) & ( for y1, y2 being set st ex f being Function st
( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) & ex f being Function st
( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) holds
y1 = y2 ) )
proof end;

scheme :: RECDEF_1:sch 13
DefRecD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Nat, P1[ set , set , set ] } :
( ex y being Element of F1() ex f being Function of NAT,F1() st
( y = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being Element of F1() st ex f being Function of NAT,F1() st
( y1 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function of NAT,F1() st
( y2 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) holds
y1 = y2 ) )
provided
A1: for n being Element of NAT
for x being Element of F1() ex y being Element of F1() st P1[n,x,y] and
A2: for n being Element of NAT
for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
proof end;

scheme :: RECDEF_1:sch 14
LambdaDefRecD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Nat, F4( set , set ) -> Element of F1() } :
( ex y being Element of F1() ex f being Function of NAT,F1() st
( y = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) & ( for y1, y2 being Element of F1() st ex f being Function of NAT,F1() st
( y1 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) & ex f being Function of NAT,F1() st
( y2 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) holds
y1 = y2 ) )
proof end;

scheme :: RECDEF_1:sch 15
SeqBinOpDef{ F1() -> FinSequence, P1[ set , set , set ] } :
( ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) & ( for x, y being set st ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) & ex p being FinSequence st
( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) holds
x = y ) )
provided
A1: for k being Element of NAT
for y being set st 1 <= k & k < len F1() holds
ex z being set st P1[F1() . (k + 1),y,z] and
A2: for k being Element of NAT
for x, y1, y2, z being set st 1 <= k & k < len F1() & z = F1() . (k + 1) & P1[z,x,y1] & P1[z,x,y2] holds
y1 = y2
proof end;

scheme :: RECDEF_1:sch 16
LambdaSeqBinOpDef{ F1() -> FinSequence, F2( set , set ) -> set } :
( ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) & ( for x, y being set st ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) & ex p being FinSequence st
( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) holds
x = y ) )
proof end;

scheme :: RECDEF_1:sch 17
SeqExD{ F1() -> non empty set , F2() -> Element of NAT , P1[ set , set ] } :
ex p being FinSequence of F1() st
( dom p = Seg F2() & ( for k being Element of NAT st k in Seg F2() holds
P1[k,p /. k] ) )
provided
A1: for k being Element of NAT st k in Seg F2() holds
ex x being Element of F1() st P1[k,x]
proof end;

scheme :: RECDEF_1:sch 18
FinRecExD2{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Element of NAT , P1[ set , set , set ] } :
ex p being FinSequence of F1() st
( len p = F3() & ( p /. 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n <= F3() - 1 holds
P1[n,p /. n,p /. (n + 1)] ) )
provided
A1: for n being Element of NAT st 1 <= n & n <= F3() - 1 holds
for x being Element of F1() ex y being Element of F1() st P1[n,x,y]
proof end;