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

Lm1: for n being 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 12;

end;

:: Schemes of existence

scheme :: RECDEF_1:sch 1
RecEx{ F₁() -> object , P₁[ object , object , object ] } :

ex f being Function st
( dom f = NAT & f . 0 = F₁() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) )

provided

A1: for n being Nat
for x being set ex y being set st P₁[n,x,y]

proof end;

scheme :: RECDEF_1:sch 2
RecExD{ F₁() -> non empty set , F₂() -> Element of F₁(), P₁[ object , object , object ] } :

ex f being sequence of F₁() st
( f . 0 = F₂() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) )

provided

A1: for n being Nat
for x being Element of F₁() ex y being Element of F₁() st P₁[n,x,y]

proof end;

Lm2: 1 in REAL
by NUMBERS:19;

scheme :: RECDEF_1:sch 3
FinRecEx{ F₁() -> object , F₂() -> Nat, P₁[ object , object , object ] } :

ex p being FinSequence st
( len p = F₂() & ( p . 1 = F₁() or F₂() = 0 ) & ( for n being Nat st 1 <= n & n < F₂() holds
P₁[n,p . n,p . (n + 1)] ) )

provided

A1: for n being Nat st 1 <= n & n < F₂() holds
for x being set ex y being set st P₁[n,x,y]

proof end;

scheme :: RECDEF_1:sch 4
FinRecExD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Nat, P₁[ object , object , object ] } :

ex p being FinSequence of F₁() st
( len p = F₃() & ( p . 1 = F₂() or F₃() = 0 ) & ( for n being Nat st 1 <= n & n < F₃() holds
P₁[n,p . n,p . (n + 1)] ) )

provided

A1: for n being Nat st 1 <= n & n < F₃() holds
for x being Element of F₁() ex y being Element of F₁() st P₁[n,x,y]

proof end;

scheme :: RECDEF_1:sch 5
SeqBinOpEx{ F₁() -> FinSequence, P₁[ object , object , object ] } :

ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
P₁[F₁() . (k + 1),p . k,p . (k + 1)] ) )

provided

A1: for k being Nat
for x being set st 1 <= k & k < len F₁() holds
ex y being set st P₁[F₁() . (k + 1),x,y]

proof end;

scheme :: RECDEF_1:sch 6
LambdaSeqBinOpEx{ F₁() -> FinSequence, F₂( object , object ) -> set } :

ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) )

proof end;

:: Schemes of uniqueness

scheme :: RECDEF_1:sch 7
FinRecUn{ F₁() -> object , F₂() -> Nat, F₃() -> FinSequence, F₄() -> FinSequence, P₁[ object , object , object ] } :

F₃() = F₄()

provided

A1: for n being Nat st 1 <= n & n < F₂() holds
for x, y1, y2 being set st P₁[n,x,y1] & P₁[n,x,y2] holds
y1 = y2 and
A2: ( len F₃() = F₂() & ( F₃() . 1 = F₁() or F₂() = 0 ) & ( for n being Nat st 1 <= n & n < F₂() holds
P₁[n,F₃() . n,F₃() . (n + 1)] ) ) and
A3: ( len F₄() = F₂() & ( F₄() . 1 = F₁() or F₂() = 0 ) & ( for n being Nat st 1 <= n & n < F₂() holds
P₁[n,F₄() . n,F₄() . (n + 1)] ) )

proof end;

scheme :: RECDEF_1:sch 8
FinRecUnD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Nat, F₄() -> FinSequence of F₁(), F₅() -> FinSequence of F₁(), P₁[ object , object , object ] } :

F₄() = F₅()

provided

A1: for n being Nat st 1 <= n & n < F₃() holds
for x, y1, y2 being Element of F₁() st P₁[n,x,y1] & P₁[n,x,y2] holds
y1 = y2 and
A2: ( len F₄() = F₃() & ( F₄() . 1 = F₂() or F₃() = 0 ) & ( for n being Nat st 1 <= n & n < F₃() holds
P₁[n,F₄() . n,F₄() . (n + 1)] ) ) and
A3: ( len F₅() = F₃() & ( F₅() . 1 = F₂() or F₃() = 0 ) & ( for n being Nat st 1 <= n & n < F₃() holds
P₁[n,F₅() . n,F₅() . (n + 1)] ) )

proof end;

scheme :: RECDEF_1:sch 9
SeqBinOpUn{ F₁() -> FinSequence, P₁[ object , object , object ], F₂() -> object , F₃() -> object } :

F₂() = F₃()

provided

A1: for k being Nat
for x, y1, y2, z being set st 1 <= k & k < len F₁() & z = F₁() . (k + 1) & P₁[z,x,y1] & P₁[z,x,y2] holds
y1 = y2 and
A2: ex p being FinSequence st
( F₂() = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
P₁[F₁() . (k + 1),p . k,p . (k + 1)] ) ) and
A3: ex p being FinSequence st
( F₃() = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
P₁[F₁() . (k + 1),p . k,p . (k + 1)] ) )

proof end;

scheme :: RECDEF_1:sch 10
LambdaSeqBinOpUn{ F₁() -> FinSequence, F₂( object , object ) -> object , F₃() -> object , F₄() -> object } :

