:: Recursive Definitions. {P}art {II}
::  by Artur Korni{\l}owicz
::
:: Received February 10, 2004
:: Copyright (c) 2004-2012 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,
      NUMBERS, XCMPLX_0, ORDINAL1, 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;
 definitions TARSKI, XBOOLE_0, XTUPLE_0;
 theorems MCART_1, NAT_1, FUNCT_1, FUNCT_2, RELSET_1, INT_1, FUNCT_4, XBOOLE_0,
      XBOOLE_1, DOMAIN_1, FUNCT_7, XREAL_1, XXREAL_0, XREAL_0, NAT_D, XTUPLE_0;
 schemes NAT_1, RECDEF_1, FUNCT_1, XBOOLE_0, PARTFUN1;

begin

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

:: Projections

definition
  let x be triple set;
  consider x1,x2,x3 being set such that
A1: x = [x1,x2,x3] by XTUPLE_0:def 5;
A2: [x1,x2,x3]`1_3 = x1;
A3: [x1,x2,x3]`2_3 = x2;
A4: [x1,x2,x3]`3_3 = x3;
  redefine func x`1_3 means
  :Def1:
  for y1,y2,y3 being set holds x = [y1,y2,y3] implies
  it = y1;
  compatibility by A1,A2,XTUPLE_0:3;
  redefine func x`2_3 means
  :Def2:
  for y1,y2,y3 being set holds x = [y1,y2,y3] implies
  it = y2;
  compatibility by A1,A3,XTUPLE_0:3;
  redefine func x`3_3 means
  :Def3:
  for y1,y2,y3 being set holds x = [y1,y2,y3] implies
  it = y3;
  compatibility by A1,A4,XTUPLE_0:3;
end;

theorem Th1:
  (ex a,b,c st z = [a,b,c]) implies z = [ z`1_3, z`2_3, z`3_3 ]
proof
  given a,b,c such that
A1: z = [a,b,c];
  z`1_3 = a & z`2_3 = b by A1,Def1,Def2;
  hence thesis by A1,Def3;
end;

theorem
  z in [:A,B,C:] implies z`1_3 in A & z`2_3 in B & z`3_3 in C
proof
  assume
A1: z in [:A,B,C:];
  then
A2: C is non empty by MCART_1:31;
A3: A is non empty & B is non empty by A1,MCART_1:31;
  then consider
  a being Element of A, b being Element of B, c being Element of C
  such that
A4: z = [a,b,c] by A1,A2,DOMAIN_1:3;
A5: z`3_3 = c by A4,Def3;
  z`1_3 = a & z`2_3 = b by A4,Def1,Def2;
  hence thesis by A3,A2,A5;
end;

theorem Th3:
  z in [:A,B,C:] implies z = [ z`1_3, z`2_3, z`3_3 ]
proof
  assume
A1: z in [:A,B,C:];
  then
A2: C is non empty by MCART_1:31;
  A is non empty & B is non empty by A1,MCART_1:31;
  then
  ex a being Element of A, b being Element of B, c being Element of C st z
  = [a,b,c] by A1,A2,DOMAIN_1:3;
  hence thesis by Th1;
end;

definition
  let x be quadruple set;
  consider x1,x2,x3,x4 being set such that
A1: x = [x1,x2,x3,x4] by XTUPLE_0:def 9;
A2: [x1,x2,x3,x4]`1_4 = x1;
A3: [x1,x2,x3,x4]`2_4 = x2;
A4: [x1,x2,x3,x4]`3_4 = x3;
A5: [x1,x2,x3,x4]`4_4 = x4;
  redefine func x`1_4 means
  :Def4:
  for y1,y2,y3,y4 being set holds x = [y1,y2,y3,y4]
  implies it = y1;
  compatibility by A1,A2,XTUPLE_0:5;
  redefine func x`2_4 means
  :Def5:
  for y1,y2,y3,y4 being set holds x = [y1,y2,y3,y4]
  implies it = y2;
  compatibility by A1,A3,XTUPLE_0:5;
  redefine func x`3_4 means
  :Def6:
  for y1,y2,y3,y4 being set holds x = [y1,y2,y3,y4]
  implies it = y3;
  compatibility by A1,A4,XTUPLE_0:5;
  redefine func x`4_4 means
  :Def7:
  for y1,y2,y3,y4 being set holds x = [y1,y2,y3,y4]
  implies it = y4;
  compatibility by A1,A5,XTUPLE_0:5;
end;

theorem Th4:
  (ex a,b,c,d st z = [a,b,c,d]) implies z = [ z`1_4, z`2_4, z`3_4,
  z`4_4 ]
proof
  given a,b,c,d such that
