The Mizar article:

Recursive Definitions

by
Krzysztof Hryniewiecki

Received September 4, 1989

Copyright (c) 1989 Association of Mizar Users

MML identifier: RECDEF_1
[ 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;
 definitions TARSKI;
 theorems AXIOMS, TARSKI, REAL_1, NAT_1, FUNCT_1, FINSEQ_1, FUNCT_2, RELAT_1,
      PARTFUN1, CARD_1, XBOOLE_1, XCMPLX_1;
 schemes NAT_1, FUNCT_1, FUNCT_2, FINSEQ_1;

begin

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

Lm1: for p being FinSequence of D st 1 <= n & n <= len p holds
            p.n is Element of D
  proof let p be FinSequence of D;
    assume 1 <= n & n <= len p;
    then n in Seg len p by FINSEQ_1:3;
    then n in dom p by FINSEQ_1:def 3;
    then A1: p.n in rng p by FUNCT_1:def 5;
      rng p c= D by FINSEQ_1:def 4;
   hence p.n is Element of D by A1;
  end;

definition let D be set, p be PartFunc of D,NAT; let n be Element of D;
 redefine func p.n -> Nat;
  coherence
    proof
      per cases;
      suppose n in dom p;
      hence p.n is Nat by PARTFUN1:27;
      suppose not n in dom p;
      hence p.n is Nat by CARD_1:51,FUNCT_1:def 4;
    end;
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
  A1: for n being Nat for x being set
       ex y being set st P[n,x,y] and
  A2: for n being Nat for x,y1,y2 being set
         st P[n,x,y1] & P[n,x,y2] holds y1=y2
proof
   deffunc S(Nat) = {k : k <= $1};
  A3: for p,q being Function,k st dom p = S(k) & dom q = S(k) & p.0 = q.0 &
            for n st n < k holds P[n,p.n,p.(n+1)] & P[n,q.n,q.(n+1)]
          holds p = q
          proof let p,q be Function;let k;
            defpred Z[Nat] means $1 <= k implies p.$1 = q.$1;
            assume A4: dom p = S(k) & dom q = S(k) & p.0 = q.0 &
            for n st n < k holds P[n,p.n,p.(n+1)] & P[n,q.n,q.(n+1)];
            then A5: Z[0];
            A6: for n be Nat st Z[n] holds Z[n+1]
               proof let n; assume A7: n <= k implies p.n = q.n;
                  assume n+1 <= k;
                   then n < k by NAT_1:38;
                   then P[n,p.n,p.(n+1)] & P[n,p.n,q.(n+1)] by A4,A7;
                  hence p.(n+1) = q.(n+1) by A2;
               end;
            A8: for n holds Z[n] from Ind(A5,A6);
              for x st x in S(k) holds p.x = q.x
              proof let x; assume x in S(k);
                 then ex m st m=x & m <= k;
               hence p.x = q.x by A8;
              end;
            hence p = q by A4,FUNCT_1:9;
          end;
  A9: for n ex p being Function st dom p = S(n) & p.0 = A() &
              for k st k < n holds P[k,p.k,p.(k+1)]
       proof
       defpred Z[Nat] means ex p being Function st dom p = S($1) & p.0 = A() &
              for k st k < $1 holds P[k,p.k,p.(k+1)];
       A10: Z[0]
           proof
             deffunc F(set)= A();
             consider s being Function such that A11:
               dom s = S(0) & for x st x in S(0) holds s.x = F(x) from Lambda;
             take s;
             thus dom s = S(0) by A11;
                   0 in S(0);
            hence s.0 = A() by A11;
            thus thesis by NAT_1:18;
           end;
       A12: for n st Z[n] holds Z[n+1]
           proof let n;
             given p being Function such that A13:
               dom p = S(n) & p.0 = A() &
              for k st k < n holds P[k,p.k,p.(k+1)];
              consider z such that A14: P[n,p.n,z] by A1;
               defpred ST[set,set] means (for k st k=$1 holds
                      (k <= n implies $2 = p.k) &
                      (k=n+1 implies $2 = z ));
              A15: for x,y1,y2 being set st x in S(n+1) &
              ST[x,y1] & ST[x,y2] holds y1 = y2
                 proof let x,y1,y2 be set;
                  assume A16: x in S(n+1) &
                    (for k st k=x holds
                      (k <= n implies y1 = p.k) &
                      (k=n+1 implies y1 = z )) &
                    (for k st k=x holds
                      (k <= n implies y2 = p.k) &
                      (k=n+1 implies y2 = z ));
 then A17:                    ex m st m=x & m <= n+1;
                    then reconsider x as Nat;
                     A18: now assume A19: x = n+1;
                          hence y1 = z by A16 .= y2 by A16,A19;
                         end;
                           now assume A20: x <= n;
                           hence y1 = p.x by A16 .= y2 by A16,A20;
                         end;
                      hence thesis by A17,A18,NAT_1:26;
                 end;

              A21: for x st x in S(n+1) ex y st ST[x,y]
                   proof let x; assume x in S(n+1);
 then A22:                     ex m st m=x & m <= n+1;
                     then reconsider t=x as Nat;

                     A23: t = n+1 implies thesis
                          proof assume A24: t=n+1;
                            take z;
                            let k such that A25: k=x;
                            thus k <= n implies z=p.k
                              proof assume k <= n;
                                then n+1 <= n+0 by A24,A25;
                               hence thesis by REAL_1:53;
                              end;
                            thus thesis;
                          end;

                           t <= n implies thesis
                           proof assume A26: t <= n;
                             take p.x; let k; assume A27: k=x;
                             hence k <= n implies p.x = p.k;

                             assume k=n+1;
                             then n+1 <= n+0 by A26,A27;
                            hence thesis by REAL_1:53;
                           end;
                      hence thesis by A22,A23,NAT_1:26;
                   end;

               consider q being Function such that A28: dom q = S(n+1) &
                  for x st x in S(n+1) holds ST[x,q.x] from FuncEx(A15,A21);
               take q;
               thus dom q = S(n+1) by A28;
               thus q.0 = A()
                 proof
                     0 <= n+1 by NAT_1:18;
                   then A29: 0 in S(n+1);
                     0 <= n by NAT_1:18;
                  hence q.0 = A() by A13,A28,A29;
                 end;
               let k such that
A30:             k < n+1;
             A31: now assume A32: k = n;
                   then k+1 in S(n+1);
                   then A33: P[k,p.k,q.(k+1)] by A14,A28,A32;
                      k <= n+1 by A32,NAT_1:29;
                    then k in S(n+1);
                  hence P[k,q.k,q.(k+1)] by A28,A32,A33;
                end;
                  now assume k <> n;
                    then A34: k+1 <> n+1 by XCMPLX_1:2;
A35:                    k+1 <= n+1 by A30,NAT_1:38;
                    then A36: k+1 <= n by A34,NAT_1:26;
                    A37: k+1 in S(n+1) by A35;

A38:                 k < n by A36,NAT_1:38;
                        then P[k,p.k,p.(k+1)] by A13;
                    then A39: P[k,p.k,q.(k+1)] by A28,A36,A37;
                          k in S(n+1) by A30;
                  hence P[k,q.k,q.(k+1)] by A28,A38,A39;
                end;
              hence thesis by A31;
           end;
         thus for n holds Z[n] from Ind(A10,A12);
       end;
  A40: for p,q being Function,k st dom p = S(k) &
               dom q = S(k+1) & p.0 = q.0 &
            for n st n < k holds P[n,p.n,p.(n+1)] & P[n,q.n,q.(n+1)]
          holds p.k = q.k
       proof let p,q be Function;let k;
         defpred Z[Nat] means $1 <= k implies p.$1 = q.$1;
         assume A41: dom p = S(k) &
               dom q = S(k+1) & p.0 = q.0 &
            for n st n < k holds P[n,p.n,p.(n+1)] & P[n,q.n,q.(n+1)];
         then A42: Z[0];
         A43: for n st Z[n] holds Z[n+1]
                proof let n; assume A44: n <= k implies p.n = q.n;
                  assume n+1 <= k;
                   then n < k by NAT_1:38;
                      then P[n,p.n,p.(n+1)] & P[n,p.n,q.(n+1)] by A41,A44;
                    hence p.(n+1) = q.(n+1) by A2;
                end;

             for n holds Z[n] from Ind(A42,A43);
          hence p.k = q.k;
       end;

     ex f being Function st dom f = NAT &
     for n ex p being Function st dom p = S(n) & p.0 = A() &
              (for k st k < n holds P[k,p.k,p.(k+1)]) &
               f.n = p.n
    proof
      defpred Z[set,set] means
          for n st n=$1 ex p being Function st dom p = S(n) & p.0 = A() &
              (for k st k < n holds P[k,p.k,p.(k+1)]) & $2 = p.n;
      A45: for x,y1,y2 being set st x in NAT & Z[x,y1] & Z[x,y2]
          holds y1 = y2
          proof let x,y1,y2 be set; assume A46: x in NAT &
          (for n st n=x ex p being Function st dom p = S(n) & p.0 = A() &
              (for k st k < n holds P[k,p.k,p.(k+1)]) & y1 = p.n) &
          (for n st n=x ex p being Function st dom p = S(n) & p.0 = A() &
              (for k st k < n holds P[k,p.k,p.(k+1)]) & y2 = p.n);

            then reconsider n=x as Nat;
            consider p1 being Function such that A47:
              dom p1 = S(n) & p1.0 = A() &
              (for k st k < n holds P[k,p1.k,p1.(k+1)]) & y1 = p1.n
                by A46;
            consider p2 being Function such that A48:
              dom p2 = S(n) & p2.0 = A() &
              (for k st k < n holds P[k,p2.k,p2.(k+1)]) & y2 = p2.n
                by A46;
               for k st k < n holds
                  P[k,p1.k,p1.(k+1)] & P[k,p2.k,p2.(k+1)] by A47,A48;
            hence y1 = y2 by A3,A47,A48;
          end;
      A49: for x st x in NAT ex y st Z[x,y]
          proof let x; assume x in NAT;
            then reconsider n=x as Nat;
            consider p being Function such that A50: dom p = S(n) & p.0 = A() &
                for k st k < n holds P[k,p.k,p.(k+1)] by A9;
            take p.n;
            let k such that A51: k = x;
            take p;
            thus thesis by A50,A51;
          end;
      consider f being Function such that A52:
          dom f = NAT & for x st x in NAT holds Z[x,f.x] from FuncEx(A45,A49);
      take f;
      thus dom f = NAT by A52;
      let n;
      consider p being Function such that A53:
        dom p = S(n) & p.0 = A() &
          (for k st k < n holds P[k,p.k,p.(k+1)])
           & f.n = p.n by A52;
      take p;
      thus dom p = S(n) & p.0 = A() by A53;
      thus for k st k < n holds P[k,p.k,p.(k+1)] by A53;
      thus f.n = p.n by A53;
    end;
   then consider f being Function such that A54: dom f = NAT &
     for n ex p being Function st dom p = S(n) & p.0 = A() &
              (for k st k < n holds P[k,p.k,p.(k+1)]) &
               f.n = p.n;
   take f;
   thus dom f = NAT by A54;
   thus f.0 = A()
      proof
           ex p being Function st dom p = S(0) & p.0 = A() &
         (for k st k < 0 holds P[k,p.k,p.(k+1)]) &
               f.0 = p.0 by A54;
        hence f.0 = A();
      end;

   let d be Element of NAT;
   consider p being Function such that A55: dom p = S(d+1) & p.0 = A() &
     (for k st k < d+1 holds P[k,p.k,p.(k+1)]) &
               f.(d+1) = p.(d+1) by A54;
   consider q being Function such that A56: dom q = S(d) & q.0 = A() &
     (for k st k < d holds P[k,q.k,q.(k+1)]) &
               f.d = q.d by A54;
   A57: p.d = q.d
      proof
          dom p = S(d+1) & dom q = S(d) & p.0 = q.0 &
            for k st k < d holds
              P[k,q.k,q.(k+1)] & P[k,p.k,p.(k+1)]
         proof
           thus dom p = S(d+1) by A55;
           thus dom q = S(d) by A56;
           thus p.0 = q.0 by A55,A56;
           let k; assume A58: k < d;
             hence P[k,q.k,q.(k+1)] by A56;
               d <= d+1 by NAT_1:29;
             then k < d+1 by A58,AXIOMS:22;
           hence thesis by A55;
         end;
        hence thesis by A40;
      end;
     d < d+1 by REAL_1:69;
  hence thesis by A55,A56,A57;
end;

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
  A1: for n being Nat for x being Element of D()
       ex y being Element of D() st P[n,x,y]
proof
  defpred Q[Element of NAT qua non empty set,set,set] means
           P[$1,$2,$3];
A2: for x being Element of NAT qua non empty set for y being Element of D()
      ex z being Element of D() st Q[x,y,z] by A1;

  consider f being Function of [:(NAT qua non empty set),D():],D()
   such that A3:
   for x being Element of NAT qua non empty set for y being Element of D()
    holds Q[x,y,f.[x qua set,y]] from FuncEx2D(A2);
  defpred P[FinSequence] means
     ($1.1=A() & for n st n+2 <= len $1 holds $1.(n+2) = f.[n,$1.(n+1)]);
  consider X being set such that A4:
     for x holds x in X iff ex p st p in D()* &
       P[p] &
       x=p from SepSeq;
 A5: x in X implies x in D()*
    proof assume x in X;
       then ex p st p in D()* &
        (p.1=A() & for n st n + 2 <= len p holds p.(n+2) = f.[n,p.(n+1)]) &
          x=p by A4;
       hence thesis;
    end;

A6:  for p,q st p in X & q in X & len p <= len q holds p c= q
     proof let p,q;
       assume A7: p in X & q in X & len p <= len q;
       A8: (p in D()* & p.1 = A() &
            for n st n + 2 <= len p holds p.(n+2) = f.[n,p.(n+1)]) &
           (q in D()* & q.1 = A() &
            for n st n + 2 <= len q holds q.(n+2) = f.[n,q.(n+1)])
            proof
             A9: ex p' being FinSequence st
                  p' in D()* & (p'.1 = A() &
                   for n st n+2<=len p' holds p'.(n+2) = f.[n,p'.(n+1)]) &
                    p=p' by A4,A7;
                  ex q' being FinSequence st
                  q' in D()* & (q'.1 = A() &
                   for n st n+2<=len q' holds q'.(n+2) = f.[n,q'.(n+1)]) &
                    q=q' by A4,A7;
                 hence thesis by A9;
            end;

       A10: for n st 1 <= n & n <= len p holds p.n = q.n
            proof
              defpred P[Nat] means 1 <= $1 & $1 <= len p & p.$1 <> q.$1;
              assume A11: ex n st P[n];
              consider k such that A12: P[k] &
                  for n st P[n] holds k <= n from Min(A11);
                    k = 1
                  proof assume A13: k <> 1;
                      0 <> k by A12;
                    then consider n such that A14: k = n+1 by NAT_1:22;
                      1 < n+1 by A12,A13,A14,REAL_1:def 5;
                    then A15: 1 <= n by NAT_1:38;
                    A16: n <> 0 by A13,A14;
                      n+0 <= n+1 by REAL_1:55;
                    then A17: n <= len p by A12,A14,AXIOMS:22;
A18:                n+0 < n+1 by REAL_1:53;
                    consider m such that A19: n=m+1 by A16,NAT_1:22;
A20:                    m+(1+1) <= len p by A12,A14,A19,XCMPLX_1:1;
                    then A21: m+2 <= len q by A7,AXIOMS:22;
                      p.k = p.(m+(1+1)) by A14,A19,XCMPLX_1:1
                      .=f.[m,p.n] by A8,A19,A20
                      .=f.[m,q.(m+1)] by A12,A14,A15,A17,A18,A19
                      .=q.(m+(1+1)) by A8,A21
                      .=q.k by A14,A19,XCMPLX_1:1;
                   hence thesis by A12;
                  end;
                hence contradiction by A8,A12;
            end;
          now let x;
          assume x in p;
            then consider n such that A22: n in dom p & x = [n,p.n] by FINSEQ_1
:16;
              n in Seg len p by A22,FINSEQ_1:def 3;
            then A23: 1 <= n & n <= len p by FINSEQ_1:3;
            then A24: x = [n,q.n] by A10,A22;
              1 <= n & n <= len q by A7,A23,AXIOMS:22;
            then n in Seg len q by FINSEQ_1:3;
            then n in dom q by FINSEQ_1:def 3;
          hence x in q by A24,FUNCT_1:8;
        end;
      hence thesis by TARSKI:def 3;
     end;

  set Y = union X;
    ex f being Function st f = Y
  proof
   defpred Z[set,set] means [$1,$2] in Y;
   A25: for x,y,z st Z[x,y] & Z[x,z] holds y=z
        proof let x,y,z;
          assume A26: [x,y] in Y & [x,z] in Y;
          then consider Z1 being set such that A27:
             [x,y] in Z1 & Z1 in X by TARSKI:def 4;
            Z1 in D()* by A5,A27;
          then reconsider p=Z1 as FinSequence of D() by FINSEQ_1:def 11;
          consider Z2 being set such that A28:
             [x,z] in Z2 & Z2 in X by A26,TARSKI:def 4;
            Z2 in D()* by A5,A28;
          then reconsider q=Z2 as FinSequence of D() by FINSEQ_1:def 11;

          A29: now assume len p <= len q;
                 then p c= Z2 by A6,A27,A28;
                 then [x,y] in q & [x,z] in q by A27,A28;
                hence y=z by FUNCT_1:def 1;
              end;
                now assume len q <= len p;
                 then q c= Z1 by A6,A27,A28;
                 then [x,y] in p & [x,z] in p by A27,A28;
                hence y=z by FUNCT_1:def 1;
              end;
            hence thesis by A29;
        end;

   consider h being Function such that A30:
     for x,y holds [x,y] in h iff x in NAT & Z[x,y] from GraphFunc(A25);
    take h;
  A31: for x,y holds [x,y] in h iff [x,y] in Y
     proof let x,y;
      thus
          [x,y] in h implies [x,y] in Y by A30;
      thus
          [x,y] in Y implies [x,y] in h
         proof
           assume A32: [x,y] in Y;
           then consider Z such that A33: [x,y] in Z & Z in X by TARSKI:def 4;
             Z in D()* by A5,A33;
           then reconsider p=Z as FinSequence of D() by FINSEQ_1:def 11;
             x in dom p by A33,RELAT_1:def 4;
          hence thesis by A30,A32;
         end;
     end;
     for x holds x in h iff x in Y
    proof let x;
      thus x in h implies x in Y
        proof
          assume A34: x in h;
           then ex y,z st [y,z] = x by RELAT_1:def 1;
         hence thesis by A31,A34;
        end;
       assume A35: x in Y;
       then consider Z such that A36: x in Z & Z in X by TARSKI:def 4;
         Z in D()* by A5,A36;
       then reconsider p=Z as FinSequence of D() by FINSEQ_1:def 11;
         x in p by A36;
        then ex y,z st [y,z] = x by RELAT_1:def 1;
      hence thesis by A31,A35;
    end;
    hence h = Y by TARSKI:2;
  end;
  then consider g being Function such that A37: g = Y;

A38:  rng g c= D()
  proof
      for x st x in rng g holds x in D()
     proof let x; assume x in rng g;
        then consider y such that A39: y in dom g & x = g.y by FUNCT_1:def 5;
          [y,x] in Y by A37,A39,FUNCT_1:8;
        then consider Z such that A40: [y,x] in Z & Z in X by TARSKI:def 4;
          Z in D()* by A5,A40;
        then reconsider p=Z as FinSequence of D() by FINSEQ_1:def 11;
        A41: y in dom p by A40,FUNCT_1:8;
          x = p.y by A40,FUNCT_1:8;
        then A42: x in rng p by A41,FUNCT_1:def 5;
          rng p c= D() by FINSEQ_1:def 4;
      hence x in D() by A42;
     end;
   hence thesis by TARSKI:def 3;
  end;
  then reconsider h = g as Function of dom g,D() by FUNCT_2:4;

    A43: for n holds (n+1) in dom h
        proof
          defpred P[Nat] means $1+1 in dom h;
           A44: P[0]
             proof
               A45: <*A()*>.1 = A() by FINSEQ_1:def 8;
               A46: <*A()*> in D()* by FINSEQ_1:def 11;
                    for n st n+2 <= len <*A()*> holds
                      <*A()*>.(n+2) = f.[n,<*A()*>.(n+1)]
                  proof let n; assume n+2 <= len <*A()*>;
                  then n+2 <= 1 by FINSEQ_1:56;
                  then n+(1+1) <= n+1 by NAT_1:37;
                  hence thesis by REAL_1:53;
                  end;
              then <*A()*> in X by A4,A45,A46;
              then A47: {[1,A()]} in X by FINSEQ_1:52;
                    [1,A()] in {[1,A()]} by TARSKI:def 1;
                 then [1,A()] in h by A37,A47,TARSKI:def 4;
                hence 0+1 in dom h by FUNCT_1:8;
             end;

           A48: for k st P[k] holds P[k+1]
                 proof let k; assume k+1 in dom h;
                   then [k+1,h.(k+1)] in Y by A37,FUNCT_1:8;
                   then consider Z such that A49:
                     [k+1,h.(k+1)] in Z & Z in X by TARSKI:def 4;
                     Z in D()* by A5,A49;
                   then reconsider Z as FinSequence of D() by FINSEQ_1:def 11;
                   A50: k+1 = len Z implies thesis
                         proof assume A51: k+1 = len Z;
                           set p=Z^<*f.[k,Z.(k+1)]*>;
                              len p = len Z + len <*f.[k,Z.(k+1)]*>
                                  by FINSEQ_1:35
                             .=k+1+1 by A51,FINSEQ_1:56;
                          then 1 <= k+1+1 & k+1+1 <= len p by NAT_1:37;
                          then k+1+1 in Seg len p by FINSEQ_1:3;
                          then k+1+1 in dom p by FINSEQ_1:def 3;
                          then A52: [k+1+1,p.(k+1+1)] in p by FUNCT_1:8;

                       p in X
                       proof
                           1 <= 1 & 1 <= len Z by A51,NAT_1:37;
                         then 1 in Seg len Z by FINSEQ_1:3;
                         then A53: 1 in dom Z by FINSEQ_1:def 3;
                            Z.1 = A()
                            proof
                                 ex p being FinSequence st
                                p in D()* & p.1 = A() &
                               (for n st n+2 <= len p holds
                                   p.(n+2) = f.[n,p.(n+1)]) & Z=p by A4,A49;
                              hence thesis;
                            end;
                         then A54: p.1 = A() by A53,FINSEQ_1:def 7;
                         A55: p in D()*
                             proof
                               reconsider n=k as Element of (NAT qua
                                          non empty set);
                                 Z.(k+1) is Element of D()
                                proof
                                    1 <= k + 1 by NAT_1:37;
                                  then k+1 in Seg len Z by A51,FINSEQ_1:3;
                                  then k+1 in dom Z by FINSEQ_1:def 3;
                                  then A56: Z.(k+1) in rng Z by FUNCT_1:def 5;
                                     rng Z c= D() by FINSEQ_1:def 4;
                                 hence Z.(k+1) is Element of D() by A56;
                                end;
                               then reconsider z=Z.(k+1) as Element of D();
                                 p= Z^<*f.[n,z]*>;
                              hence thesis by FINSEQ_1:def 11;
                             end;
                           for n st n+2 <= len p holds
                              p.(n+2) = f.[n,p.(n+1)]
                         proof let n;assume n+2 <= len p;
                   then A57: n+2 <=
 len Z + len <*f.[k,Z.(k+1)]*> by FINSEQ_1:35;
                           then A58: n+2 <= len Z + 1 by FINSEQ_1:57;
                           A59: n+2 = len Z + 1 implies thesis
                              proof assume A60: n+2 = len Z + 1;
                                then n+2 = k+(1+1) by A51,XCMPLX_1:1;
                             then A61: n=k by XCMPLX_1:2;
                              A62:  p.(n+2) =
                                <*f.[k,Z.(k+1)]*>.(n+2-len Z) by A57,A60,
FINSEQ_1:36
                                .=<*f.[k,Z.(k+1)]*>.(n+2-(n+2-1)) by A60,
XCMPLX_1:26
                                .=<*f.[k,Z.(k+1)]*>.(n+2-(n+2)+1) by XCMPLX_1:
37
                                .=<*f.[k,Z.(k+1)]*>.(0+1) by XCMPLX_1:14
                                .=f.[n,Z.(n+1)] by A61,FINSEQ_1:57;
                                 A63: 1 <= n + 1 by NAT_1:37;
                                   n+(1+1) <= len Z + 1 by A57,FINSEQ_1:57;
                                 then n+1+1 <= len Z + 1 by XCMPLX_1:1;
                                 then n+1 <= len Z by REAL_1:53;
                                 then n+1 in Seg len Z by A63,FINSEQ_1:3;
                                 then n+1 in dom Z by FINSEQ_1:def 3;
                               hence thesis by A62,FINSEQ_1:def 7;
                              end;
                                 n+2 <> len Z + 1 implies thesis
                                proof assume A64: n+2 <> len Z + 1;
                                   then A65: n+2 <= len Z by A58,NAT_1:26;
                                     1 <= n+(1+1) by NAT_1:37;
                                   then n+2 in Seg len Z by A65,FINSEQ_1:3;
then A66:                                   n+2 in dom Z by FINSEQ_1:def 3;
                                      ex q st
                                     q in D()* & q.1 = A() &
                                    (for n st n+2 <= len q holds
                                       q.(n+2) = f.[n,q.(n+1)]) &
                                            Z = q by A4,A49;
                                 then Z.(n+2) = f.[n,Z.(n+1)] by A65;
                                 then A67: p.(n+2) = f.[n,Z.(n+1)] by A66,
FINSEQ_1:def 7;
                                 A68: 1 <= n + 1 by NAT_1:37;
                                   n+(1+1) <= len Z by A58,A64,NAT_1:26;
                                 then n+1+1 <= len Z by XCMPLX_1:1;
                                 then n+1+1 <= len Z + 1 by NAT_1:37;
                                 then n+1 <= len Z by REAL_1:53;
                                 then n+1 in Seg len Z by A68,FINSEQ_1:3;
                                 then n+1 in dom Z by FINSEQ_1:def 3;
                                hence thesis by A67,FINSEQ_1:def 7;
                               end;
                            hence thesis by A59;
                         end;
                        hence thesis by A4,A54,A55;
                       end;
                          then [k+1+1,p.(k+1+1)] in h by A37,A52,TARSKI:def 4;
                         hence k+1+1 in dom h by FUNCT_1:8;
                     end;

                        k+1 <> len Z implies thesis
                        proof assume A69: k+1 <> len Z;
                           k+1 in dom Z by A49,FUNCT_1:8;
                         then k+1 in Seg len Z by FINSEQ_1:def 3;
                          then 1 <= k+1 & k+1 <= len Z by FINSEQ_1:3;
                         then k+1 < len Z by A69,REAL_1:def 5;
                         then A70: k+1+1 <= len Z by NAT_1:38;
                           1 <= k+1+1 by NAT_1:37;
                         then k+1+1 in Seg len Z by A70,FINSEQ_1:3;
                         then k+1+1 in dom Z by FINSEQ_1:def 3;
                          then [k+1+1,Z.(k+1+1)] in Z by FUNCT_1:8;
                         then [k+1+1,Z.(k+1+1)] in h by A37,A49,TARSKI:def 4;
                        hence k+1+1 in dom h by FUNCT_1:8;
                       end;
                     hence thesis by A50;
                 end;
          thus for k holds P[k] from Ind(A44,A48);
        end;

    ex g being Function of NAT,D() st for n holds g.n = h.(n+1)
    proof
        ex g being Function st dom g = NAT & for n holds g.n = h.(n+1)
      proof
        defpred P[set,set] means ex n st n = $1 & $2=h.(n+1);
        A71: for x,y1,y2 st x in NAT & P[x,y1] & P[x,y2] holds y1=y2;
        A72: for x st x in NAT ex y st P[x,y]
            proof let x; assume x in NAT;
               then reconsider n=x as Nat;
               take h.(n+1);take n;thus thesis;
            end;
        consider g being Function such that A73:
          dom g = NAT & for x st x in NAT holds P[x,g.x] from FuncEx(A71,A72);
        take g;
        thus dom g = NAT by A73;
        thus for n holds g.n = h.(n+1)
           proof let n;
                 ex m st m=n & g.n = h.(m+1) by A73;
              hence thesis;
           end;
      end;
      then consider g being Function such that
      A74: dom g = NAT & for n holds g.n = h.(n+1);
       rng g c= D()
       proof let x; assume x in rng g;
         then consider y such that A75: y in dom g & x = g.y by FUNCT_1:def 5;
         reconsider k=y as Nat by A74,A75;
           k+1 in dom h by A43;
         then A76: h.(k+1) in rng h by FUNCT_1:def 5;
           x=h.(k+1) by A74,A75;
        hence x in D() by A38,A76;
       end;
     then reconsider g as Function of NAT,D() by A74,FUNCT_2:4;
     take g;
     thus thesis by A74;
   end;
  then consider g being Function of NAT,D() such that A77:
     for n holds g.n = h.(n+1);
  take g;

 A78: for n holds h.(n+2) = f.[n,h.(n+1)]
     proof let n;
         (n+1)+1 in dom h by A43;
       then n+(1+1) in dom h by XCMPLX_1:1;
       then [n+2,h.(n+2)] in h by FUNCT_1:def 4;
       then consider Z being set such that A79:
         [n+2,h.(n+2)] in Z & Z in X by A37,TARSKI:def 4;
 A80:       ex p st p in D()* &
        (p.1=A() & for n st n+2 <= len p holds p.(n+2) = f.[n,p.(n+1)]) &
          Z=p by A4,A79;

         Z in D()* by A5,A79;
       then reconsider Z as FinSequence of D() by FINSEQ_1:def 11;
          n+2 in dom Z & h.(n+2) = Z.(n+2) by A79,FUNCT_1:8;
       then n+2 in Seg len Z by FINSEQ_1:def 3;
       then A81: n+2 <= len Z by FINSEQ_1:3;
      A82: 1 <= n+1 by NAT_1:37;
        n+1 <= n+2 by REAL_1:55;
      then n+1 <= len Z by A81,AXIOMS:22;
      then n+1 in Seg len Z by A82,FINSEQ_1:3;
      then n+1 in dom Z by FINSEQ_1:def 3;
       then [n+1,Z.(n+1)] in Z by FUNCT_1:8;
then A83:      [n+1,Z.(n+1)] in h by A37,A79,TARSKI:def 4;
     thus h.(n+2) = Z.(n+2) by A79,FUNCT_1:8
      .= f.[n,Z.(n+1)] by A80,A81
      .= f.[n,h.(n+1)] by A83,FUNCT_1:8;
    end;

  thus g.0 = A()
    proof
      A84: <*A()*> in D()* by FINSEQ_1:def 11;
      A85: <*A()*>.1 = A() by FINSEQ_1:def 8;
         for n st n + 2 <= len <*A()*>
           holds <*A()*>.(n+2) = f.[n,<*A()*>.(n+1)]
          proof let n; assume n + 2 <= len <*A()*>;
              then n +(1+1) <= 0 + 1 by FINSEQ_1:56;
              then n +1+1 <= 0 + 1 by XCMPLX_1:1;
              then n + 1 <= 0 by REAL_1:53;
              then n + 1 <= 0 + n by NAT_1:37;
            hence thesis by REAL_1:53;
          end;
     then <*A()*> in X by A4,A84,A85;
     then A86: {[1,A()]} in X by FINSEQ_1:52;
       [1,A()] in {[1,A()]} by TARSKI:def 1;
     then [1,A()] in h by A37,A86,TARSKI:def 4;
     then A() = h.(0+1) by FUNCT_1:8
      .= g.0 by A77;
    hence thesis;
   end;

      let n be Element of NAT;
           P[n,g.n,f.[n,g.n]] by A3;
        then A87: P[n,g.n,f.[n,h.(n+1)]] by A77;
            h.(n+(1+1)) =f.[n,h.(n+1)] by A78;
         then P[n,g.n,h.(n+1+1)] by A87,XCMPLX_1:1;
        hence P[n,g.n,g.(n+1)] by A77;
end;

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)
proof
  defpred P[set,set,set] means $3 = G($1,$2);
  A1: for n being Nat for x being set
        ex y being set st P[n,x,y];
  A2: for n being Nat for x,y1,y2 being set
        st P[n,x,y1] & P[n,x,y2] holds y1=y2;

  consider f being Function such that A3: dom f = NAT & f.0 = A() &
   for n being Element of NAT holds P[n,f.n,f.(n+1)] from RecEx(A1,A2);
  take f;
  thus dom f = NAT & f.0 = A() by A3;
  thus thesis by A3;
end;

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)
proof
  defpred P[set,set,set] means $3=G($1,$2);
  A1: for n being Nat for x being Element of D()
        ex y being Element of D() st P[n,x,y];
  consider f being Function of NAT,D() such that A2: f.0 = A() &
   for n being Element of NAT holds P[n,f.n,f.(n+1)] from RecExD(A1);
  take f;
  thus f.0 = A() by A2;
  thus for n being (Element of NAT) holds f.(n+1) = G(n,f.n) by A2;
end;

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
   A1: for n being Nat st 1 <= n & n < N()
          for x being set ex y being set st P[n,x,y] and
   A2: 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
proof
  defpred Q[Nat,set,set] means ($1 < N()-1 implies P[$1+1,$2,$3]) &
       (not $1 < N()-1 implies $3=0);

  A3: for n being Nat for x being set ex y being set st Q[n,x,y]
      proof let n be Nat,x be set;
           n < N()-1 implies thesis
              proof assume A4: n < N()-1;
                then A5:             n+1 < N() by REAL_1:86;
                  1 <= n+1 by NAT_1:29;
                then consider y such that A6: P[n+1,x,y] by A1,A5;
                take y;
                thus n < N()-1 implies P[n+1,x,y] by A6;
                thus thesis by A4;
              end;
          hence thesis;
      end;
  A7: for n being Nat for x,y1,y2 being set st Q[n,x,y1] & Q[n,x,y2]
      holds y1 = y2
      proof let n be Nat,x,y1,y2 be set;
        assume A8: (n < N()-1 implies P[n+1,x,y1]) &
       (not n < N()-1 implies y1=0) &
       (n < N()-1 implies P[n+1,x,y2]) &
       (not n < N()-1 implies y2=0);

          n < N()-1 implies thesis
            proof assume n < N()-1;
              then A9:            n+1 < N() by REAL_1:86;
                 1 <= n+1 by NAT_1:29;
              hence y1 = y2 by A2,A8,A9;
            end;
         hence thesis by A8;
      end;
    consider f being Function such that A10: dom f = NAT & f.0 = A() &
       for n being Element of NAT holds Q[n,f.n,f.(n+1)] from RecEx(A3,A7);
    defpred Q[set,set] means for r being Real st r=$1 holds $2=f.(r-1);
    A11: for x st x in REAL ex y st Q[x,y]
      proof let x; assume x in REAL;
        then reconsider r=x as Real;
        take f.(r-1);
        thus thesis;
      end;
    A12: for x,y1,y2 st x in REAL & Q[x,y1] & Q[x,y2]
         holds y1 = y2
       proof let x,y1,y2; assume A13: x in REAL &
             (for r being Real st r=x holds y1=f.(r-1)) &
             (for r being Real st r=x holds y2=f.(r-1));
           then reconsider r = x as Real;
           thus y1 = f.(r-1) by A13 .= y2 by A13;
       end;

    consider g being Function such that A14: dom g = REAL &
       for x st x in REAL  holds Q[x,g.x] from FuncEx(A12,A11);
      Seg N() c= REAL by XBOOLE_1:1;
   then A15: dom (g|Seg N()) = Seg N() by A14,RELAT_1:91;
   then reconsider p = g|Seg N() as FinSequence by FINSEQ_1:def 2;
   take p;

   A16: for n being Nat st n < N() holds p.(n+1) = f.n
     proof let n be Nat such that A17: n < N();
       A18: 1 <= n+1 by NAT_1:29;
          n+1 <= N() by A17,NAT_1:38;
then A19:        n+1 in Seg N() by A18,FINSEQ_1:3;

          g.(n+1) = f.(n+1-1) by A14
        .= f.(n+(1-1)) by XCMPLX_1:29
        .= f.n;
       hence thesis by A19,FUNCT_1:72;
     end;

   thus len p = N() by A15,FINSEQ_1:def 3;
   thus p.1 = A() or N() = 0
      proof
              N() <> 0 implies thesis
              proof assume N() <> 0;
                 then consider k such that A20: N() = k+1 by NAT_1:22;
                   0 <= k by NAT_1:18;
                 then 0 + 1 <= k +1 by REAL_1:55;
                 then 1 in Seg N() by A20,FINSEQ_1:3;
                then p.1 = g.1 by FUNCT_1:72
                  .= f.(1-1) by A14
                  .= A() by A10;
                hence thesis;
              end;
           hence thesis;
      end;

   let n; assume A21: 1 <= n & n < N();
    then 0 <> n;
    then consider k such that A22: n = k+1 by NAT_1:22;
      k < N()-1 by A21,A22,REAL_1:86;
    then P[k+1,f.k,f.(k+1)] by A10;
  then A23: P[k+1,f.k,p.(k+1+1)] by A16,A21,A22;
      k <= k+1 by NAT_1:29;
    then k < N() by A21,A22,AXIOMS:22;
   hence P[n,p.n,p.(n+1)] by A16,A22,A23;
end;

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
A1: 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]
proof
  consider 00 being Element of D();
  defpred Z[Nat,set,set] means ($1 < N()-1 implies P[$1+1,$2,$3]) &
       (not $1 < N()-1 implies $3=00);
  A2: for n being Nat for x being Element of D() ex y being Element of D() st
            Z[n,x,y]
      proof let n be Nat,x be Element of D();
            n < N()-1 implies thesis
              proof assume A3: n < N()-1;
                then 1 <= n+1 & n+1 < N() by NAT_1:29,REAL_1:86;
                then consider y being Element of D() such that A4: P[n+1,x,y]
