:: Recursive Definitions. {P}art {II}
::  by Artur Korni{\l}owicz
::
:: Received February 10, 2004
:: Copyright (c) 2004-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, ZFMISC_1, XBOOLE_0, SUBSET_1, FUNCT_1, RELAT_1, FUNCT_4,
      TARSKI, CARD_1, ARYTM_3, MCART_1, NAT_1, ARYTM_1, XXREAL_0, FUNCT_7,
      RECDEF_2, XTUPLE_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, MCART_1, DOMAIN_1,
      ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, NAT_D, RELAT_1, FUNCT_1, FUNCT_2,
      FUNCT_4, FUNCT_7, XXREAL_0;
 constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, INT_1, BINARITH, FUNCT_7,
      NAT_D, RELSET_1, XTUPLE_0;
 registrations SUBSET_1, ORDINAL1, RELSET_1, XREAL_0, NAT_1, INT_1, XTUPLE_0;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;


begin

reserve a,b,c,d,e,z for object, A,B,C,D,E for set;

:: Projections

definition
  let x be triple object;
  redefine func x`1_3 means
:: RECDEF_2:def 1

  for y1,y2,y3 being object holds x = [y1,y2,y3] implies
  it = y1;
  redefine func x`2_3 means
:: RECDEF_2:def 2

  for y1,y2,y3 being object holds x = [y1,y2,y3] implies
  it = y2;
  redefine func x`3_3 means
:: RECDEF_2:def 3

  for y1,y2,y3 being object holds x = [y1,y2,y3] implies
  it = y3;
end;

::$CT

theorem :: RECDEF_2:2
  z in [:A,B,C:] implies z`1_3 in A & z`2_3 in B & z`3_3 in C;