A1: z = [a,b,c,d];
A2: z`3_4 = c by A1,Def6;
  z`1_4 = a & z`2_4 = b by A1,Def4,Def5;
  hence thesis by A1,A2,Def7;
end;

theorem
  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
proof
  assume
A1: z in [:A,B,C,D:];
  then
A2: C is non empty & D is non empty by MCART_1:51;
A3: A is non empty & B is non empty by A1,MCART_1:51;
  then consider
  a being Element of A, b being Element of B, c being Element of C, d
  being Element of D such that
A4: z = [a,b,c,d] by A1,A2,DOMAIN_1:10;
A5: z`3_4 = c & z`4_4 = d by A4,Def6,Def7;
  z`1_4 = a & z`2_4 = b by A4,Def4,Def5;
  hence thesis by A3,A2,A5;
end;

theorem
  z in [:A,B,C,D:] implies z = [ z`1_4, z`2_4, z`3_4, z`4_4 ]
proof
  assume
A1: z in [:A,B,C,D:];
  then
A2: C is non empty & D is non empty by MCART_1:51;
  A is non empty & B is non empty by A1,MCART_1:51;
  then ex a being Element of A, b being Element of B, c being Element of C, d
  being Element of D st z = [a,b,c,d] by A1,A2,DOMAIN_1:10;
  hence thesis by Th4;
end;

definition
 canceled 5;
end;

canceled 3;

:: Conditional schemes

scheme
  ExFunc3Cond { C() -> set, P,Q,R[set], F,G,H(set) -> set }: 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
A1: 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
A2: for c being set st c in C() holds P[c] or Q[c] or R[c]
proof
  consider D1 being set such that
A3: for x being set holds x in D1 iff x in C() & P[x] from XBOOLE_0:sch
  1;
  consider D3 being set such that
A4: for x being set holds x in D3 iff x in C() & R[x] from XBOOLE_0:sch
  1;
  consider f1 being Function such that
A5: dom f1 = D1 and
A6: for x being set st x in D1 holds f1.x = F(x) from FUNCT_1:sch 3;
  consider D2 being set such that
A7: for x being set holds x in D2 iff x in C() & Q[x] from XBOOLE_0:sch
  1;
  consider f3 being Function such that
A8: dom f3 = D3 and
A9: for x being set st x in D3 holds f3.x = H(x) from FUNCT_1:sch 3;
  consider f2 being Function such that
A10: dom f2 = D2 and
A11: for x being set st x in D2 holds f2.x = G(x) from FUNCT_1:sch 3;
  set f = f1 +* f2 +* f3;
  take f;
A12: dom f = dom (f1 +* f2) \/ dom f3 by FUNCT_4:def 1
    .= dom f1 \/ dom f2 \/ dom f3 by FUNCT_4:def 1;
  thus dom f = C()
  proof
A13: D3 c= C()
    proof
      let x be set;
      thus thesis by A4;
    end;
A14: D2 c= C()
    proof
      let x be set;
      thus thesis by A7;
    end;
    D1 c= C()
    proof
      let x be set;
      thus thesis by A3;
    end;
    then D1 \/ D2 c= C() by A14,XBOOLE_1:8;
    hence dom f c= C() by A5,A10,A8,A12,A13,XBOOLE_1:8;
    let x be set;
    assume
A15: x in C();
    then P[x] or Q[x] or R[x] by A2;
    then x in D1 or x in D2 or x in D3 by A3,A7,A4,A15;
    then x in D1 \/ D2 or x in D3 by XBOOLE_0:def 3;
    hence thesis by A5,A10,A8,A12,XBOOLE_0:def 3;
  end;
  let c be set such that
A16: c in C();
  hereby
    assume
A17: P[c];
    not Q[c] by A1,A16,A17;
    then
A19: not c in D2 by A7;
    not R[c] by A1,A16,A17;
    then not c in D3 by A4;
    hence f.c = (f1 +* f2).c by A8,FUNCT_4:11
      .= f1.c by A10,A19,FUNCT_4:11
      .= F(c) by A6,A17,A3,A16;
  end;
  hereby
    assume
A20: Q[c];
    not R[c] by A1,A16,A20;
    then not c in D3 by A4;
    hence f.c = (f1 +* f2).c by A8,FUNCT_4:11
      .= f2.c by A10,A20,A7,A16,FUNCT_4:13
      .= G(c) by A11,A20,A7,A16;
  end;
  assume
Z:  R[c];
  hence f.c = f3.c by A8,A4,A16,FUNCT_4:13
    .= H(c) by A9,Z,A4,A16;
end;

scheme
  ExFunc4Cond { C() -> set, P,Q,R,S[set], F,G,H,I(set) -> set }: 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
A1: 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
A2: for c being set st c in C() holds P[c] or Q[c] or R[c] or S[c]
proof
  consider D1 being set such that
A3: for x being set holds x in D1 iff x in C() & P[x] from XBOOLE_0:sch
  1;
  consider D4 being set such that
A4: for x being set holds x in D4 iff x in C() & S[x] from XBOOLE_0:sch
  1;
  consider f1 being Function such that
A5: dom f1 = D1 and
A6: for x being set st x in D1 holds f1.x = F(x) from FUNCT_1:sch 3;
  consider D2 being set such that
A7: for x being set holds x in D2 iff x in C() & Q[x] from XBOOLE_0:sch
  1;
  consider f2 being Function such that
A8: dom f2 = D2 and
A9: for x being set st x in D2 holds f2.x = G(x) from FUNCT_1:sch 3;
  consider D3 being set such that
A10: for x being set holds x in D3 iff x in C() & R[x] from XBOOLE_0:sch
  1;
  consider f4 being Function such that
A11: dom f4 = D4 and
A12: for x being set st x in D4 holds f4.x = I(x) from FUNCT_1:sch 3;
  consider f3 being Function such that
A13: dom f3 = D3 and
A14: for x being set st x in D3 holds f3.x = H(x) from FUNCT_1:sch 3;
  set f = f1 +* f2 +* f3 +* f4;
  take f;
A15: dom f = dom (f1 +* f2 +* f3) \/ dom f4 by FUNCT_4:def 1
    .= dom (f1 +* f2) \/ dom f3 \/ dom f4 by FUNCT_4:def 1
    .= dom f1 \/ dom f2 \/ dom f3 \/ dom f4 by FUNCT_4:def 1;
  thus dom f = C()
  proof
A16: D4 c= C()
    proof
      let x be set;
      thus thesis by A4;
    end;
A17: D3 c= C()
    proof
      let x be set;
      thus thesis by A10;
    end;
A18: D2 c= C()
    proof
      let x be set;
      thus thesis by A7;
    end;
    D1 c= C()
    proof
      let x be set;
      thus thesis by A3;
    end;
    then D1 \/ D2 c= C() by A18,XBOOLE_1:8;
    then D1 \/ D2 \/ D3 c= C() by A17,XBOOLE_1:8;
    hence dom f c= C() by A5,A8,A13,A11,A15,A16,XBOOLE_1:8;
    let x be set;
    assume
A19: x in C();
    then P[x] or Q[x] or R[x] or S[x] by A2;
    then x in D1 or x in D2 or x in D3 or x in D4 by A3,A7,A10,A4,A19;
    then x in D1 \/ D2 or x in D3 or x in D4 by XBOOLE_0:def 3;
    then x in D1 \/ D2 \/ D3 or x in D4 by XBOOLE_0:def 3;
    hence thesis by A5,A8,A13,A11,A15,XBOOLE_0:def 3;
  end;
  let c be set such that
A20: c in C();
  hereby
    assume
A21: P[c];
    not R[c] by A1,A20,A21;
    then
A23: not c in D3 by A10;
    not Q[c] by A1,A20,A21;
    then
A24: not c in D2 by A7;
    not S[c] by A1,A20,A21;
    then not c in D4 by A4;
    hence f.c = (f1 +* f2 +* f3).c by A11,FUNCT_4:11
      .= (f1 +* f2).c by A13,A23,FUNCT_4:11
      .= f1.c by A8,A24,FUNCT_4:11
      .= F(c) by A6,A21,A3,A20;
  end;
  hereby
    assume
A25: Q[c];
    not R[c] by A1,A20,A25;
    then
A27: not c in D3 by A10;
    not S[c] by A1,A20,A25;
    then not c in D4 by A4;
    hence f.c = (f1 +* f2 +* f3).c by A11,FUNCT_4:11
      .= (f1 +* f2).c by A13,A27,FUNCT_4:11
      .= f2.c by A8,A25,A7,A20,FUNCT_4:13
      .= G(c) by A9,A25,A7,A20;
  end;
  hereby
    assume
A28: R[c];
    not S[c] by A1,A20,A28;
    then not c in D4 by A4;
    hence f.c = (f1 +* f2 +* f3).c by A11,FUNCT_4:11
      .= f3.c by A13,A28,A10,A20,FUNCT_4:13
      .= H(c) by A14,A28,A10,A20;
  end;
  assume
Z: S[c];
  hence f.c = f4.c by A11,A4,A20,FUNCT_4:13
    .= I(c) by A12,Z,A4,A20;
end;

:: 1 step

scheme
  DoubleChoiceRec { A, B() -> non empty set, A0() -> Element of A(), B0() ->
  Element of B(), P[set,set,set,set,set] }: ex f being Function of NAT, A(), g
being Function of NAT, B() st f.0 = A0() & g.0 = B0() & for n being Element of
  NAT holds P[n,f.n,g.n,f.(n+1),g.(n+1)]
provided
A1: for n being Element of 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]
proof
  defpred P1[set,set,set] means P[$1,($2)`1,($2)`2,($3)`1,($3)`2];
A2: for n being Element of NAT, x being Element of [:A(),B():] ex y being
  Element of [:A(),B():] st P1[n,x,y]
  proof
    let n be Element of NAT, x be Element of [:A(),B():];
    consider ai being Element of A(), bi being Element of B() such that
A3: P[n,x`1,x`2,ai,bi] by A1;
    take [ai,bi];
    thus thesis by A3;
  end;
  consider f being Function of NAT, [:A(),B():] such that
A4: f.0 = [A0(),B0()] and
A5: for e being Element of NAT holds P1[e,f.e,f.(e+1)] from RECDEF_1:sch
  2( A2);
  take pr1 f, pr2 f;
   [A0(),B0()]`1 = A0() & [A0(),B0()]`2 = B0();
  hence (pr1 f).0 = A0() & (pr2 f).0 = B0() by A4,FUNCT_2:def 5,def 6;
  let i be Element of NAT;
A6: (f.(i+1))`1 = (pr1 f).(i+1) & (f.(i+1))`2 = (pr2 f).(i+1) by FUNCT_2:def 5
,def 6;
  (f.i)`1 = (pr1 f).i & (f.i)`2 = (pr2 f).i by FUNCT_2:def 5,def 6;
  hence thesis by A5,A6;
end;

:: 2 steps

scheme
  LambdaRec2Ex { A,B() -> set, F(set,set,set) -> set }: ex f being Function st
dom f = NAT & f.0 = A() & f.1 = B() & for n being Element of NAT holds f.(n+2)
  = F(n,f.n,f.(n+1)) proof
  defpred C[set] means $1 = 0;
  deffunc G(Nat,set) = [$2`2_3, $2`3_3, F($1+1,$2`2_3,$2`3_3)];
  set r03 = F(0,A(),B());
  set r13 = F(1,B(),r03);
  deffunc H(Nat,set) = G($1+1,$2);
  consider h being Function such that
  dom h = NAT and
A1: h.0 = [ B(), r03, r13 ] and
A2: for n being Nat holds h.(n+1) = H(n,h.n) from NAT_1:sch 11;
  deffunc Y(Element of NAT) = h.($1-'1);
  deffunc X(set) = [ A(), B(), r03 ];
  consider g being Function such that
  dom g = NAT and
A3: for x being Element of NAT holds (C[x] implies g.x = X(x)) & (not C[
  x] implies g.x = Y(x)) from PARTFUN1:sch 4;
  deffunc M(set) = (g.$1)`1_3;
  consider f being Function such that