by A1;
                take y;
                thus n < N()-1 implies P[n+1,x,y] by A4;
                thus thesis by A3;
              end;
          hence thesis;
      end;
    consider f being Function of NAT,D() such that A5: f.0 = A() &
       for n being Element of NAT holds Z[n,f.n,f.(n+1)] from RecExD(A2);
    defpred P[set,set] means for r being Real st r = $1
            holds $2 = f.(r-1);
    A6: for x st x in REAL ex y st P[x,y]
      proof let x; assume x in REAL;
        then reconsider r=x as Real;
        take f.(r-1);
        thus thesis;
      end;
    A7: for x,y1,y2 st x in REAL & P[x,y1] & P[x,y2] holds y1 = y2
       proof let x,y1,y2; assume A8: x in REAL &
             (for r being Real st r=x holds y1=f.(r-1)) &
             (for r being Real st r=x holds y2=f.(r-1));
           then reconsider r = x as Real;
           thus y1 = f.(r-1) by A8 .= y2 by A8;
       end;
    consider g being Function such that A9: dom g = REAL &
       for x st x in REAL holds P[x,g.x] from FuncEx(A7,A6);
      Seg N() c= REAL by XBOOLE_1:1;
   then A10: dom (g|Seg N()) = Seg N() by A9,RELAT_1:91;
   then reconsider p = g|Seg N() as FinSequence by FINSEQ_1:def 2;
     rng p c= D()
     proof let x; assume x in rng p;
       then consider y such that A11: y in dom p & x = p.y by FUNCT_1:def 5;
       reconsider y as Nat by A11;
    A12: f.(y-1) in D()
          proof
               y <> 0 by A10,A11,FINSEQ_1:3;
             then consider k such that A13: y = k+1 by NAT_1:22;
                f.k in D();
           hence f.(y-1) in D() by A13,XCMPLX_1:26;
          end;

       p.y = g.y by A11,FUNCT_1:70;
      hence thesis by A9,A11,A12;
     end;
   then reconsider p as FinSequence of D() by FINSEQ_1:def 4;
   take p;

   A14: for n being Nat st n < N() holds p.(n+1) = f.n
     proof let n be Nat such that A15: n < N();
       A16: 1 <= n+1 by NAT_1:29;
          n+1 <= N() by A15,NAT_1:38;