theorem :: RECDEF_2:3
  z in [:A,B,C:] implies z = [ z`1_3, z`2_3, z`3_3 ];

definition
  let x be quadruple object;
  redefine func x`1_4 means
:: RECDEF_2:def 4

  for y1,y2,y3,y4 being object holds x = [y1,y2,y3,y4]
  implies it = y1;
  redefine func x`2_4 means
:: RECDEF_2:def 5

  for y1,y2,y3,y4 being object holds x = [y1,y2,y3,y4]
  implies it = y2;
  redefine func x`3_4 means
:: RECDEF_2:def 6

  for y1,y2,y3,y4 being object holds x = [y1,y2,y3,y4]
  implies it = y3;
  redefine func x`4_4 means
:: RECDEF_2:def 7

  for y1,y2,y3,y4 being object holds x = [y1,y2,y3,y4]
  implies it = y4;
end;

::$CT

theorem :: RECDEF_2:5
  z in [:A,B,C,D:] implies z`1_4 in A & z`2_4 in B & z`3_4 in C & z`4_4 in D;

theorem :: RECDEF_2:6
  z in [:A,B,C,D:] implies z = [ z`1_4, z`2_4, z`3_4, z`4_4 ];

definition
::$CD 5
end;

::$CT 3

:: Conditional schemes

scheme :: RECDEF_2:sch 1
  ExFunc3Cond { C() -> set, P,Q,R[object], F,G,H(object) -> object }:
 ex f being
Function st dom f = C() & for c being set st c in C() holds (P[c] implies f.c =
  F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c))
provided
 for c being set st c in C() holds (P[c] implies not Q[c]) & (P[c]
implies not R[c]) & (Q[c] implies not R[c]) and
 for c being set st c in C() holds P[c] or Q[c] or R[c];

scheme :: RECDEF_2:sch 2
  ExFunc4Cond { C() -> set, P,Q,R,S[object], F,G,H,I(object) -> object }:
 ex f being
Function st dom f = C() & for c being set st c in C() holds (P[c] implies f.c =
F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c)) & (S[c] implies f
  .c = I(c))
provided
 for c being set st c in C() holds (P[c] implies not Q[c]) & (P[c]
implies not R[c]) & (P[c] implies not S[c]) & (Q[c] implies not R[c]) & (Q[c]
implies not S[c]) & (R[c] implies not S[c]) and
 for c being set st c in C() holds P[c] or Q[c] or R[c] or S[c];

:: 1 step

scheme :: RECDEF_2:sch 3
 DoubleChoiceRec { A, B() -> non empty set, A0() -> Element of
  A(), B0() -> Element of B(), P[object,object,object,object,object] }:
ex f
  being sequence of A(), g being sequence of B() st f.0 = A0() & g.0 =
  B0() & for n being Nat holds P[n,f.n,g.n,f.(n+1),g.(n+1)] provided
   for n being Nat, x being Element of A(), y being Element of B()
  ex x1 being Element of A(), y1 being Element of B() st
  P[n,x,y,x1,y1];

:: 2 steps

scheme :: RECDEF_2:sch 4
  LambdaRec2Ex { A,B() -> set, F(object,object,object) -> object }:
ex f being Function st
dom f = NAT & f.0 = A() & f.1 = B() & for n being Nat holds f.(n+2)
  = F(n,f.n,f.(n+1));

scheme :: RECDEF_2:sch 5
  LambdaRec2ExD { X() -> non empty set, A,B() -> Element of X(),
  F(object,object,object) -> Element of X() }:
  ex f being sequence of X() st f.0 = A() & f.1 = B()
  & for n being Nat holds f.(n+2) = F(n,f.n,f.(n+1));

scheme :: RECDEF_2:sch 6
  LambdaRec2Un { A,B() -> object, F,G() -> Function,
  F(object,object,object) -> object }:
  F() = G()
provided
 dom F() = NAT and
 F().0 = A() & F().1 = B() and
 for n being Nat holds F().(n+2) = F(n,F().n,F().(n+1)) and
 dom G() = NAT and
 G().0 = A() & G().1 = B() and
 for n being Nat holds G().(n+2) = F(n,G().n,G().(n+1));

scheme :: RECDEF_2:sch 7
  LambdaRec2UnD { X() -> non empty set, A,B() -> Element of X(), F,G() ->
  sequence of X(), F(object,object,object) -> Element of X() }: F() = G()
provided
 F().0 = A() & F().1 = B() and
 for n being Nat holds F().(n+2) = F(n,F().n,F().(n+1)) and
 G().0 = A() & G().1 = B() and
 for n being Nat holds G().(n+2) = F(n,G().n,G().(n+1));

:: 3 steps

scheme :: RECDEF_2:sch 8
  LambdaRec3Ex { A,B,C() -> set, F(object,object,object,object) -> object }:
ex f being
  Function st dom f = NAT & f.0 = A() & f.1 = B() & f.2 = C() & for n being
  Nat holds f.(n+3) = F(n,f.n,f.(n+1),f.(n+2));

scheme :: RECDEF_2:sch 9
  LambdaRec3ExD { X() -> non empty set, A,B,C() -> Element of X(),
  F(object,object,object,object) -> Element of X() }:
  ex f being sequence of X() st f.0 = A() & f.1 = B() & f.2 = C() &
  for n being Nat holds f.(n+3) = F(n,f.n,f.(n+1),f.(n+2));

scheme :: RECDEF_2:sch 10
  LambdaRec3Un { A,B,C() -> object, F,G() -> Function,
  F(object,object,object,object) -> object }: F() = G()
provided
 dom F() = NAT and
 F().0 = A() & F().1 = B() & F().2 = C() and
 for n being Nat holds F().(n+3) = F(n,F().n,F().(n+1),F()
.(n+2)) and
 dom G() = NAT and
 G().0 = A() & G().1 = B() & G().2 = C() and
 for n being Nat holds G().(n+3) = F(n,G().n,G().(n+1),G()
.(n+2));

scheme :: RECDEF_2:sch 11
  LambdaRec3UnD { X() -> non empty set, A,B,C() -> Element of X(), F,G() ->
  sequence of X(), F(object,object,object,object) -> Element of X() }:
  F() = G()
provided
 F().0 = A() & F().1 = B() & F().2 = C() and
 for n being Nat holds F().(n+3) = F(n,F().n,F().(n+1),F()
.(n+2)) and
 G().0 = A() & G().1 = B() & G().2 = C() and
 for n being Nat holds G().(n+3) = F(n,G().n,G().(n+1),G()
.(n+2));

:: 4 steps

scheme :: RECDEF_2:sch 12
  LambdaRec4Un { A,B,C,D() -> object, F,G() -> Function,
  F(object,object,object,object,object) -> object }: F() = G()
provided
 dom F() = NAT and
 F().0 = A() & F().1 = B() & F().2 = C() & F().3 = D() and
 for n being Nat holds F().(n+4) = F(n,F().n,F().(n+1),F()
.(n+2),F().(n+3)) and
 dom G() = NAT and
 G().0 = A() & G().1 = B() & G().2 = C() & G().3 = D() and
 for n being Nat holds G().(n+4) = F(n,G().n,G().(n+1),G()
.(n+2),G().(n+3));

scheme :: RECDEF_2:sch 13
  LambdaRec4UnD { X() -> non empty set, A,B,C,D() -> Element of X(), F,G() ->
  sequence of X(), F(object,object,object,object,object) -> Element of X() }:
  F() = G()
provided
 F().0 = A() & F().1 = B() & F().2 = C() & F().3 = D() and
 for n being Nat holds F().(n+4) = F(n,F().n,F().(n+1),F()
.(n+2),F().(n+3)) and
 G().0 = A() & G().1 = B() & G().2 = C() & G().3 = D() and
 for n being Nat holds G().(n+4) = F(n,G().n,G().(n+1),G()
.(n+2),G().(n+3));

begin :: Addenda

:: 2010.05.120, A.T.

theorem :: RECDEF_2:10
 for x,y,X,Y,Z being set
  st x`1_3 = y`1_3 & x`2_3 = y`2_3 & x`3_3 = y`3_3 &
  y in [:X,Y,Z:] & x in [:X,Y,Z:]
     holds x = y;