A4: dom f = NAT and
A5: for x being set st x in NAT holds f.x = M(x) from FUNCT_1:sch 3;
  defpred P[Element of NAT] means f.($1+2) = (g.($1+1))`2_3 & (g.($1+1))`1_3 =
(g.$1)`2_3 & (g.($1+2))`1_3 = (g.$1)`3_3 & (g.($1+2))`1_3 = (g.($1+1))`2_3 & (g
  .($1+2))`2_3 = (g.($1+1))`3_3 & f.($1+2) = F($1,f.$1,f.($1+1));
A6: g.0 = [ A(), B(), r03 ] by A3;
A7: for n being Element of NAT holds g.(n+2) = G(n+1,g.(n+1))
  proof
    let n be Element of NAT;
A8: n+2-1 = n+(2-1) & 0 <= n+1 by NAT_1:2;
A9: g.(n+1) = Y(n+1) by A3
      .= h.n by NAT_D:34;
    thus g.(n+2) = Y(n+2) by A3
      .= h.(n+1) by A8,XREAL_0:def 2
      .= G(n+1,g.(n+1)) by A2,A9;
  end;
  then
A10: (g.(0+2))`2_3 = G(0+1,g.(0+1))`2_3
    .= (g.(0+1))`3_3;
  take f;
  thus dom f = NAT by A4;
  thus