then A17:        n+1 in Seg N() by A16,FINSEQ_1:3;

          g.(n+1) = f.(n+1-1) by A9
        .= f.(n+(1-1)) by XCMPLX_1:29
        .= f.n;
       hence thesis by A17,FUNCT_1:72;
     end;

   thus len p = N() by A10,FINSEQ_1:def 3;
   thus p.1 = A() or N() = 0
      proof
              N() <> 0 implies thesis
              proof assume N() <> 0;
                 then consider k such that A18: N() = k+1 by NAT_1:22;
                   0 <= k by NAT_1:18;
                 then 0 + 1 <= k +1 by REAL_1:55;
                 then 1 in Seg N() by A18,FINSEQ_1:3;
                then p.1 = g.1 by FUNCT_1:72
                  .= f.(1-1) by A9
                  .= A() by A5;
                hence thesis;
              end;
           hence thesis;
      end;

   let n; assume A19: 1 <= n & n < N();
    then 0 <> n;
    then consider k such that A20: n = k+1 by NAT_1:22;
      k < N() - 1 by A19,A20,REAL_1:86;
    then P[k+1,f.k,f.(k+1)] by A5;
  then A21: P[k+1,f.k,p.(k+1+1)] by A14,A19,A20;
      k <= k+1 by NAT_1:29;
    then k < N() by A19,A20,AXIOMS:22;
   hence P[n,p.n,p.(n+1)] by A14,A20,A21;
