:: 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;
let n be set ;

:: original: .

redefine func p . n -> Element of NAT ;

coherence

p . n is Element of NAT by ORDINAL1:def 12;

:: Schemes of existence

Lm2: 1 in REAL

by NUMBERS:19;

scheme :: RECDEF_1:sch 4

FinRecExD{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}() -> Nat, P_{1}[ object , object , object ] } :

FinRecExD{ F

ex p being FinSequence of F_{1}() st

( len p = F_{3}() & ( p . 1 = F_{2}() or F_{3}() = 0 ) & ( for n being Nat st 1 <= n & n < F_{3}() holds

P_{1}[n,p . n,p . (n + 1)] ) )

provided( len p = F

P

A1:
for n being Nat st 1 <= n & n < F_{3}() holds

for x being Element of F_{1}() ex y being Element of F_{1}() st P_{1}[n,x,y]

for x being Element of F

proof end;

scheme :: RECDEF_1:sch 5

SeqBinOpEx{ F_{1}() -> FinSequence, P_{1}[ object , object , object ] } :

SeqBinOpEx{ F

ex x being set ex p being FinSequence st

( x = p . (len p) & len p = len F_{1}() & p . 1 = F_{1}() . 1 & ( for k being Nat st 1 <= k & k < len F_{1}() holds

P_{1}[F_{1}() . (k + 1),p . k,p . (k + 1)] ) )

provided( x = p . (len p) & len p = len F

P

A1:
for k being Nat

for x being set st 1 <= k & k < len F_{1}() holds

ex y being set st P_{1}[F_{1}() . (k + 1),x,y]

for x being set st 1 <= k & k < len F

ex y being set st P

proof end;

scheme :: RECDEF_1:sch 6

LambdaSeqBinOpEx{ F_{1}() -> FinSequence, F_{2}( object , object ) -> set } :

LambdaSeqBinOpEx{ F

ex x being set ex p being FinSequence st

( x = p . (len p) & len p = len F_{1}() & p . 1 = F_{1}() . 1 & ( for k being Nat st 1 <= k & k < len F_{1}() holds

p . (k + 1) = F_{2}((F_{1}() . (k + 1)),(p . k)) ) )

( x = p . (len p) & len p = len F

p . (k + 1) = F

proof end;

:: Schemes of uniqueness

scheme :: RECDEF_1:sch 7

FinRecUn{ F_{1}() -> object , F_{2}() -> Nat, F_{3}() -> FinSequence, F_{4}() -> FinSequence, P_{1}[ object , object , object ] } :

provided

FinRecUn{ F

provided

A1:
for n being Nat st 1 <= n & n < F_{2}() holds

for x, y1, y2 being set st P_{1}[n,x,y1] & P_{1}[n,x,y2] holds

y1 = y2 and

A2: ( len F_{3}() = F_{2}() & ( F_{3}() . 1 = F_{1}() or F_{2}() = 0 ) & ( for n being Nat st 1 <= n & n < F_{2}() holds

P_{1}[n,F_{3}() . n,F_{3}() . (n + 1)] ) )
and

A3: ( len F_{4}() = F_{2}() & ( F_{4}() . 1 = F_{1}() or F_{2}() = 0 ) & ( for n being Nat st 1 <= n & n < F_{2}() holds

P_{1}[n,F_{4}() . n,F_{4}() . (n + 1)] ) )

for x, y1, y2 being set st P

y1 = y2 and

A2: ( len F

P

A3: ( len F

P

proof end;

scheme :: RECDEF_1:sch 8

FinRecUnD{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}() -> Nat, F_{4}() -> FinSequence of F_{1}(), F_{5}() -> FinSequence of F_{1}(), P_{1}[ object , object , object ] } :

provided

FinRecUnD{ F

provided

A1:
for n being Nat st 1 <= n & n < F_{3}() holds

for x, y1, y2 being Element of F_{1}() st P_{1}[n,x,y1] & P_{1}[n,x,y2] holds

y1 = y2 and

A2: ( len F_{4}() = F_{3}() & ( F_{4}() . 1 = F_{2}() or F_{3}() = 0 ) & ( for n being Nat st 1 <= n & n < F_{3}() holds

P_{1}[n,F_{4}() . n,F_{4}() . (n + 1)] ) )
and

A3: ( len F_{5}() = F_{3}() & ( F_{5}() . 1 = F_{2}() or F_{3}() = 0 ) & ( for n being Nat st 1 <= n & n < F_{3}() holds

P_{1}[n,F_{5}() . n,F_{5}() . (n + 1)] ) )

for x, y1, y2 being Element of F

y1 = y2 and

A2: ( len F

P

A3: ( len F

P

proof end;

scheme :: RECDEF_1:sch 9

SeqBinOpUn{ F_{1}() -> FinSequence, P_{1}[ object , object , object ], F_{2}() -> object , F_{3}() -> object } :

provided

SeqBinOpUn{ F

provided

A1:
for k being Nat

for x, y1, y2, z being set st 1 <= k & k < len F_{1}() & z = F_{1}() . (k + 1) & P_{1}[z,x,y1] & P_{1}[z,x,y2] holds

y1 = y2 and

A2: ex p being FinSequence st

( F_{2}() = p . (len p) & len p = len F_{1}() & p . 1 = F_{1}() . 1 & ( for k being Nat st 1 <= k & k < len F_{1}() holds

P_{1}[F_{1}() . (k + 1),p . k,p . (k + 1)] ) )
and

A3: ex p being FinSequence st

( F_{3}() = p . (len p) & len p = len F_{1}() & p . 1 = F_{1}() . 1 & ( for k being Nat st 1 <= k & k < len F_{1}() holds

P_{1}[F_{1}() . (k + 1),p . k,p . (k + 1)] ) )

for x, y1, y2, z being set st 1 <= k & k < len F

y1 = y2 and

A2: ex p being FinSequence st

( F

P

A3: ex p being FinSequence st

( F

P

proof end;

scheme :: RECDEF_1:sch 10

LambdaSeqBinOpUn{ F_{1}() -> FinSequence, F_{2}( object , object ) -> object , F_{3}() -> object , F_{4}() -> object } :

provided

LambdaSeqBinOpUn{ F

provided

A1:
ex p being FinSequence st

( F_{3}() = p . (len p) & len p = len F_{1}() & p . 1 = F_{1}() . 1 & ( for k being Nat st 1 <= k & k < len F_{1}() holds

p . (k + 1) = F_{2}((F_{1}() . (k + 1)),(p . k)) ) )
and

A2: ex p being FinSequence st

( F_{4}() = p . (len p) & len p = len F_{1}() & p . 1 = F_{1}() . 1 & ( for k being Nat st 1 <= k & k < len F_{1}() holds

p . (k + 1) = F_{2}((F_{1}() . (k + 1)),(p . k)) ) )

( F

p . (k + 1) = F

A2: ex p being FinSequence st

( F

p . (k + 1) = F

proof end;

:: Schemes of definitness

scheme :: RECDEF_1:sch 11

DefRec{ F_{1}() -> object , F_{2}() -> Nat, P_{1}[ object , object , object ] } :

DefRec{ F

( ex y being set ex f being Function st

( y = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds P_{1}[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being set st ex f being Function st

( y1 = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds P_{1}[n,f . n,f . (n + 1)] ) ) & ex f being Function st

( y2 = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds P_{1}[n,f . n,f . (n + 1)] ) ) holds

y1 = y2 ) )

provided( y = f . F

( y1 = f . F

( y2 = f . F

y1 = y2 ) )

A1:
for n being Nat

for x being set ex y being set st P_{1}[n,x,y]
and

A2: for n being Nat

for x, y1, y2 being set st P_{1}[n,x,y1] & P_{1}[n,x,y2] holds

y1 = y2

for x being set ex y being set st P

A2: for n being Nat

for x, y1, y2 being set st P

y1 = y2

proof end;

scheme :: RECDEF_1:sch 12

LambdaDefRec{ F_{1}() -> object , F_{2}() -> Nat, F_{3}( object , object ) -> set } :

LambdaDefRec{ F

( ex y being set ex f being Function st

( y = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds f . (n + 1) = F_{3}(n,(f . n)) ) ) & ( for y1, y2 being set st ex f being Function st

( y1 = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds f . (n + 1) = F_{3}(n,(f . n)) ) ) & ex f being Function st

( y2 = f . F_{2}() & dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds f . (n + 1) = F_{3}(n,(f . n)) ) ) holds

y1 = y2 ) )

( y = f . F

( y1 = f . F

( y2 = f . F

y1 = y2 ) )

proof end;

scheme :: RECDEF_1:sch 13

DefRecD{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}() -> Nat, P_{1}[ object , object , object ] } :

DefRecD{ F

( ex y being Element of F_{1}() ex f being sequence of F_{1}() st

( y = f . F_{3}() & f . 0 = F_{2}() & ( for n being Nat holds P_{1}[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being Element of F_{1}() st ex f being sequence of F_{1}() st

( y1 = f . F_{3}() & f . 0 = F_{2}() & ( for n being Nat holds P_{1}[n,f . n,f . (n + 1)] ) ) & ex f being sequence of F_{1}() st

( y2 = f . F_{3}() & f . 0 = F_{2}() & ( for n being Nat holds P_{1}[n,f . n,f . (n + 1)] ) ) holds

y1 = y2 ) )

provided( y = f . F

( y1 = f . F

( y2 = f . F

y1 = y2 ) )

A1:
for n being Nat

for x being Element of F_{1}() ex y being Element of F_{1}() st P_{1}[n,x,y]
and

A2: for n being Nat

for x, y1, y2 being Element of F_{1}() st P_{1}[n,x,y1] & P_{1}[n,x,y2] holds

y1 = y2

for x being Element of F

A2: for n being Nat

for x, y1, y2 being Element of F

y1 = y2

proof end;

scheme :: RECDEF_1:sch 14

LambdaDefRecD{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}() -> Nat, F_{4}( object , object ) -> Element of F_{1}() } :

LambdaDefRecD{ F

( ex y being Element of F_{1}() ex f being sequence of F_{1}() st

( y = f . F_{3}() & f . 0 = F_{2}() & ( for n being Nat holds f . (n + 1) = F_{4}(n,(f . n)) ) ) & ( for y1, y2 being Element of F_{1}() st ex f being sequence of F_{1}() st

( y1 = f . F_{3}() & f . 0 = F_{2}() & ( for n being Nat holds f . (n + 1) = F_{4}(n,(f . n)) ) ) & ex f being sequence of F_{1}() st

( y2 = f . F_{3}() & f . 0 = F_{2}() & ( for n being Nat holds f . (n + 1) = F_{4}(n,(f . n)) ) ) holds

y1 = y2 ) )

( y = f . F

( y1 = f . F

( y2 = f . F

y1 = y2 ) )

proof end;

scheme :: RECDEF_1:sch 15

SeqBinOpDef{ F_{1}() -> FinSequence, P_{1}[ object , object , object ] } :

SeqBinOpDef{ F

( ex x being set ex p being FinSequence st

( x = p . (len p) & len p = len F_{1}() & p . 1 = F_{1}() . 1 & ( for k being Nat st 1 <= k & k < len F_{1}() holds

P_{1}[F_{1}() . (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_{1}() & p . 1 = F_{1}() . 1 & ( for k being Nat st 1 <= k & k < len F_{1}() holds

P_{1}[F_{1}() . (k + 1),p . k,p . (k + 1)] ) ) & ex p being FinSequence st

( y = p . (len p) & len p = len F_{1}() & p . 1 = F_{1}() . 1 & ( for k being Nat st 1 <= k & k < len F_{1}() holds

P_{1}[F_{1}() . (k + 1),p . k,p . (k + 1)] ) ) holds

x = y ) )

provided( x = p . (len p) & len p = len F

P

( x = p . (len p) & len p = len F

P

( y = p . (len p) & len p = len F

P

x = y ) )

A1:
for k being Nat

for y being set st 1 <= k & k < len F_{1}() holds

ex z being set st P_{1}[F_{1}() . (k + 1),y,z]
and

A2: for k being Nat

for x, y1, y2, z being set st 1 <= k & k < len F_{1}() & z = F_{1}() . (k + 1) & P_{1}[z,x,y1] & P_{1}[z,x,y2] holds

y1 = y2

for y being set st 1 <= k & k < len F

ex z being set st P

A2: for k being Nat

for x, y1, y2, z being set st 1 <= k & k < len F

y1 = y2

proof end;

scheme :: RECDEF_1:sch 16

LambdaSeqBinOpDef{ F_{1}() -> FinSequence, F_{2}( object , object ) -> set } :

LambdaSeqBinOpDef{ F

( ex x being set ex p being FinSequence st

( x = p . (len p) & len p = len F_{1}() & p . 1 = F_{1}() . 1 & ( for k being Nat st 1 <= k & k < len F_{1}() holds

p . (k + 1) = F_{2}((F_{1}() . (k + 1)),(p . k)) ) ) & ( for x, y being set st ex p being FinSequence st

( x = p . (len p) & len p = len F_{1}() & p . 1 = F_{1}() . 1 & ( for k being Nat st 1 <= k & k < len F_{1}() holds

p . (k + 1) = F_{2}((F_{1}() . (k + 1)),(p . k)) ) ) & ex p being FinSequence st

( y = p . (len p) & len p = len F_{1}() & p . 1 = F_{1}() . 1 & ( for k being Nat st 1 <= k & k < len F_{1}() holds

p . (k + 1) = F_{2}((F_{1}() . (k + 1)),(p . k)) ) ) holds

x = y ) )

( x = p . (len p) & len p = len F

p . (k + 1) = F

( x = p . (len p) & len p = len F

p . (k + 1) = F

( y = p . (len p) & len p = len F

p . (k + 1) = F

x = y ) )

proof end;

:: from POLYNOM2, 2010.02.13, A.T.

scheme :: RECDEF_1:sch 18

FinRecExD2{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}() -> Element of NAT , P_{1}[ object , object , object ] } :

FinRecExD2{ F

ex p being FinSequence of F_{1}() st

( len p = F_{3}() & ( p /. 1 = F_{2}() or F_{3}() = 0 ) & ( for n being Nat st 1 <= n & n <= F_{3}() - 1 holds

P_{1}[n,p /. n,p /. (n + 1)] ) )

provided( len p = F

P

A1:
for n being Nat st 1 <= n & n <= F_{3}() - 1 holds

for x being Element of F_{1}() ex y being Element of F_{1}() st P_{1}[n,x,y]

for x being Element of F

proof end;