A11: f.0 = (g.0)`1_3 by A5
    .= A() by A6,Def1;
A12: g.1 = Y(1) by A3
    .= [ B(), r03, r13 ] by A1,XREAL_1:232;
  then
A13: (g.(0+1))`1_3 = B() by Def1
    .= (g.0)`2_3 by A6,Def2;
A14: for x being Element of NAT st P[x] holds P[x+1]
  proof
    let x be Element of NAT;
    assume
A15: P[x];
    then
A16: f.(x+1) = (g.x)`2_3 by A5;
    thus
A17: f.(x+1+2) = (g.(x+1+2))`1_3 by A5
      .= G(x+1+1,g.(x+1+1))`1_3 by A7
      .= (g.(x+1+1))`2_3;
    thus (g.(x+1+1))`1_3 = (g.(x+1))`2_3 by A15;
    thus (g.(x+1+2))`1_3 = G(x+1+1,g.(x+1+1))`1_3 by A7
      .= (g.(x+1))`3_3 by A15;
    hence (g.(x+1+2))`1_3 = (g.(x+1+1))`2_3 by A15;
    thus (g.(x+1+2))`2_3 = G(x+1+1,g.(x+1+1))`2_3 by A7
      .= (g.(x+1+1))`3_3;
    per cases;
    suppose
A18:  x = 0;
      hence f.(x+1+2) = (g.(1+2))`1_3 by A5
        .= G(1+1,g.(1+1))`1_3 by A7
        .= (g.(0+1))`3_3 by A15,A18
        .= r13 by A12,Def3
        .= F(0+1,B(),(g.0)`3_3) by A6,Def3
        .= F(x+1,f.(x+1),f.(x+1+1)) by A6,A15,A16,A18,Def2;
    end;
    suppose
      x <> 0;
      then 0 < x by NAT_1:3;
      then
A19:  0+1 <= x by NAT_1:13;
      then
A20:  x-'1+1 = x by XREAL_1:235;
      1-1 <= x-1 by A19,XREAL_1:13;
      then
A21:  x-1 = x-'1 by XREAL_0:def 2;
      x+1 = x-1+2;
      hence f.(x+1+2) = G(x-'1+1,g.(x-'1+1))`3_3 by A7,A15,A17,A21
        .= F(x+1,f.(x+1),f.(x+1+1)) by A15,A16,A20;
    end;
  end;
A22: f.(0+2) = (g.(0+2))`1_3 by A5
    .= G(0+1,g.(0+1))`1_3 by A7
    .= (g.(0+1))`2_3;
  thus
A23: f.1 = (g.1)`1_3 by A5
    .= B() by A12,Def1;
A24: (g.(0+2))`1_3 = G(0+1,g.(0+1))`1_3 by A7
    .= (g.1)`2_3
    .= r03 by A12,Def2
    .= (g.0)`3_3 by A6,Def3;
  then (g.(0+2))`1_3 = r03 by A6,Def3
    .= (g.(0+1))`2_3 by A12,Def2;
  then
A25: P[0] by A12,A11,A23,A22,A13,A24,A10,Def2;
  for x being Element of NAT holds P[x] from NAT_1:sch 1(A25,A14);
  hence thesis;
end;

scheme
  LambdaRec2ExD { X() -> non empty set, A,B() -> Element of X(), F(set,set,set
) -> Element of X() }: ex f being Function of NAT,X() st f.0 = A() & f.1 = B()
  & for n being Element of NAT holds f.(n+2) = F(n,f.n,f.(n+1)) proof
  consider f being Function such that
A1: dom f = NAT and
A2: f.0 = A() & f.1 = B() and
A3: for n being Element of NAT holds f.(n+2) = F(n,f.n,f.(n+1)) from
  LambdaRec2Ex;
  rng f c= X()
  proof
    let y be set;
    assume y in rng f;
    then consider n being set such that
A4: n in dom f and
A5: f.n = y by FUNCT_1:def 3;
    reconsider n as Element of NAT by A1,A4;
    per cases;
    suppose
      n <= 1;
      then n = 0 or n = 1 by NAT_1:25;
      hence thesis by A2,A5;
    end;
    suppose
      n > 1;
      then 1+1 <= n by NAT_1:13;
      then n-2 is Element of NAT by INT_1:5;
      then f.(n-2+2) = F(n-2,f.(n-2),f.(n-2+1)) by A3;
      hence thesis by A5;
    end;
  end;
  then f is Function of NAT,X() by A1,FUNCT_2:def 1,RELSET_1:4;
  hence thesis by A2,A3;
end;

scheme
  LambdaRec2Un { A,B() -> set, F,G() -> Function, F(set,set,set) -> set }: F()
  = G()
provided
A1: dom F() = NAT and
A2: F().0 = A() & F().1 = B() and
A3: for n being Element of NAT holds F().(n+2) = F(n,F().n,F().(n+1)) and
A4: dom G() = NAT and
A5: G().0 = A() & G().1 = B() and
A6: for n being Element of NAT holds G().(n+2) = F(n,G().n,G().(n+1))
proof
  defpred Q[Nat] means F().$1 <> G().$1;
  assume F() <> G();
  then ex x being set st x in NAT & F().x <> G().x by A1,A4,FUNCT_1:2;
  then
A7: ex k being Nat st Q[k];
  consider m being Nat such that
A8: Q[m] and
A9: for n being Nat st Q[n] holds m <= n from NAT_1:sch 5(A7);
  now
    set k = m-'2;
A10: F().(k+2) = F(k,F().k,F().(k+1)) & G().(k+2) = F(k,G().k,G().(k+1))
    by A3,A6;
    assume m <> 0 & m <> 1;
    then 2 <= m by NAT_1:26;
    then
A11: m = k+2 by XREAL_1:235;
    then
A12: F().(k+1) = G().(k+1) by A9,XREAL_1:6;
    k+0 < m by A11,XREAL_1:6;
    hence contradiction by A8,A9,A11,A12,A10;
  end;
  hence contradiction by A2,A5,A8;
end;

scheme
  LambdaRec2UnD { X() -> non empty set, A,B() -> Element of X(), F,G() ->
  Function of NAT,X(), F(set,set,set) -> Element of X() }: F() = G()
provided
A1: F().0 = A() & F().1 = B() and
A2: for n being Element of NAT holds F().(n+2) = F(n,F().n,F().(n+1)) and
A3: G().0 = A() & G().1 = B() and
A4: for n being Element of NAT holds G().(n+2) = F(n,G().n,G().(n+1))
proof
A5: dom G() = NAT by FUNCT_2:def 1;
A6: dom F() = NAT by FUNCT_2:def 1;
  thus F() = G() from LambdaRec2Un(A6,A1,A2,A5,A3,A4);
end;

:: 3 steps

scheme
  LambdaRec3Ex { A,B,C() -> set, F(set,set,set,set) -> set }: ex f being
  Function st dom f = NAT & f.0 = A() & f.1 = B() & f.2 = C() & for n being
  Element of NAT holds f.(n+3) = F(n,f.n,f.(n+1),f.(n+2)) proof
  defpred C3[set] means In($1,NAT) > 1;
  defpred C2[set] means $1 = 1;
  defpred C1[set] means $1 = 0;
  deffunc G(Nat,set) = [$2`2_4, $2`3_4, $2`4_4, F($1+1,$2`2_4,$2`3_4,$2`4_4)];
  set r04 = F(0,A(),B(),C());
  set r14 = F(1,B(),C(),r04);
  set r24 = F(2,C(),r04,r14);
  deffunc H(Nat,set) = G($1+2,$2);
  consider h being Function such that
  dom h = NAT and