end;

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
A1: for k,x st 1 <= k & k < len S() ex y st P[S().(k+1),x,y] and
A2: 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
proof
  defpred Q[Nat,set,set] means P[S().($1+1),$2,$3];
  A3: for k st 1 <= k & k < len S()
           for x ex y st Q[k,x,y] by A1;
  A4: for k st 1 <= k & k < len S() for x,y1,y2 st
           Q[k,x,y1] & Q[k,x,y2] holds y1 = y2 by A2;
  consider p such that A5: len p = len S() & (p.1 = S().1 or len S() = 0) &
     for k st 1 <= k & k < len S() holds Q[k,p.k,p.(k+1)]
       from FinRecEx(A3,A4);

  A6: len S() <> 0 implies thesis
       proof assume A7: len S() <> 0;
          take p.(len p),p;
          thus p.(len p) = p.(len p) & len p = len S() & p.1 = S().1 by A5,A7;
          let k;
          assume 1 <= k & k < len S();
         hence thesis by A5;
       end;
    len S() = 0 implies thesis
      proof assume A8: len S() = 0;
       take S().0,S();
       thus S().0 = S().(len S()) & len S() = len S() & S().1 = S(). 1 by A8;
       thus thesis by A8,AXIOMS:22;
      end;
  hence thesis by A6;
