Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Recursive Definitions

by
Krzysztof Hryniewiecki

MML identifier: RECDEF_1
[ Mizar article, MML identifier index ]

```environ

vocabulary FINSEQ_1, FUNCT_1, RELAT_1, PARTFUN1, TARSKI, ARYTM_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, REAL_1,
NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCT_2, DOMAIN_1;
constructors REAL_1, NAT_1, FINSEQ_1, FUNCT_2, DOMAIN_1, XREAL_0, MEMBERED,
XBOOLE_0;
clusters FUNCT_1, RELSET_1, FINSEQ_1, SUBSET_1, ARYTM_3, MEMBERED, ZFMISC_1,
XBOOLE_0, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin

reserve n,m,k for Nat,
D for non empty set,
Z,x,y,z,y1,y2 for set,
p,q for FinSequence;

definition let D be set, p be PartFunc of D,NAT; let n be Element of D;
redefine func p.n -> Nat;
end;

::::::::::::::::::::::::::::::::::::::::
::       Schemes of existence         ::
::::::::::::::::::::::::::::::::::::::::

scheme RecEx{A() -> set,P[set,set,set]}:
ex f being Function st dom f = NAT & f.0 = A() &
for n being Element of NAT holds P[n,f.n,f.(n+1)]
provided
for n being Nat for x being set
ex y being set st P[n,x,y] and
for n being Nat for x,y1,y2 being set
st P[n,x,y1] & P[n,x,y2] holds y1=y2;

scheme RecExD{D()->non empty set,A() -> Element of D(),
P[set,set,set]}:
ex f being Function of NAT,D() st
f.0 = A() &
for n being Element of NAT holds P[n,f.n,f.(n+1)]
provided
for n being Nat for x being Element of D()
ex y being Element of D() st P[n,x,y];

scheme LambdaRecEx{A() -> set,G(set,set) -> set}:
ex f being Function st dom f = NAT &
f.0 = A() & for n being Element of NAT holds f.(n+1) = G(n,f.n);

scheme LambdaRecExD{D() -> non empty set, A() -> Element of D(),
G(set,set) -> Element of D()}:
ex f being Function of NAT,D() st
f.0 = A() & for n being Element of NAT holds f.(n+1) = G(n,f.n);

scheme FinRecEx{A() -> set,N() -> Nat,P[set,set,set]}:
ex p being FinSequence st len p = N() & (p.1 = A() or N() = 0) &
for n st 1 <= n & n < N() holds P[n,p.n,p.(n+1)]
provided
for n being Nat st 1 <= n & n < N()
for x being set ex y being set st P[n,x,y] and
for n being Nat st 1 <= n & n < N()
for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2;

scheme FinRecExD{D() -> non empty set,A() -> Element of D(),
N() -> Nat, P[set,set,set]}:
ex p being FinSequence of D() st len p = N() & (p.1 = A() or N() = 0) &
for n st 1 <= n & n < N() holds P[n,p.n,p.(n+1)]
provided
for n being Nat st 1 <= n & n < N() holds for x being Element of D()
ex y being Element of D() st P[n,x,y];

scheme SeqBinOpEx{S() -> FinSequence,P[set,set,set]}:
ex x st ex p being FinSequence st x = p.(len p) & len p = len S() &
p.1 = S().1 & for k st 1 <= k & k < len S() holds
P[S().(k+1),p.k,p.(k+1)]
provided
for k,x st 1 <= k & k < len S() ex y st P[S().(k+1),x,y] and
for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) &
P[z,x,y1] & P[z,x,y2] holds y1 = y2;

scheme LambdaSeqBinOpEx{S() -> FinSequence,F(set,set) -> set}:
ex x st ex p being FinSequence st x = p.(len p) & len p = len S() &
p.1 = S().1 & for k st 1 <= k & k < len S()
holds p.(k+1) = F(S().(k+1),p.k);

::::::::::::::::::::::::::::::::::::::
::     Schemes of uniqueness        ::
::::::::::::::::::::::::::::::::::::::

scheme RecUn{A() -> set, F, G() -> Function, P[set,set,set]}:
F() = G()
provided
dom F() = NAT & F().0 = A() & for n holds P[n,F().n,F().(n+1)] and
dom G() = NAT & G().0 = A() & for n holds P[n,G().n,G().(n+1)] and
for n for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2;

scheme RecUnD{D() -> non empty set,A() -> Element of D(),
P[set,set,set], F, G() -> Function of NAT,D()} : F() = G()
provided
F().0 = A() & (for n holds P[n,F().n,F().(n+1)]) and
G().0 = A() & (for n holds P[n,G().n,G().(n+1)]) and
for n being Nat,x,y1,y2 being Element of D()
st P[n,x,y1] & P[n,x,y2] holds y1=y2;

scheme LambdaRecUn{A() -> set, RecFun(set,set) -> set,
F, G() -> Function}:
F() = G()
provided
dom F() = NAT & F().0 = A() &
for n holds F().(n+1) = RecFun(n,F().n) and
dom G() = NAT & G().0 = A() &
for n holds G().(n+1) = RecFun(n,G().n);

scheme LambdaRecUnD{D() -> non empty set,A() -> Element of D(),
RecFun(set,set) -> Element of D(),
F, G() -> Function of NAT,D()}:
F() = G()
provided
F().0 = A() & for n holds F().(n+1) = RecFun(n,F().n) and
G().0 = A() & for n holds G().(n+1) = RecFun(n,G().n);

scheme LambdaRecUnR{A() -> Real, RecFun(set,set) -> set,
F, G() -> Function of NAT,REAL}:
F() = G()
provided
F().0 = A() & for n holds F().(n+1) = RecFun(n,F().n) and
G().0 = A() & for n holds G().(n+1) = RecFun(n,G().n);

scheme FinRecUn{A() -> set,N() -> Nat,
F, G() -> FinSequence, P[set,set,set]}:
F() = G()
provided
for n st 1 <= n & n < N()
for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2 and
len F() = N() & (F().1 = A() or N() = 0) &
for n st 1 <= n & n < N() holds P[n,F().n,F().(n+1)] and
len G() = N() & (G().1 = A() or N() = 0) &
for n st 1 <= n & n < N() holds P[n,G().n,G().(n+1)];

scheme FinRecUnD{D() -> non empty set, A() -> Element of D(), N() -> Nat,
F, G() -> FinSequence of D(), P[set,set,set]}:
F() = G()
provided
for n st 1 <= n & n < N()
for x,y1,y2 being Element of D()
st P[n,x,y1] & P[n,x,y2] holds y1 = y2 and
len F() = N() & (F().1 = A() or N() = 0) &
for n st 1 <= n & n < N() holds P[n,F().n,F().(n+1)] and
len G() = N() & (G().1 = A() or N() = 0) &
for n st 1 <= n & n < N() holds P[n,G().n,G().(n+1)];

scheme SeqBinOpUn{S() -> FinSequence,P[set,set,set],x, y() -> set}:
x() = y()
provided
for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) &
P[z,x,y1] & P[z,x,y2] holds y1 = y2 and
ex p being FinSequence st x() = p.(len p) & len p = len S() & p.1 = S().1 &
for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)] and
ex p being FinSequence st y() = p.(len p) & len p = len S() & p.1 = S().1 &
for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)];

scheme LambdaSeqBinOpUn{S() -> FinSequence, F(set,set) -> set,
x, y() -> set}:
x() = y()
provided
ex p being FinSequence st x() = p.(len p) & len p = len S() & p.1 = S().1 &
for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k)
and
ex p being FinSequence st y() = p.(len p) & len p = len S() & p.1 = S().1 &
for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k);
:::::::::::::::::::::::::::::::
::   Schemes of definitness  ::
:::::::::::::::::::::::::::::::

scheme DefRec{A() -> set,n() -> Nat,P[set,set,set]}:
(ex y being set st ex f being Function st
y = f.n() & dom f = NAT & f.0 = A() &
for n holds P[n,f.n,f.(n+1)]) &
for y1,y2 being set st
(ex f being Function st
y1 = f.n() & dom f = NAT & f.0 = A() & for n holds P[n,f.n,f.(n+1)]) &
(ex f being Function st
y2 = f.n() & dom f = NAT & f.0 = A() & for n holds P[n,f.n,f.(n+1)])
holds y1 = y2
provided

for n,x ex y st P[n,x,y] and
for n,x,y1,y2 st P[n,x,y1] & P[n,x,y2] holds y1 = y2;

scheme LambdaDefRec{A() -> set,n() -> Nat,RecFun(set,set) -> set}:
(ex y being set st ex f being Function st
y = f.n() & dom f = NAT & f.0 = A() &
for n holds f.(n+1) = RecFun(n,f.n)) &
for y1,y2 being set st
(ex f being Function st
y1 = f.n() & dom f = NAT & f.0 = A() &
for n holds f.(n+1) = RecFun(n,f.n)) &
(ex f being Function st
y2 = f.n() & dom f = NAT & f.0 = A() &
for n holds f.(n+1) = RecFun(n,f.n))
holds y1 = y2;

scheme DefRecD{D() -> non empty set,A() -> (Element of D()),
n() -> Nat,P[set,set,set]}:
(ex y being Element of D() st ex f being Function of NAT,D() st
y = f.n() & f.0 = A() &
for n holds P[n,f.n,f.(n+1)]) &
for y1,y2 being Element of D() st
(ex f being Function of NAT,D() st
y1 = f.n() & f.0 = A() & for n holds P[n,f.n,f.(n+1)]) &
(ex f being Function of NAT,D() st
y2 = f.n() & f.0 = A() & for n holds P[n,f.n,f.(n+1)])
holds y1 = y2
provided
for n being Nat,x being Element of D()
ex y being Element of D() st P[n,x,y] and
for n being Nat, x,y1,y2 being Element of D()
st P[n,x,y1] & P[n,x,y2] holds y1 = y2;

scheme LambdaDefRecD{D() -> non empty set, A() -> Element of D(),
n() -> Nat, RecFun(set,set) -> Element of D()}:
(ex y being Element of D() st ex f being Function of NAT,D() st
y = f.n() & f.0 = A() &
for n being Nat holds f.(n+1) = RecFun(n,f.n)) &
for y1,y2 being Element of D() st
(ex f being Function of NAT,D() st
y1 = f.n() & f.0 = A() &
for n being Nat holds f.(n+1) = RecFun(n,f.n)) &
(ex f being Function of NAT,D() st
y2 = f.n() & f.0 = A() &
for n being Nat holds f.(n+1) = RecFun(n,f.n))
holds y1 = y2;

scheme SeqBinOpDef{S() -> FinSequence,P[set,set,set]}:
(ex x st ex p being FinSequence st x = p.(len p) & len p = len S() &
p.1 = S().1 & for k st 1 <= k & k < len S() holds
P[S().(k+1),p.k,p.(k+1)]) &
for x,y st
(ex p being FinSequence st x = p.(len p) & len p = len S() &
p.1 = S().1 & for k st 1 <= k & k < len S() holds
P[S().(k+1),p.k,p.(k+1)]) &
(ex p being FinSequence st y = p.(len p) & len p = len S() &
p.1 = S().1 & for k st 1 <= k & k < len S() holds
P[S().(k+1),p.k,p.(k+1)])
holds x = y
provided
for k,y st 1 <= k & k < len S() ex z st P[S().(k+1),y,z] and
for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) &
P[z,x,y1] & P[z,x,y2] holds y1 = y2;

scheme LambdaSeqBinOpDef{S() -> FinSequence,F(set,set) -> set}:
(ex x st ex p being FinSequence st x = p.(len p) & len p = len S() &
p.1 = S().1 & for k st 1 <= k & k < len S()
holds p.(k+1) = F(S().(k+1),p.k)) &
for x,y st
(ex p being FinSequence st x = p.(len p) & len p = len S() &
p.1 = S().1 & for k st 1 <= k & k < len S()
holds p.(k+1) = F(S().(k+1),p.k)) &
(ex p being FinSequence st y = p.(len p) & len p = len S() &
p.1 = S().1 & for k st 1 <= k & k < len S()
holds p.(k+1) = F(S().(k+1),p.k))
holds x = y;
```