A1: h.0 = [ C(), r04, r14, r24 ] and
A2: for n being Nat holds h.(n+1) = H(n,h.n) from NAT_1:sch 11;
  deffunc X3(set) = h.(In($1,NAT)-'2);
  deffunc X2(set) = [ B(), C(), r04, r14 ];
  deffunc X1(set) = [ A(), B(), C(), r04 ];
A3: for c being set st c in NAT holds C1[c] or C2[c] or C3[c]
  proof
    let c be set;
    assume c in NAT;
    then In(c,NAT) = c by FUNCT_7:def 1;
    hence thesis by NAT_1:25;
  end;
A4: for c being set st c in NAT holds (C1[c] implies not C2[c]) & (C1[c]
  implies not C3[c]) & (C2[c] implies not C3[c])
  proof
    let c be set;
    assume c in NAT;
    then In(c,NAT) = c by FUNCT_7:def 1;
    hence thesis;
  end;
  consider g being Function such that
  dom g = NAT and
A5: for x being set st x in NAT holds (C1[x] implies g.x = X1(x)) & (C2[
x] implies g.x = X2(x)) & (C3[x] implies g.x = X3(x)) from ExFunc3Cond(A4,A3);
A6: In(2,NAT) = 2 by FUNCT_7:def 1;
  then
A7: g.2 = X3(2) by A5
    .= [ C(), r04, r14, r24 ] by A1,A6,XREAL_1:232;
A8: for n being Element of NAT holds g.(n+3) = G(n+2,g.(n+2))
  proof
    let n be Element of NAT;
A9: In(n+2,NAT) = n+2 by FUNCT_7:def 1;
    0+1 < n+2 by NAT_1:2,XREAL_1:8;
    then
A10: g.(n+2) = X3(n+2) by A5,A9
      .= h.n by A9,NAT_D:34;
A11: In(n+3,NAT) = n+3 by FUNCT_7:def 1;
A12: n+3-2 = n+(3-2) & 0 <= n+1 by NAT_1:2;
    0+1 < n+3 by NAT_1:2,XREAL_1:8;
    hence g.(n+3) = X3(n+3) by A5,A11
      .= h.(n+1) by A11,A12,XREAL_0:def 2
      .= G(n+2,g.(n+2)) by A2,A10;
  end;
A13: g.1 = [ B(), C(), r04, r14 ] by A5;
  then
A14: (g.(0+1))`3_4 = r04 by Def6
    .= (g.(0+2))`2_4 by A7,Def5;
A15: g.0 = [ A(), B(), C(), r04 ] by A5;
  then
A16: (g.0)`3_4 = C() by Def6
    .= (g.(0+1))`2_4 by A13,Def5;
A17: (g.(0+1))`4_4 = r14 by A13,Def7
    .= (g.(0+2))`3_4 by A7,Def6;
A18: (g.0)`4_4 = r04 by A15,Def7
    .= (g.(0+1))`3_4 by A13,Def6;
A19: (g.(0+1))`1_4 = B() by A13,Def4
    .= (g.0)`2_4 by A15,Def5;
  deffunc M(Element of NAT) = (g.$1)`1_4;
  consider f being Function such that
A20: dom f = NAT and
A21: for x being Element of NAT holds f.x = M(x) from FUNCT_1:sch 4;
A22: f.(0+3) = (g.(0+3))`1_4 by A21
    .= G(0+2,g.(0+2))`1_4 by A8
    .= (g.(0+2))`2_4;
  take f;
  thus dom f = NAT by A20;
  defpred P[Element of NAT] means f.($1+3) = (g.($1+2))`2_4 & (g.$1)`2_4 = (g.
($1+1))`1_4 & (g.$1)`3_4 = (g.($1+1))`2_4 & (g.$1)`4_4 = (g.($1+1))`3_4 & (g.(
$1+1))`2_4 = (g.($1+2))`1_4 & (g.($1+1))`3_4 = (g.($1+2))`2_4 & (g.($1+1))`4_4
= (g.($1+2))`3_4 & (g.($1+2))`2_4 = (g.($1+3))`1_4 & f.($1+3) = F($1,f.$1,f.($1
  +1),f.($1+2));
A23: (g.(0+2))`2_4 = G(0+2,g.(0+2))`1_4
    .= (g.(0+3))`1_4 by A8;
  thus
A24: f.0 = (g.0)`1_4 by A21
    .= A() by A15,Def4;
  thus
A25: f.1 = (g.1)`1_4 by A21
    .= B() by A13,Def4;
  thus
A26: f.2 = (g.2)`1_4 by A21
    .= C() by A7,Def4;
A27: for x being Element of NAT st P[x] holds P[x+1]
  proof
    let x be Element of NAT;
A28: x+1+2 = x+(1+2);
    assume
A29: P[x];
    then
A30: f.(x+1+1) = (g.x)`3_4 by A21;
    thus
A31: f.(x+1+3) = (g.(x+1+3))`1_4 by A21
      .= G(x+1+2,g.(x+1+2))`1_4 by A8
      .= (g.(x+1+2))`2_4;
    thus (g.(x+1+1))`1_4 = (g.(x+1))`2_4 by A29;
    thus (g.(x+1))`3_4 = (g.(x+1+1))`2_4 by A29;
    thus (g.(x+1))`4_4 = (g.(x+1+1))`3_4 by A29;
    thus (g.(x+1+1))`2_4 = G(x+2,g.(x+2))`1_4
      .= (g.(x+1+2))`1_4 by A8,A28;
    thus (g.(x+1+1))`3_4 = G(x+2,g.(x+2))`2_4
      .= (g.(x+1+2))`2_4 by A8,A28;
    thus (g.(x+1+1))`4_4 = G(x+2,g.(x+2))`3_4
      .= (g.(x+1+2))`3_4 by A8,A28;
    thus (g.(x+1+2))`2_4 = G(x+1+2,g.(x+1+2))`1_4
      .= (g.(x+1+3))`1_4 by A8;
    per cases;
    suppose
      x <= 1 & x <> 1;
      then
A32:  x = 0 by NAT_1:25;
      hence f.(x+1+3) = (g.(1+3))`1_4 by A21
        .= G(1+2,g.(1+2))`1_4 by A8
        .= (g.(0+3))`2_4
        .= G(0+2,g.(0+2))`2_4 by A8
        .= (g.(0+2))`3_4
        .= r14 by A7,Def6
        .= F(x+1,f.(x+1),f.(x+1+1),f.(x+1+2)) by A15,A25,A26,A29,A32,Def7;
    end;
    suppose
A33:  x = 1;
      then
A34:  f.(x+1+1) = r04 & f.(x+1+2) = r14 by A13,A29,A30,Def6,Def7;
      thus f.(x+1+3) = (g.(1+1+3))`1_4 by A21,A33
        .= G(2+2,g.(2+2))`1_4 by A8
        .= (g.(1+3))`2_4
        .= G(1+2,g.(1+2))`2_4 by A8
        .= (g.(0+3))`3_4
        .= G(0+2,g.(0+2))`3_4 by A8
        .= (g.(0+2))`4_4
        .= F(x+1,f.(x+1),f.(x+1+1),f.(x+1+2)) by A7,A26,A33,A34,Def7;
    end;
    suppose
A35:  1 < x;
      then 1-1 <= x-1 by XREAL_1:13;
      then
A36:  x-1 = x-'1 by XREAL_0:def 2;
A37:  1+1 <= x by A35,NAT_1:13;
      then
A38:  x-'2+2 = x by XREAL_1:235;
      2-2 <= x-2 by A37,XREAL_1:13;
      then
A39:  x-2 = x-'2 by XREAL_0:def 2;
A40:  x+1 = x-1+2;
      thus f.(x+1+3) = (g.(x+(1+2)))`2_4 by A31
        .= G(x+2,g.(x+2))`2_4 by A8
        .= (g.(x-'1+3))`3_4 by A36
        .= G(x+1,g.(x+1))`3_4 by A8,A36,A40
        .= (g.(x-'2+3))`4_4 by A39
        .= G(x-'2+2,g.(x-'2+2))`4_4 by A8
        .= F(x+1,(g.x)`2_4,(g.x)`3_4,(g.x)`4_4) by A38
        .= F(x+1,f.(x+1),f.(x+1+1),f.(x+1+2)) by A21,A29,A30;
    end;
  end;
  (g.(0+1))`2_4 = C() by A13,Def5
    .= (g.(0+2))`1_4 by A7,Def4;
  then