end;

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)
proof
  defpred P[set,set,set] means $3 = F($1,$2);
  A1: for k,x st 1 <= k & k < len S() ex y st P[S().(k+1),x,y];
  A2: 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;

  consider x such that A3: ex p 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)] from SeqBinOpEx(A1,A2);
  take x;
  consider p such that A4: 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) by A3;
  take p;
  thus x = p.(len p) & len p = len S() & p.1 = S().1 by A4;
  let k; assume 1 <= k & k < len S();
  hence p.(k+1) = F(S().(k+1),p.k) by A4;
end;

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

scheme RecUn{A() -> set, F, G() -> Function, P[set,set,set]}:
  F() = G()
provided
A1: dom F() = NAT & F().0 = A() & for n holds P[n,F().n,F().(n+1)] and
A2: dom G() = NAT & G().0 = A() & for n holds P[n,G().n,G().(n+1)] and
A3: for n for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2
proof
  defpred P[Nat] means F().$1 = G().$1;
  A4: P[0] by A1,A2;
  A5: for n st P[n] holds P[n+1]
      proof let n; assume F().n = G().n;
         then P[n,F().n,F().(n+1)] & P[n,F().n,G().(n+1)] by A1,A2;
        hence F().(n+1) = G().(n+1) by A3;
      end;
     for n holds P[n] from Ind(A4,A5);
  then for x st x in NAT holds F().x = G().x;
 hence F() = G() by A1,A2,FUNCT_1:9;