F₃() = F₄()

provided

A1: ex p being FinSequence st
( F₃() = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) ) and
A2: ex p being FinSequence st
( F₄() = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) )

proof end;

:: Schemes of definitness

scheme :: RECDEF_1:sch 11
DefRec{ F₁() -> object , F₂() -> Nat, P₁[ object , object , object ] } :

( ex y being set ex f being Function st
( y = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being set st ex f being Function st
( y1 = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) ) & ex f being Function st
( y2 = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) ) holds
y1 = y2 ) )

provided

A1: for n being Nat
for x being set ex y being set st P₁[n,x,y] and
A2: for n being Nat
for x, y1, y2 being set st P₁[n,x,y1] & P₁[n,x,y2] holds
y1 = y2

proof end;

scheme :: RECDEF_1:sch 12
LambdaDefRec{ F₁() -> object , F₂() -> Nat, F₃( object , object ) -> set } :

( ex y being set ex f being Function st
( y = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) ) & ( for y1, y2 being set st ex f being Function st
( y1 = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) ) & ex f being Function st
( y2 = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) ) holds
y1 = y2 ) )

proof end;

scheme :: RECDEF_1:sch 13
DefRecD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Nat, P₁[ object , object , object ] } :

( ex y being Element of F₁() ex f being sequence of F₁() st
( y = f . F₃() & f . 0 = F₂() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being Element of F₁() st ex f being sequence of F₁() st
( y1 = f . F₃() & f . 0 = F₂() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) ) & ex f being sequence of F₁() st
( y2 = f . F₃() & f . 0 = F₂() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) ) holds
y1 = y2 ) )

provided

A1: for n being Nat
for x being Element of F₁() ex y being Element of F₁() st P₁[n,x,y] and
A2: for n being Nat
for x, y1, y2 being Element of F₁() st P₁[n,x,y1] & P₁[n,x,y2] holds
y1 = y2

proof end;

scheme :: RECDEF_1:sch 14
LambdaDefRecD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Nat, F₄( object , object ) -> Element of F₁() } :

( ex y being Element of F₁() ex f being sequence of F₁() st
( y = f . F₃() & f . 0 = F₂() & ( for n being Nat holds f . (n + 1) = F₄(n,(f . n)) ) ) & ( for y1, y2 being Element of F₁() st ex f being sequence of F₁() st
( y1 = f . F₃() & f . 0 = F₂() & ( for n being Nat holds f . (n + 1) = F₄(n,(f . n)) ) ) & ex f being sequence of F₁() st
( y2 = f . F₃() & f . 0 = F₂() & ( for n being Nat holds f . (n + 1) = F₄(n,(f . n)) ) ) holds
y1 = y2 ) )

proof end;

scheme :: RECDEF_1:sch 15
SeqBinOpDef{ F₁() -> FinSequence, P₁[ object , object , object ] } :

( ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
P₁[F₁() . (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 F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
P₁[F₁() . (k + 1),p . k,p . (k + 1)] ) ) & ex p being FinSequence st
( y = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
P₁[F₁() . (k + 1),p . k,p . (k + 1)] ) ) holds
x = y ) )

provided

A1: for k being Nat
for y being set st 1 <= k & k < len F₁() holds
ex z being set st P₁[F₁() . (k + 1),y,z] and
A2: for k being Nat
for x, y1, y2, z being set st 1 <= k & k < len F₁() & z = F₁() . (k + 1) & P₁[z,x,y1] & P₁[z,x,y2] holds
y1 = y2

proof end;

scheme :: RECDEF_1:sch 16
LambdaSeqBinOpDef{ F₁() -> FinSequence, F₂( object , object ) -> set } :

( ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) ) & ( for x, y being set st ex p being FinSequence st
( x = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) ) & ex p being FinSequence st
( y = p . (len p) & len p = len F₁() & p . 1 = F₁() . 1 & ( for k being Nat st 1 <= k & k < len F₁() holds
p . (k + 1) = F₂((F₁() . (k + 1)),(p . k)) ) ) holds
x = y ) )

proof end;

:: from POLYNOM2, 2010.02.13, A.T.

scheme :: RECDEF_1:sch 17
SeqExD{ F₁() -> non empty set , F₂() -> Nat, P₁[ object , object ] } :

ex p being FinSequence of F₁() st
( dom p = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
P₁[k,p /. k] ) )

provided

A1: for k being Nat st k in Seg F₂() holds
ex x being Element of F₁() st P₁[k,x]

proof end;

scheme :: RECDEF_1:sch 18
FinRecExD2{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of NAT , P₁[ object , object , object ] } :

ex p being FinSequence of F₁() st
( len p = F₃() & ( p /. 1 = F₂() or F₃() = 0 ) & ( for n being Nat st 1 <= n & n <= F₃() - 1 holds
P₁[n,p /. n,p /. (n + 1)] ) )

provided

A1: for n being Nat st 1 <= n & n <= F₃() - 1 holds
for x being Element of F₁() ex y being Element of F₁() st P₁[n,x,y]

proof end;