A41: P[0] by A7,A24,A25,A26,A22,A19,A16,A18,A14,A17,A23,Def5;
  for x being Element of NAT holds P[x] from NAT_1:sch 1(A41,A27);
  hence thesis;
end;

scheme
  LambdaRec3ExD { X() -> non empty set, A,B,C() -> Element of X(), F(set,set,
set,set) -> Element of X() }: ex f being Function of NAT,X() st f.0 = A() & f.1
= B() & f.2 = C() & for n being Element of NAT holds f.(n+3) = F(n,f.n,f.(n+1),
  f.(n+2)) proof
  consider f being Function such that
A1: dom f = NAT and
A2: f.0 = A() & f.1 = B() & f.2 = C() and
A3: for n being Element of NAT holds f.(n+3) = F(n,f.n,f.(n+1),f.(n+2))
  from LambdaRec3Ex;
  rng f c= X()
  proof
    let y be set;
    assume y in rng f;
    then consider n being set such that
A4: n in dom f and
A5: f.n = y by FUNCT_1:def 3;
    reconsider n as Element of NAT by A1,A4;
    per cases;
    suppose
      n <= 2;
      then n = 0 or n = 1 or n = 2 by NAT_1:26;
      hence thesis by A2,A5;
    end;
    suppose
      n > 2;
      then 2+1 <= n by NAT_1:13;
      then n-3 is Element of NAT by INT_1:5;
      then f.(n-3+3) = F(n-3,f.(n-3),f.(n-3+1),f.(n-3+2)) by A3;
      hence thesis by A5;
    end;
  end;
  then f is Function of NAT,X() by A1,FUNCT_2:def 1,RELSET_1:4;
  hence thesis by A2,A3;