end;

scheme RecUnD{D() -> non empty set,A() -> Element of D(),
        P[set,set,set], F, G() -> Function of NAT,D()} : F() = G()
 provided
  A1: F().0 = A() & (for n holds P[n,F().n,F().(n+1)]) and
  A2: G().0 = A() & (for n holds P[n,G().n,G().(n+1)]) and
  A3: for n being Nat,x,y1,y2 being Element of D()
         st P[n,x,y1] & P[n,x,y2] holds y1=y2
proof
  assume A4: F() <> G();
  A5: dom F() = NAT by FUNCT_2:def 1;
     dom G() = NAT by FUNCT_2:def 1;
  then consider x such that A6: x in NAT & F().x <> G().x by A4,A5,FUNCT_1:9;
  defpred Q[Nat] means F().$1 <> G().$1;
  A7: ex k st Q[k] by A6;
  consider m such that A8: Q[m] &
      for n st Q[n] holds m <= n from Min(A7);

    now assume m<>0;
     then consider k such that A9: m=k+1 by NAT_1:22;
       k < m by A9,NAT_1:38;
     then A10: F().k = G().k by A8;
       P[k,F().k,F().(k+1)] & P[k,G().k,G().(k+1)] by A1,A2;
   hence contradiction by A3,A8,A9,A10;
  end;
 hence contradiction by A1,A2,A8;
