:: Recursive Definitions
::  by Krzysztof Hryniewiecki
::
:: Received September 4, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, XBOOLE_0, FINSEQ_1, XXREAL_0, FUNCT_1,
      RELAT_1, TARSKI, VALUED_0, CARD_1, ARYTM_3, ORDINAL1, CLASSES1, ZFMISC_1,
      ORDINAL2, FUNCOP_1, MCART_1, NAT_1, ORDINAL4, ARYTM_1, REAL_1, PARTFUN1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, SUBSET_1, ORDINAL1,
      XXREAL_0, XCMPLX_0, XREAL_0, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCOP_1,
      ORDINAL2, NUMBERS, CLASSES1, FINSEQ_1, FUNCT_2, BINOP_1, DOMAIN_1,
      VALUED_0;
 constructors BINOP_1, DOMAIN_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, FINSEQ_1,
      VALUED_0, CLASSES1, ORDINAL2, RELSET_1, XTUPLE_0, XREAL_0;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, RELSET_1,
      FINSEQ_1, VALUED_0, XTUPLE_0;
 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 p be natural-valued Function;
  let n be set;
  redefine func p.n -> Element of NAT;
end;

::       Schemes of existence

scheme :: RECDEF_1:sch 1
  RecEx{A() -> object,P[object,object,object]}:
 ex f being Function st dom f = NAT & f.0 =
  A() & for n being 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 ];

scheme :: RECDEF_1:sch 2
  RecExD{D()->non empty set,A() -> Element of D(), P[object,object,object]}:
  ex f being sequence of D() st f.0 = A() &
  for n being 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 :: RECDEF_1:sch 3
  FinRecEx{A() -> object,N() -> Nat,P[object,object,object]}:
  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];

scheme :: RECDEF_1:sch 4
  FinRecExD{D() -> non empty set,A() -> Element of D(), N() -> Nat,
     P[object,object,object]}:
 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() for x being Element
of D() ex y being Element of D() st P[n,x,y];

scheme :: RECDEF_1:sch 5
  SeqBinOpEx{S() -> FinSequence,P[object,object,object]}:
  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];

scheme :: RECDEF_1:sch 6
  LambdaSeqBinOpEx{S() -> FinSequence,F(object,object) -> 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 :: RECDEF_1:sch 7
  FinRecUn{A() -> object, N() -> Nat, F,G() -> FinSequence,
  P[object,object,object]}:
  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 :: RECDEF_1:sch 8
  FinRecUnD{D() -> non empty set, A() -> Element of D(), N() -> Nat, F, G() ->
  FinSequence of D(), P[object,object,object]}: 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 :: RECDEF_1:sch 9
  SeqBinOpUn{S() -> FinSequence,P[object,object,object], x,y() -> object}:
  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 :: RECDEF_1:sch 10
  LambdaSeqBinOpUn{S() -> FinSequence, F(object,object) -> object,
  x, y() -> object}:
  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 :: RECDEF_1:sch 11
  DefRec{A() -> object,n() -> Nat,P[object,object,object]}:
  (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 :: RECDEF_1:sch 12
  LambdaDefRec{A() -> object,n() -> Nat,RecFun(object,object) -> 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 :: RECDEF_1:sch 13
  DefRecD{D() -> non empty set,A() -> (Element of D()), n() -> Nat,
  P[object,object,object]}:
  (ex y being Element of D() st ex f being sequence of 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 sequence of D() st y1 = f.n() & f.0 = A() & for n holds P[n,
f.n,f.(n+1)]) & (ex f being sequence of 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 :: RECDEF_1:sch 14
  LambdaDefRecD{D() -> non empty set, A() -> Element of D(), n() -> Nat,
  RecFun(object,object) -> Element of D()}:
  (ex y being Element of D() st ex f being
sequence of 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 sequence of
D() st y1 = f.n() & f.0 = A() & for n being Nat holds f.(n+1) = RecFun(n,f.n))
  & (ex f being sequence of D() st y2 = f.n() & f.0 = A() & for n being Nat
  holds f.(n+1) = RecFun(n,f.n)) holds y1 = y2;

scheme :: RECDEF_1:sch 15
  SeqBinOpDef{S() -> FinSequence,P[object,object,object]}:
  (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 :: RECDEF_1:sch 16
  LambdaSeqBinOpDef{S() -> FinSequence,F(object,object) -> 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;

:: from POLYNOM2, 2010.02.13, A.T.

scheme :: RECDEF_1:sch 17
  SeqExD{D() -> non empty set, N() -> Nat, P[object,object]}: ex p being
FinSequence of D() st dom p = Seg N() & for k being Nat st k in Seg
  N() holds P[k,p/.k]
provided
 for k being Nat st k in Seg N() ex x being Element of D()
st P[k,x];

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