end;

scheme
  LambdaRec3Un { A,B,C() -> set, F,G() -> Function, F(set,set,set,set) -> set
  }: F() = G()
provided
A1: dom F() = NAT and
A2: F().0 = A() & F().1 = B() & F().2 = C() and
A3: for n being Element of NAT holds F().(n+3) = F(n,F().n,F().(n+1),F()
.(n+2)) and
A4: dom G() = NAT and
A5: G().0 = A() & G().1 = B() & G().2 = C() and
A6: for n being Element of NAT holds G().(n+3) = F(n,G().n,G().(n+1),G()
.(n+2))
proof
  defpred Q[Nat] means F().$1 <> G().$1;
  assume F() <> G();
  then ex x being set st x in NAT & F().x <> G().x by A1,A4,FUNCT_1:2;
  then
A7: ex k being Nat st Q[k];
  consider m being Nat such that
A8: Q[m] and
A9: for n being Nat st Q[n] holds m <= n from NAT_1:sch 5(A7);
  now
    set k = m-'3;
A10: F().(k+3) = F(k,F().k,F().(k+1),F().(k+2)) & G().(k+3) = F(k,G().k,G(
    ).(k+1) ,G().(k+2)) by A3,A6;
    assume m <> 0 & m <> 1 & m <> 2;
    then 3 <= m by NAT_1:27;
    then