end;

scheme LambdaRecUn{A() -> set, RecFun(set,set) -> set,
        F, G() -> Function}:
  F() = G()
  provided
  A1: dom F() = NAT & F().0 = A() &
        for n holds F().(n+1) = RecFun(n,F().n) and
  A2: dom G() = NAT & G().0 = A() &
        for n holds G().(n+1) = RecFun(n,G().n)
proof
  defpred P[Nat,set,set] means $3=RecFun($1,$2);
  A3: dom F() = NAT & F().0 = A() & for n holds P[n,F().n,F().(n+1)]
 by A1;
  A4: dom G() = NAT & G().0 = A() & for n holds P[n,G().n,G().(n+1)]
 by A2;
  A5: for n being Nat,x,y1,y2 being set
        st P[n,x,y1] & P[n,x,y2] holds y1=y2;
  thus F() = G() from RecUn(A3,A4,A5);
end;

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
  A1: F().0 = A() & for n holds F().(n+1) = RecFun(n,F().n) and
  A2: G().0 = A() & for n holds G().(n+1) = RecFun(n,G().n)
proof
  defpred P[Nat,set,set] means $3=RecFun($1,$2);
  A3: F().0 = A() & for n holds P[n,F().n,F().(n+1)] by A1;
  A4: G().0 = A() & for n holds P[n,G().n,G().(n+1)] by A2;
  A5: for n being Nat,x,y1,y2 being Element of D()
        st P[n,x,y1] & P[n,x,y2] holds y1=y2;
  thus F() = G() from RecUnD(A3,A4,A5);
end;

scheme LambdaRecUnR{A() -> Real, RecFun(set,set) -> set,
   F, G() -> Function of NAT,REAL}:
 F() = G()
 provided
A1: F().0 = A() & for n holds F().(n+1) = RecFun(n,F().n) and
A2: G().0 = A() & for n holds G().(n+1) = RecFun(n,G().n)
proof
  defpred P[Nat,set,set] means $3=RecFun($1,$2);
  A3: F().0 = A() & for n holds P[n,F().n,F().(n+1)] by A1;
  A4: G().0 = A() & for n holds P[n,G().n,G().(n+1)] by A2;
  A5: for n being Nat,x,y1,y2 being Element of REAL
        st P[n,x,y1] & P[n,x,y2] holds y1=y2;
  thus F() = G() from RecUnD(A3,A4,A5);
end;

scheme FinRecUn{A() -> set,N() -> Nat,
       F, G() -> FinSequence, P[set,set,set]}:
  F() = G()
provided
A1: 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
A2: 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
A3: len G() = N() & (G().1 = A() or N() = 0) &
    for n st 1 <= n & n < N() holds P[n,G().n,G().(n+1)]
proof
   A4: dom F() = Seg len G() by A2,A3,FINSEQ_1:def 3
              .= dom G() by FINSEQ_1:def 3;
   assume F() <> G();
   then consider x such that A5: x in dom F() & F().x <> G().x by A4,FUNCT_1:9;
   A6: x in Seg len F() by A5,FINSEQ_1:def 3;
   reconsider x as Nat by A5;
   defpred P[Nat] means 1 <= $1 & $1 <= N() & F().$1 <> G().$1;
   1 <= x & x <= N() by A2,A6,FINSEQ_1:3;
   then A7: ex n st P[n] by A5;
   consider n such that A8: P[n]&
       for k st P[k] holds n <= k from Min(A7);
       n <> 1 by A2,A3,A8;
then A9:    1 < n by A8,REAL_1:def 5;
     0 <> n by A8;
   then consider k such that A10: n = k+1 by NAT_1:22;
   A11: 1 <= k by A9,A10,NAT_1:38;
       k < n by A10,REAL_1:69;
   then A12: k < N() by A8,AXIOMS:22;
         n > k by A10,NAT_1:38;
    then F().k = G().k by A8,A11,A12;
    then P[k,F().k,F().(k+1)] & P[k,F().k,G().(k+1)] by A2,A3,A11,A12;
   hence contradiction by A1,A8,A10,A11,A12;
end;

scheme FinRecUnD{D() -> non empty set, A() -> Element of D(), N() -> Nat,
    F, G() -> FinSequence of D(), P[set,set,set]}:
  F() = G()
provided
A1: 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
A2: 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
A3: len G() = N() & (G().1 = A() or N() = 0) &
    for n st 1 <= n & n < N() holds P[n,G().n,G().(n+1)]
proof
   A4: dom F() = Seg len G() by A2,A3,FINSEQ_1:def 3
      .= dom G() by FINSEQ_1:def 3;
   assume F() <> G();
   then consider x such that A5: x in dom F() & F().x <> G().x by A4,FUNCT_1:9;
   A6: x in Seg len F() by A5,FINSEQ_1:def 3;
   reconsider x as Nat by A5;
   defpred P[Nat] means 1 <= $1 & $1 <= N() & F().$1 <> G().$1;
   1 <= x & x <= N() by A2,A6,FINSEQ_1:3;
   then A7: ex n st P[n] by A5;
   consider n such that A8: P[n] &
       for k st P[k] holds n <= k from Min(A7);
       n <> 1 by A2,A3,A8;
then A9:    1 < n by A8,REAL_1:def 5;
     0 <> n by A8;
   then consider k such that A10: n = k+1 by NAT_1:22;
   A11: 1 <= k by A9,A10,NAT_1:38;
       k < n by A10,REAL_1:69;
   then A12: k < N() by A8,AXIOMS:22;
         n > k by A10,NAT_1:38;
   then A13: F().k = G().k by A8,A11,A12;
    reconsider Fk = F().k as Element of D() by A2,A11,A12,Lm1;
    reconsider Fk1 = F().(k+1) as Element of D() by A2,A8,A10,Lm1;
    reconsider Gk1 = G().(k+1) as Element of D() by A3,A8,A10,Lm1;
      P[k,Fk,Fk1] & P[k,Fk,Gk1] by A2,A3,A11,A12,A13;
   hence contradiction by A1,A8,A10,A11,A12;
end;

scheme SeqBinOpUn{S() -> FinSequence,P[set,set,set],x, y() -> set}:
  x() = y()
provided
A1: 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
A2: 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
A3: 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)]
proof
 defpred Q[Nat,set,set] means P[S().($1+1),$2,$3];
 A4: for k st 1 <= k & k < len S() for x,y1,y2 st
         Q[k,x,y1] & Q[k,x,y2] holds y1 = y2 by A1;
 consider p such that A5: x() = p.(len p) & len p = len S() & p.1 = S().1 &
      for k st 1 <= k & k < len S() holds Q[k,p.k,p.(k+1)] by A2;
 consider q such that A6: y() = q.(len q) & len q = len S() & q.1 = S().1 &
      for k st 1 <= k & k < len S() holds Q[k,q.k,q.(k+1)] by A3;
 A7: len p = len S() & (p.1 = S().1 or len S() = 0) &
      for k st 1 <= k & k < len S() holds Q[k,p.k,p.(k+1)] by A5;
 A8: len q = len S() & (q.1 = S().1 or len S() = 0) &
      for k st 1 <= k & k < len S() holds Q[k,q.k,q.(k+1)] by A6;
    p = q from FinRecUn(A4,A7,A8);
   hence x() = y() by A5,A6;
end;

scheme LambdaSeqBinOpUn{S() -> FinSequence, F(set,set) -> set,
                          x, y() -> set}:
  x() = y()
provided
A1: 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
A2: 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)
proof
  defpred P[set,set,set] means $3 = F($1,$2);
  A3: 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;
  A4: ex p 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)] by A1;
  A6: ex p 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)] by A2;
  thus x() = y() from SeqBinOpUn(A3,A4,A6);
end;
           :::::::::::::::::::::::::::::::
::   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

A1: for n,x ex y st P[n,x,y] and
A2: for n,x,y1,y2 st P[n,x,y1] & P[n,x,y2] holds y1 = y2
proof
  defpred Q[set,set,set] means P[$1,$2,$3];
  A3: for n,x ex y st Q[n,x,y] by A1;
  A4: for n,x,y1,y2 st Q[n,x,y1] & Q[n,x,y2] holds y1 = y2 by A2;
  consider f being Function such that A5: dom f = NAT & f.0 = A() &
    for n being Element of NAT holds Q[n,f.n,f.(n+1)] from RecEx(A3,A4);
 thus
     (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)])
 proof
  take f.n(),f;
  thus f.n() = f.n() & dom f = NAT & f.0 = A() &
         for n holds P[n,f.n,f.(n+1)] by A5;
 end;
  let y1,y2 be set;
  given f1 being Function such that A6: y1 = f1.n() & dom f1 = NAT &
    f1.0 = A() & for n holds Q[n,f1.n,f1.(n+1)];
  given f2 being Function such that A7: y2 = f2.n() & dom f2 = NAT &
    f2.0 = A() & for n holds Q[n,f2.n,f2.(n+1)];
  A8: dom f1 = NAT & f1.0 = A() & for n holds Q[n,f1.n,f1.(n+1)] by A6;
  A9: dom f2 = NAT & f2.0 = A() & for n holds Q[n,f2.n,f2.(n+1)] by A7;
     f1 = f2 from RecUn(A8,A9,A4);
  hence y1 = y2 by A6,A7;
end;

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
proof
  defpred P[set,set,set] means for z st z = $2 holds $3 = RecFun($1,z);
  A1: for n,x ex y st P[n,x,y]
      proof let n,x; take RecFun(n,x);let z; assume z = x;
        hence thesis;
      end;
  A2: for n,x,y1,y2 st P[n,x,y1] & P[n,x,y2] holds y1 = y2
       proof let n,x,y1,y2; assume A3:
         (for z st z = x holds y1 = RecFun(n,z)) &
          for z st z = x holds y2 = RecFun(n,z);
         hence y1 = RecFun(n,x) .= y2 by A3;
       end;
X:   (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 from DefRec(A1,A2);
   then consider y being set, f being Function such that
W1:  y = f.n() & dom f = NAT & f.0 = A() and
W2:  for n holds  P[n,f.n,f.(n+1)];
  thus 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)
  proof take y,f;
   thus thesis by W1,W2;
  end;
   let y1,y2 being set;
   given f1 being Function such that
G1:     y1 = f1.n() & dom f1 = NAT & f1.0 = A() &
       for n holds f1.(n+1) = RecFun(n,f1.n);
   given f2 being Function such that
G2:     y2 = f2.n() & dom f2 = NAT & f2.0 = A() &
       for n holds f2.(n+1) = RecFun(n,f2.n);
A: for n holds P[n,f1.n,f1.(n+1)] by G1;
   for n holds P[n,f2.n,f2.(n+1)] by G2;
  hence y1 = y2 by X,G1,G2,A;
end;

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
A1: for n being Nat,x being Element of D()
      ex y being Element of D() st P[n,x,y] and
A2: for n being Nat, x,y1,y2 being Element of D()
      st P[n,x,y1] & P[n,x,y2] holds y1 = y2
proof
  defpred Q[set,set,set] means P[$1,$2,$3];
  A3: for n being Nat,x being Element of D()
      ex y being Element of D() st Q[n,x,y] by A1;
  consider f being Function of NAT,D() such that A4: f.0 = A() &
    for n being Element of NAT holds Q[n,f.n,f.(n+1)] from RecExD(A3);
thus
     (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)])
 proof
  take f.n(),f;
  thus f.n() = f.n() & f.0 = A() &
         for n holds P[n,f.n,f.(n+1)] by A4;
 end;
A5: for n being Nat, x,y1,y2 being Element of D()
      st Q[n,x,y1] & Q[n,x,y2] holds y1 = y2 by A2;
  let y1,y2 be Element of D();
  given f1 being Function of NAT,D() such that A6: y1 = f1.n() &
    f1.0 = A() & for n holds Q[n,f1.n,f1.(n+1)];
  given f2 being Function of NAT,D() such that A7: y2 = f2.n() &
    f2.0 = A() & for n holds Q[n,f2.n,f2.(n+1)];
  A8: f1.0 = A() & for n holds Q[n,f1.n,f1.(n+1)] by A6;
  A9: f2.0 = A() & for n holds Q[n,f2.n,f2.(n+1)] by A7;
     f1 = f2 from RecUnD(A8,A9,A5);
  hence y1 = y2 by A6,A7;
end;

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
proof
  defpred Q[set,set,set] means for z being Element of D() st
       z=$2 holds $3 = RecFun($1,z);
  A1: for n being Nat,x being Element of D()
        ex y being Element of D() st Q[n,x,y]
       proof let n be Nat,x be Element of D();take RecFun(n,x);
          let z be Element of D();
         assume z = x; hence thesis;
       end;
  A2: for n being Nat,x,y1,y2 being Element of D()
        st Q[n,x,y1] & Q[n,x,y2]
       holds y1 = y2
      proof let n be Nat,x,y1,y2 be Element of D();assume A3:
        (for z being Element of D() st z = x holds y1 = RecFun(n,z)) &
         for z being Element of D() st z = x holds y2 = RecFun(n,z);
        hence y1 = RecFun(n,x) .= y2 by A3;
      end;
X:   (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 Q[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 being Nat holds Q[n,f.n,f.(n+1)]) &
     (ex f being Function of NAT,D() st
     y2 = f.n() & f.0 = A() &
       for n being Nat holds Q[n,f.n,f.(n+1)])
    holds y1 = y2 from DefRecD(A1,A2);
     then
      consider y being Element of D(), f being Function of NAT,D() such that
W1:    y = f.n() & f.0 = A() and
W2:    for n being Nat holds Q[n,f.n,f.(n+1)];
    thus 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)
     proof
      take y,f;
      thus thesis by W1,W2;
     end;
    let y1,y2 being Element of D();
    given f being Function of NAT,D() such that
G1:  y1 = f.n() & f.0 = A() &
       for n being Nat holds f.(n+1) = RecFun(n,f.n);
    given f2 being Function of NAT,D() such that
G2:   y2 = f2.n() & f2.0 = A() &
       for n being Nat holds f2.(n+1) = RecFun(n,f2.n);
A: for n being Nat holds Q[n,f.n,f.(n+1)] by G1;
   for n being Nat holds Q[n,f2.n,f2.(n+1)] by G2;
  hence y1 = y2 by X,A,G1,G2;
end;

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
A1: for k,y st 1 <= k & k < len S() ex z st P[S().(k+1),y,z] and
A2: 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
proof
  defpred Q[set,set,set] means P[$1,$2,$3];
A3: for k,y st 1 <= k & k < len S() ex z st Q[S().(k+1),y,z] by A1;
A4: for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) &
          Q[z,x,y1] & Q[z,x,y2] holds y1 = y2 by A2;
  thus
    (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
        Q[S().(k+1),p.k,p.(k+1)]) from SeqBinOpEx(A3,A4);
  let x,y;
  assume A5: 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
        Q[S().(k+1),p.k,p.(k+1)];
  assume A6: 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
        Q[S().(k+1),p.k,p.(k+1)];
  thus x = y from SeqBinOpUn(A4,A5,A6);
end;

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
proof
  deffunc G(set,set)= F($1,$2);
  thus
     (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) = G(S().(k+1),p.k)) from LambdaSeqBinOpEx;
  let x,y;
  assume A1: 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) = G(S().(k+1),p.k);
  assume A2: 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) = G(S().(k+1),p.k);
  thus x = y from LambdaSeqBinOpUn(A1,A2);
end;

Back to top