A11: m = k+3 by XREAL_1:235;
    then
A12: F().(k+1) = G().(k+1) by A9,XREAL_1:6;
A13: F().(k+2) = G().(k+2) by A9,A11,XREAL_1:6;
    k+0 < m by A11,XREAL_1:6;
    hence contradiction by A8,A9,A11,A12,A13,A10;
  end;
  hence contradiction by A2,A5,A8;
end;

scheme
  LambdaRec3UnD { X() -> non empty set, A,B,C() -> Element of X(), F,G() ->
  Function of NAT,X(), F(set,set,set,set) -> Element of X() }: F() = G()
provided
A1: F().0 = A() & F().1 = B() & F().2 = C() and
A2: for n being Element of NAT holds F().(n+3) = F(n,F().n,F().(n+1),F()
.(n+2)) and
A3: G().0 = A() & G().1 = B() & G().2 = C() and
A4: for n being Element of NAT holds G().(n+3) = F(n,G().n,G().(n+1),G()
.(n+2))
proof
A5: dom G() = NAT by FUNCT_2:def 1;
A6: dom F() = NAT by FUNCT_2:def 1;
  thus F() = G() from LambdaRec3Un(A6,A1,A2,A5,A3,A4);
end;

:: 4 steps

scheme
  LambdaRec4Un { A,B,C,D() -> set, F,G() -> Function, F(set,set,set,set,set)
  -> set }: F() = G()
provided
A1: dom F() = NAT and
A2: F().0 = A() & F().1 = B() & F().2 = C() & F().3 = D() and
A3: for n being Element of NAT holds F().(n+4) = F(n,F().n,F().(n+1),F()
.(n+2),F().(n+3)) and
A4: dom G() = NAT and
A5: G().0 = A() & G().1 = B() & G().2 = C() & G().3 = D() and
A6: for n being Element of NAT holds G().(n+4) = F(n,G().n,G().(n+1),G()
.(n+2),G().(n+3))
proof
  defpred Q[Nat] means F().$1 <> G().$1;
  assume F() <> G();
  then ex x being set st x in NAT & F().x <> G().x by A1,A4,FUNCT_1:2;
  then
A7: ex k being Nat st Q[k];
  consider m being Nat such that
A8: Q[m] and
A9: for n being Nat st Q[n] holds m <= n from NAT_1:sch 5(A7);
  now
    set k = m-'4;
A10: F().(k+4) = F(k,F().k,F().(k+1),F().(k+2),F().(k+3)) & G().(k+4) = F(
    k,G().k,G().(k+1),G().(k+2),G().(k+3)) by A3,A6;
    assume m <> 0 & m <> 1 & m <> 2 & m <> 3;
    then 4 <= m by NAT_1:28;
    then
A11: m = k+4 by XREAL_1:235;
    then
A12: F().(k+1) = G().(k+1) by A9,XREAL_1:6;
    k+3 < m by A11,XREAL_1:6;
    then
A13: F().(k+3) = G().(k+3) by A9;
    k+2 < m by A11,XREAL_1:6;
    then
A14: F().(k+2) = G().(k+2) by A9;
    k+0 < m by A11,XREAL_1:6;
    hence contradiction by A8,A9,A11,A12,A14,A13,A10;
  end;
  hence contradiction by A2,A5,A8;
end;

scheme
  LambdaRec4UnD { X() -> non empty set, A,B,C,D() -> Element of X(), F,G() ->
  Function of NAT,X(), F(set,set,set,set,set) -> Element of X() }: F() = G()
provided
A1: F().0 = A() & F().1 = B() & F().2 = C() & F().3 = D() and
A2: for n being Element of NAT holds F().(n+4) = F(n,F().n,F().(n+1),F()
.(n+2),F().(n+3)) and
A3: G().0 = A() & G().1 = B() & G().2 = C() & G().3 = D() and
A4: for n being Element of NAT holds G().(n+4) = F(n,G().n,G().(n+1),G()
.(n+2),G().(n+3))
proof
A5: dom G() = NAT by FUNCT_2:def 1;
A6: dom F() = NAT by FUNCT_2:def 1;
  thus F() = G() from LambdaRec4Un(A6,A1,A2,A5,A3,A4);
end;

begin :: Addenda

:: 2010.05.120, A.T.

theorem
 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
  proof
   let x,y,X,Y,Z be set;
   assume
A1:  x`1_3 = y`1_3 & x`2_3 = y`2_3 & x`3_3 = y`3_3 & y in [:X,Y,Z:];
   assume x in [:X,Y,Z:];
   hence x = [ x`1_3, x`2_3, x`3_3 ] by Th3
      .= y by A1,Th3;
  end;