comput_1.miz

    begin

    reserve i,j,k,c,m,n for Element of NAT ,

a,x,y,z,X,Y for set,

D,E for non empty set,

R for Relation,

f,g for Function,

p,q for FinSequence;

    theorem :: COMPUT_1:1



     Th1: ( <*x, y*> +* (1,z)) = <*z, y*> & ( <*x, y*> +* (2,z)) = <*x, z*>

    proof

      set a = ( <*x, y*> +* (1,z)), b = ( <*x, y*> +* (2,z));

      ( <*x, y*> . 1) = x by FINSEQ_1: 44;

      then

       A1: (b . 1) = x by FUNCT_7: 32;

      ( <*x, y*> . 2) = y by FINSEQ_1: 44;

      then

       A2: (a . 2) = y by FUNCT_7: 32;



       A3: ( len <*x, y*>) = 2 by FINSEQ_1: 44;

      then 1 in ( dom <*x, y*>) by FINSEQ_3: 25;

      then

       A4: (a . 1) = z by FUNCT_7: 31;

      ( len a) = 2 by A3, FUNCT_7: 97;

      hence ( <*x, y*> +* (1,z)) = <*z, y*> by A4, A2, FINSEQ_1: 44;

      2 in ( dom <*x, y*>) by A3, FINSEQ_3: 25;

      then

       A5: (b . 2) = z by FUNCT_7: 31;

      ( len b) = 2 by A3, FUNCT_7: 97;

      hence thesis by A1, A5, FINSEQ_1: 44;

    end;

    theorem :: COMPUT_1:2



     Th2: (f +* (a,x)) = (g +* (a,y)) implies (f +* (a,z)) = (g +* (a,z))

    proof

      set i = a;

      assume

       A1: (f +* (i,x)) = (g +* (i,y));



       A2: ( dom (g +* (i,z))) = ( dom g) by FUNCT_7: 30;



       A3: ( dom (g +* (i,y))) = ( dom g) by FUNCT_7: 30;



       A4: ( dom (f +* (i,x))) = ( dom f) by FUNCT_7: 30;

      now

        thus ( dom (f +* (i,z))) = ( dom f) by FUNCT_7: 30;

        thus ( dom (g +* (i,z))) = ( dom f) by A1, A3, A2, FUNCT_7: 30;

        let a be object;

        assume

         A5: a in ( dom f);

        per cases ;

          suppose

           A6: a = i;



          hence ((f +* (i,z)) . a) = z by A5, FUNCT_7: 31

          .= ((g +* (i,z)) . a) by A1, A4, A3, A5, A6, FUNCT_7: 31;

        end;

          suppose

           A7: a <> i;



          hence ((f +* (i,z)) . a) = (f . a) by FUNCT_7: 32

          .= ((g +* (i,y)) . a) by A1, A7, FUNCT_7: 32

          .= (g . a) by A7, FUNCT_7: 32

          .= ((g +* (i,z)) . a) by A7, FUNCT_7: 32;

        end;

      end;

      hence thesis;

    end;

    theorem :: COMPUT_1:3



     Th3: for i be Nat holds ( Del ((p +* (i,x)),i)) = ( Del (p,i))

    proof

      let i be Nat;

      set f = p;

      per cases ;

        suppose

         A1: i in ( dom f);

        then

         A2: i <= ( len f) by FINSEQ_3: 25;

        1 <= i by A1, FINSEQ_3: 25;

        then

        consider j be Nat such that

         A3: ( len f) = (j + 1) by A2, NAT_1: 6;

        reconsider j as Element of NAT by ORDINAL1:def 12;



         A4: ( dom (f +* (i,x))) = ( dom f) by FUNCT_7: 30;

        then

         A5: ( len (f +* (i,x))) = ( len f) by FINSEQ_3: 29;

        then ( len ( Del ((f +* (i,x)),i))) = j by A1, A3, A4, FINSEQ_3: 109;

        then

         A6: ( dom ( Del ((f +* (i,x)),i))) = ( Seg j) by FINSEQ_1:def 3;

        now

          thus ( len ( Del ((f +* (i,x)),i))) = j by A1, A3, A4, A5, FINSEQ_3: 109;

          thus ( len ( Del (f,i))) = j by A1, A3, FINSEQ_3: 109;

          let a be Nat;

          assume a in ( dom ( Del ((f +* (i,x)),i)));

          then

           A7: a <= j by A6, FINSEQ_1: 1;

          per cases ;

            suppose

             A8: a < i;



            hence (( Del ((f +* (i,x)),i)) . a) = ((f +* (i,x)) . a) by FINSEQ_3: 110

            .= (f . a) by A8, FUNCT_7: 32

            .= (( Del (f,i)) . a) by A8, FINSEQ_3: 110;

          end;

            suppose

             A9: i <= a;

            then

             A10: i < (a + 1) by NAT_1: 13;



            thus (( Del ((f +* (i,x)),i)) . a) = ((f +* (i,x)) . (a + 1)) by A1, A3, A4, A5, A7, A9, FINSEQ_3: 111

            .= (f . (a + 1)) by A10, FUNCT_7: 32

            .= (( Del (f,i)) . a) by A1, A3, A7, A9, FINSEQ_3: 111;

          end;

        end;

        hence thesis by FINSEQ_2: 9;

      end;

        suppose not i in ( dom f);

        hence thesis by FUNCT_7:def 3;

      end;

    end;

    theorem :: COMPUT_1:4



     Th4: (p +* (i,a)) = (q +* (i,a)) implies ( Del (p,i)) = ( Del (q,i))

    proof

      set x = p, y = q;

      assume

       A1: (x +* (i,a)) = (y +* (i,a));

      set xi = (x +* (i,a)), yi = (y +* (i,a));

      set dx = ( Del (x,i)), dy = ( Del (y,i));



       A2: ( dom xi) = ( dom x) by FUNCT_7: 30;



       A3: ( dom yi) = ( dom y) by FUNCT_7: 30;



       A4: ( Seg ( len y)) = ( dom y) by FINSEQ_1:def 3;



       A5: ( Seg ( len x)) = ( dom x) by FINSEQ_1:def 3;

      per cases ;

        suppose

         A6: i in ( dom x);



         A7: ( dom ( Del (x,i))) = ( Seg ( len dx)) by FINSEQ_1:def 3;

        now

          thus ( len dx) = ( len dx);

          x <> {} by A6;

          then

          consider m be Nat such that

           A8: ( len x) = (m + 1) by NAT_1: 6;

          reconsider m as Element of NAT by ORDINAL1:def 12;



           A9: ( len dx) = m by A6, A8, FINSEQ_3: 109;

          hence ( len dy) = ( len dx) by A1, A2, A3, A5, A4, A6, A8, FINSEQ_1: 6, FINSEQ_3: 109;

          let j be Nat;

          assume j in ( dom ( Del (x,i)));

          then

           A10: j <= m by A7, A9, FINSEQ_1: 1;

          per cases ;

            suppose

             A11: j < i;



            hence (dx . j) = (x . j) by FINSEQ_3: 110

            .= (yi . j) by A1, A11, FUNCT_7: 32

            .= (y . j) by A11, FUNCT_7: 32

            .= (dy . j) by A11, FINSEQ_3: 110;

          end;

            suppose

             A12: i <= j;

            then

             A13: (j + 1) > i by NAT_1: 13;



            thus (dx . j) = (x . (j + 1)) by A6, A8, A10, A12, FINSEQ_3: 111

            .= (yi . (j + 1)) by A1, A13, FUNCT_7: 32

            .= (y . (j + 1)) by A13, FUNCT_7: 32

            .= (dy . j) by A1, A2, A3, A5, A4, A6, A8, A10, A12, FINSEQ_1: 6, FINSEQ_3: 111;

          end;

        end;

        hence thesis by FINSEQ_2: 9;

      end;

        suppose

         A14: not i in ( dom x);

        then xi = x by FUNCT_7:def 3;

        hence thesis by A1, A3, A14, FUNCT_7:def 3;

      end;

    end;

    theorem :: COMPUT_1:5



     Th5: ( 0 -tuples_on X) = { {} }

    proof

      set S = { s where s be Element of (X * ) : ( len s) = 0 };

      now

        let x be object;

        hereby

          assume x in S;

          then

          consider s be Element of (X * ) such that

           A1: x = s and

           A2: ( len s) = 0 ;

          s = {} by A2;

          hence x in { {} } by A1, TARSKI:def 1;

        end;

        assume x in { {} };

        then

         A3: x = {} by TARSKI:def 1;

        ( <*> (X * )) is Element of (X * ) by FINSEQ_1: 49;

        hence x in S by A3, CARD_1: 27;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: COMPUT_1:6

    n <> 0 implies (n -tuples_on {} ) = {}

    proof

      assume that

       A1: n <> 0 and

       A2: (n -tuples_on {} ) <> {} ;

      consider x be object such that

       A3: x in (n -tuples_on {} ) by A2;

      ex s be Element of ( {} * ) st s = x & ( len s) = n by A3;

      hence contradiction by A1;

    end;

    theorem :: COMPUT_1:7



     Th7: for f be Function-yielding Function holds {} in ( rng f) implies <:f:> = {}

    proof

      let f be Function-yielding Function;



       A1: ( dom <:f:>) = ( meet ( doms f)) by FUNCT_6: 29

      .= ( meet ( rng ( doms f))) by FUNCT_6:def 4;

      assume {} in ( rng f);

      then

      consider x be object such that

       A2: x in ( dom f) and

       A3: (f . x) = {} by FUNCT_1:def 3;



       A4: ( dom ( doms f)) = ( dom f) by FUNCT_6:def 2;

      then

       A5: x in ( dom ( doms f)) by A2;

      then (( doms f) . x) = {} by A3, A4, FUNCT_6:def 2;

      hence thesis by A1, A5, FUNCT_1: 3, SETFAM_1: 4;

    end;

    theorem :: COMPUT_1:8



     Th8: ( rng f) = D implies ( rng <: <*f*>:>) = (1 -tuples_on D)

    proof

      set X = D;



       A1: ( dom <: <*f*>:>) = ( dom f) by FINSEQ_3: 141;

      assume

       A2: ( rng f) = X;

      now

        let x be object;

        hereby

          assume x in ( rng <: <*f*>:>);

          then

          consider y be object such that

           A3: y in ( dom <: <*f*>:>) and

           A4: ( <: <*f*>:> . y) = x by FUNCT_1:def 3;

          reconsider fy = (f . y) as Element of X by A2, A1, A3, FUNCT_1: 3;



           A5: <*fy*> is Element of (1 -tuples_on X) by FINSEQ_2: 131;

          ( <: <*f*>:> . y) = <*(f . y)*> by A1, A3, FINSEQ_3: 141;

          hence x in (1 -tuples_on X) by A4, A5;

        end;

        assume x in (1 -tuples_on X);

        then x is Tuple of 1, X by FINSEQ_2: 131;

        then

        consider d be Element of X such that

         A6: x = <*d*> by FINSEQ_2: 97;

        consider y be object such that

         A7: y in ( dom f) and

         A8: (f . y) = d by A2, FUNCT_1:def 3;

        ( <: <*f*>:> . y) = <*d*> by A7, A8, FINSEQ_3: 141;

        hence x in ( rng <: <*f*>:>) by A1, A6, A7, FUNCT_1: 3;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: COMPUT_1:9



     Th9: 1 <= i & i <= (n + 1) implies for p be Element of ((n + 1) -tuples_on D) holds ( Del (p,i)) in (n -tuples_on D)

    proof

      set X = D;

      assume that

       A1: 1 <= i and

       A2: i <= (n + 1);

      let p be Element of ((n + 1) -tuples_on X);



       A3: ( len p) = (n + 1) by CARD_1:def 7;

      then i in ( dom p) by A1, A2, FINSEQ_3: 25;

      then

       A4: ( len ( Del (p,i))) = n by A3, FINSEQ_3: 109;

      ( Del (p,i)) is FinSequence of X by FINSEQ_3: 105;

      then ( Del (p,i)) is Element of (n -tuples_on X) by A4, FINSEQ_2: 92;

      hence thesis;

    end;

    begin

    definition

      let X be set;

      :: COMPUT_1:def1

      attr X is compatible means

      : Def1: for f,g be Function st f in X & g in X holds f tolerates g;

    end

    registration

      cluster non empty functional compatible for set;

      existence

      proof

        set A = { {} };

        take A;

        A is compatible

        proof

          let f,g be Function;

          assume that

           A1: f in A and g in A;

          f = {} by A1, TARSKI:def 1;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let X be functional compatible set;

      cluster ( union X) -> Function-like Relation-like;

      coherence

      proof

        thus ( union X) is Function-like

        proof

          let x,y1,y2 be object;

          assume that

           A1: [x, y1] in ( union X) and

           A2: [x, y2] in ( union X);

          consider f be set such that

           A3: [x, y1] in f and

           A4: f in X by A1, TARSKI:def 4;

          consider g be set such that

           A5: [x, y2] in g and

           A6: g in X by A2, TARSKI:def 4;

          reconsider f, g as Function by A4, A6;



           A7: y1 is set & y2 is set by TARSKI: 1;



           A8: x in ( dom f) by A3, XTUPLE_0:def 12;

          then

           A9: (f . x) = y1 by A3, FUNCT_1:def 2, A7;



           A10: x in ( dom g) by A5, XTUPLE_0:def 12;

          then

           A11: (g . x) = y2 by A5, FUNCT_1:def 2, A7;



           A12: x in (( dom f) /\ ( dom g)) by A8, A10, XBOOLE_0:def 4;

          f tolerates g by A4, A6, Def1;

          hence thesis by A9, A11, A12;

        end;

        thus ( union X) is Relation-like

        proof

          let x be object;

          assume x in ( union X);

          then ex f be set st x in f & f in X by TARSKI:def 4;

          hence thesis by RELAT_1:def 1;

        end;

      end;

    end

    ::$Canceled

    theorem :: COMPUT_1:11



     Th10: X is functional compatible iff ( union X) is Function

    proof

      now

        assume

         A1: ( union X) is Function;

        thus X is functional

        proof

          let f be object;

          assume

           A2: f in X;

          reconsider f as set by TARSKI: 1;



           A3: f is Function-like

          proof

            let x,y1,y2 be object;

            assume that

             A4: [x, y1] in f and

             A5: [x, y2] in f;



             A6: [x, y2] in ( union X) by A2, A5, TARSKI:def 4;

             [x, y1] in ( union X) by A2, A4, TARSKI:def 4;

            hence thesis by A1, A6, FUNCT_1:def 1;

          end;

          f is Relation-like

          proof

            let x be object;

            assume x in f;

            then x in ( union X) by A2, TARSKI:def 4;

            hence thesis by A1, RELAT_1:def 1;

          end;

          hence thesis by A3;

        end;

        thus X is compatible

        proof

          let f,g be Function such that

           A7: f in X and

           A8: g in X;

          let x be object;

          assume

           A9: x in (( dom f) /\ ( dom g));

          then

           A10: x in ( dom g) by XBOOLE_0:def 4;

          then

          consider y2 be object such that

           A11: [x, y2] in g by XTUPLE_0:def 12;



           A12: [x, y2] in ( union X) by A8, A11, TARSKI:def 4;



           A13: x in ( dom f) by A9, XBOOLE_0:def 4;

          then

          consider y1 be object such that

           A14: [x, y1] in f by XTUPLE_0:def 12;



           A15: y1 is set by TARSKI: 1;

           [x, y1] in ( union X) by A7, A14, TARSKI:def 4;

          then

           A16: y1 = y2 by A1, A12, FUNCT_1:def 1;



          thus (f . x) = y1 by A13, A14, FUNCT_1:def 2, A15

          .= (g . x) by A10, A11, A16, FUNCT_1:def 2, A15;

        end;

      end;

      hence thesis;

    end;

    registration

      let X,Y be set;

      cluster non empty compatible for PFUNC_DOMAIN of X, Y;

      existence

      proof

        set A = { {} };



         A1: A is compatible

        proof

          let f,g be Function;

          assume that

           A2: f in A and g in A;

          f = {} by A2, TARSKI:def 1;

          hence thesis;

        end;

        now

          let x be Element of A;

          x = {} by TARSKI:def 1;

          hence x is PartFunc of X, Y by XBOOLE_1: 2;

        end;

        then A is PFUNC_DOMAIN of X, Y by RFUNCT_3:def 3;

        hence thesis by A1;

      end;

    end

    theorem :: COMPUT_1:12



     Th11: for X be non empty functional compatible set holds ( dom ( union X)) = ( union the set of all ( dom f) where f be Element of X)

    proof

      let X be non empty functional compatible set;

      set F = the set of all ( dom f) where f be Element of X;

      now

        let x be object;

        hereby

          assume x in ( dom ( union X));

          then

          consider y be object such that

           A1: [x, y] in ( union X) by XTUPLE_0:def 12;

          consider Z be set such that

           A2: [x, y] in Z and

           A3: Z in X by A1, TARSKI:def 4;

          reconsider Z as Element of X by A3;



           A4: ( dom Z) in F;

          x in ( dom Z) by A2, XTUPLE_0:def 12;

          hence x in ( union F) by A4, TARSKI:def 4;

        end;

        assume x in ( union F);

        then

        consider Z be set such that

         A5: x in Z and

         A6: Z in F by TARSKI:def 4;

        consider f be Element of X such that

         A7: Z = ( dom f) by A6;

        consider y be object such that

         A8: [x, y] in f by A5, A7, XTUPLE_0:def 12;

         [x, y] in ( union X) by A8, TARSKI:def 4;

        hence x in ( dom ( union X)) by XTUPLE_0:def 12;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: COMPUT_1:13



     Th12: for X be functional compatible set, f be Function st f in X holds ( dom f) c= ( dom ( union X)) & for x be set st x in ( dom f) holds (( union X) . x) = (f . x)

    proof

      let X be functional compatible set, f be Function such that

       A1: f in X;

      thus ( dom f) c= ( dom ( union X))

      proof

        let x be object;

        assume x in ( dom f);

        then

        consider y be object such that

         A2: [x, y] in f by XTUPLE_0:def 12;

         [x, y] in ( union X) by A1, A2, TARSKI:def 4;

        hence thesis by XTUPLE_0:def 12;

      end;

      let x be set;

      assume x in ( dom f);

      then

      consider y be object such that

       A3: [x, y] in f by XTUPLE_0:def 12;

       [x, y] in ( union X) by A1, A3, TARSKI:def 4;



      hence (( union X) . x) = y by FUNCT_1: 1

      .= (f . x) by A3, FUNCT_1: 1;

    end;

    theorem :: COMPUT_1:14



     Th13: for X be non empty functional compatible set holds ( rng ( union X)) = ( union the set of all ( rng f) where f be Element of X)

    proof

      let X be non empty functional compatible set;

      set F = the set of all ( rng f) where f be Element of X;

      now

        let y be object;

        hereby

          assume y in ( rng ( union X));

          then

          consider x be object such that

           A1: [x, y] in ( union X) by XTUPLE_0:def 13;

          consider Z be set such that

           A2: [x, y] in Z and

           A3: Z in X by A1, TARSKI:def 4;

          reconsider Z as Element of X by A3;



           A4: ( rng Z) in F;

          y in ( rng Z) by A2, XTUPLE_0:def 13;

          hence y in ( union F) by A4, TARSKI:def 4;

        end;

        assume y in ( union F);

        then

        consider Z be set such that

         A5: y in Z and

         A6: Z in F by TARSKI:def 4;

        consider f be Element of X such that

         A7: Z = ( rng f) by A6;

        consider x be object such that

         A8: [x, y] in f by A5, A7, XTUPLE_0:def 13;

         [x, y] in ( union X) by A8, TARSKI:def 4;

        hence y in ( rng ( union X)) by XTUPLE_0:def 13;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let X, Y;

      cluster -> functional for PFUNC_DOMAIN of X, Y;

      coherence by RFUNCT_3:def 3;

    end

    theorem :: COMPUT_1:15



     Th14: for P be compatible PFUNC_DOMAIN of X, Y holds ( union P) is PartFunc of X, Y

    proof

      let D be compatible PFUNC_DOMAIN of X, Y;

      set E = the set of all ( dom f) where f be Element of D;

      set F = the set of all ( rng f) where f be Element of D;

      reconsider u = ( union D) as Function;



       A1: ( rng u) c= Y

      proof

        let y be object;

        assume y in ( rng u);

        then y in ( union F) by Th13;

        then

        consider Z be set such that

         A2: y in Z and

         A3: Z in F by TARSKI:def 4;

        consider f be Element of D such that

         A4: Z = ( rng f) by A3;

        ( rng f) c= Y by RELAT_1:def 19;

        hence thesis by A2, A4;

      end;

      ( dom u) c= X

      proof

        let x be object;

        assume x in ( dom u);

        then x in ( union E) by Th11;

        then

        consider Z be set such that

         A5: x in Z and

         A6: Z in E by TARSKI:def 4;

        ex f be Element of D st Z = ( dom f) by A6;

        hence thesis by A5;

      end;

      hence thesis by A1, RELSET_1: 4;

    end;

    begin

    notation

      let f be Relation;

      synonym f is to-naturals for f is natural-valued;

    end

    registration

      cluster ( NAT * ) -defined to-naturals for Function;

      existence

      proof

        take f = {} ;

        thus ( dom f) c= ( NAT * );

        thus thesis;

      end;

    end

    definition

      let f be ( NAT * ) -defined Relation;

      :: COMPUT_1:def2

      attr f is len-total means

      : Def2: for x,y be FinSequence of NAT st ( len x) = ( len y) & x in ( dom f) holds y in ( dom f);

    end

    theorem :: COMPUT_1:16



     Th15: ( dom R) c= (n -tuples_on D) implies R is homogeneous;

    registration

      cluster empty -> homogeneous for Relation;

      coherence ;

    end

    registration

      let p be FinSequence, x be set;

      cluster (p .--> x) -> non empty homogeneous;

      coherence ;

    end

    registration

      cluster non empty homogeneous for Function;

      existence

      proof

        set p = the FinSequence;

        take (p .--> 0 );

        thus thesis;

      end;

    end

    registration

      let f be homogeneous Function, g be Function;

      cluster (g * f) -> homogeneous;

      coherence

      proof

        ( dom (g * f)) c= ( dom f) by RELAT_1: 25;

        hence ( dom (g * f)) is with_common_domain;

      end;

    end

    registration

      let X,Y be set;

      cluster homogeneous for PartFunc of (X * ), Y;

      existence

      proof

        set f = {} ;

        reconsider f as PartFunc of (X * ), Y by XBOOLE_1: 2;

        take f;

        thus ( dom f) is with_common_domain;

      end;

    end

    registration

      let X,Y be non empty set;

      cluster non empty homogeneous for PartFunc of (X * ), Y;

      existence

      proof

        set y = the Element of Y;

        reconsider Z = ( 0 -tuples_on X) as non empty Subset of (X * ) by FINSEQ_2: 90;

        reconsider f = (Z --> y) as PartFunc of (X * ), Y;

        take f;

        thus f is non empty;

        thus ( dom f) is with_common_domain;

      end;

    end

    registration

      let X be non empty set;

      cluster non empty homogeneous quasi_total for PartFunc of (X * ), X;

      existence

      proof

        set n = the Element of NAT , y = the Element of X;

        reconsider Z = (n -tuples_on X) as non empty Subset of (X * ) by FINSEQ_2: 90;

        reconsider f = (Z --> y) as PartFunc of (X * ), X;

        take f;

        thus f is non empty;

        thus f is homogeneous;

        let p,q be FinSequence of X;

        assume that

         A2: ( len p) = ( len q) and

         A3: p in ( dom f);

        ( len q) = n by A2, A3, CARD_1:def 7;

        then q is Element of Z by FINSEQ_2: 92;

        hence thesis;

      end;

    end

    registration

      cluster non empty homogeneous to-naturals len-total for ( NAT * ) -defined Function;

      existence

      proof

        reconsider Z = ( 0 -tuples_on NAT ) as non empty Subset of ( NAT * ) by FINSEQ_2: 90;

        set f = (Z --> 0 );

        reconsider f as ( NAT * ) -defined Function;



         A2: f is len-total

        proof

          let x,y be FinSequence of NAT such that

           A3: ( len x) = ( len y) and

           A4: x in ( dom f);



           A5: y is Element of (( len y) -tuples_on NAT ) by FINSEQ_2: 92;

          ( len x) = 0 by A4;

          hence thesis by A3, A5;

        end;

        take f;

        thus thesis by A2;

      end;

    end

    registration

      cluster -> to-naturals( NAT * ) -defined for PartFunc of ( NAT * ), NAT ;

      coherence ;

    end

    registration

      cluster quasi_total -> len-total for PartFunc of ( NAT * ), NAT ;

      coherence ;

    end

    theorem :: COMPUT_1:17



     Th16: for g be len-total to-naturals( NAT * ) -defined Function holds g is quasi_total PartFunc of ( NAT * ), NAT

    proof

      let g be len-total to-naturals( NAT * ) -defined Function;



       A1: ( rng g) c= NAT by VALUED_0:def 6;

      ( dom g) c= ( NAT * );

      then

      reconsider g9 = g as PartFunc of ( NAT * ), NAT by A1, RELSET_1: 4;

      for x,y be FinSequence of NAT st ( len x) = ( len y) & x in ( dom g) holds y in ( dom g) by Def2;

      then g9 is quasi_total;

      hence thesis;

    end;

    theorem :: COMPUT_1:18



     Th17: ( arity {} ) = 0

    proof

       not ex x be FinSequence st x in ( dom {} );

      hence thesis by MARGREL1:def 25;

    end;

    theorem :: COMPUT_1:19



     Th18: for f be homogeneous Relation st ( dom f) = { {} } holds ( arity f) = 0

    proof

      let f be homogeneous Relation;

      assume ( dom f) = { {} };

      then {} in ( dom f) by TARSKI:def 1;

      hence thesis by CARD_1: 27, MARGREL1:def 25;

    end;

    theorem :: COMPUT_1:20



     Th19: for f be homogeneous PartFunc of (X * ), Y holds ( dom f) c= (( arity f) -tuples_on X)

    proof

      let f be homogeneous PartFunc of (X * ), Y;

      let x be object;

      assume

       A1: x in ( dom f);

      per cases ;

        suppose

         A2: X is empty;

        then x = ( <*> (X * )) by A1, FUNCT_7: 17, TARSKI:def 1;

        then

         A3: ( arity f) = ( len ( <*> (X * ))) by A1, MARGREL1:def 25;

        ( 0 -tuples_on X) = { {} } by Th5;

        hence thesis by A1, A2, A3, FUNCT_7: 17;

      end;

        suppose X is non empty;

        then

        reconsider X9 = X as non empty set;

        reconsider x9 = x as FinSequence of X9 by A1, FINSEQ_1:def 11;

        ( len x9) = ( arity f) by A1, MARGREL1:def 25;

        then x9 is Element of (( arity f) -tuples_on X9) by FINSEQ_2: 92;

        hence thesis;

      end;

    end;

    theorem :: COMPUT_1:21



     Th20: for f be homogeneous( NAT * ) -defined Function holds ( dom f) c= (( arity f) -tuples_on NAT )

    proof

      let f be homogeneous( NAT * ) -defined Function;

      let x be object;

      assume

       A1: x in ( dom f);

      reconsider x9 = x as FinSequence of NAT by A1, FINSEQ_1:def 11;

      ( len x9) = ( arity f) by A1, MARGREL1:def 25;

      then x9 is Element of (( arity f) -tuples_on NAT ) by FINSEQ_2: 92;

      hence thesis;

    end;



     Lm1: for f be homogeneous PartFunc of (D * ), D holds f is quasi_total non empty iff ( dom f) = (( arity f) -tuples_on D)

    proof

      set X = D;

      let f be homogeneous PartFunc of (X * ), X;



       A1: ( dom f) c= (( arity f) -tuples_on X) by Th19;

      hereby

        assume f is quasi_total non empty;

        then

        reconsider f9 = f as quasi_total non empty homogeneous PartFunc of (X * ), X;

        consider x be object such that

         A2: x in ( dom f9) by XBOOLE_0:def 1;

        reconsider x9 = x as FinSequence of X by A2, FINSEQ_1:def 11;



         A3: ( len x9) = ( arity f) by A2, MARGREL1:def 25;

        now

          let z be object;

          thus z in ( dom f) implies z in (( arity f) -tuples_on X) by A1;

          assume z in (( arity f) -tuples_on X);

          then

          reconsider z9 = z as Element of (( arity f) -tuples_on X);

          ( len z9) = ( arity f) by CARD_1:def 7;

          hence z in ( dom f) by A2, A3, MARGREL1:def 22;

        end;

        hence ( dom f) = (( arity f) -tuples_on X);

      end;

      assume

       A4: ( dom f) = (( arity f) -tuples_on X);

      thus f is quasi_total

      proof

        let x,y be FinSequence of X;

        assume that

         A5: ( len x) = ( len y) and

         A6: x in ( dom f);

        ( len x) = ( arity f) by A4, A6, CARD_1:def 7;

        then y is Element of (( arity f) -tuples_on X) by A5, FINSEQ_2: 92;

        hence y in ( dom f) by A4;

      end;

      thus thesis by A4;

    end;

    theorem :: COMPUT_1:22



     Th21: for f be homogeneous PartFunc of (X * ), X holds f is quasi_total non empty iff ( dom f) = (( arity f) -tuples_on X)

    proof

      let f be homogeneous PartFunc of (X * ), X;

      per cases ;

        suppose X is empty;

        then f = {} ;

        hence thesis by Th5, Th17;

      end;

        suppose X is non empty;

        hence thesis by Lm1;

      end;

    end;

    theorem :: COMPUT_1:23



     Th22: for f be homogeneous to-naturals( NAT * ) -defined Function holds f is len-total non empty iff ( dom f) = (( arity f) -tuples_on NAT )

    proof

      let f be homogeneous to-naturals( NAT * ) -defined Function;



       A1: ( dom f) c= (( arity f) -tuples_on NAT ) by Th20;

      hereby

        assume f is len-total non empty;

        then

        reconsider f9 = f as quasi_total non empty homogeneous PartFunc of ( NAT * ), NAT by Th16;

        consider x be object such that

         A2: x in ( dom f9) by XBOOLE_0:def 1;

        reconsider x9 = x as FinSequence of NAT by A2, FINSEQ_1:def 11;



         A3: ( len x9) = ( arity f) by A2, MARGREL1:def 25;

        now

          let z be object;

          thus z in ( dom f) implies z in (( arity f) -tuples_on NAT ) by A1;

          assume z in (( arity f) -tuples_on NAT );

          then

          reconsider z9 = z as Element of (( arity f) -tuples_on NAT );

          ( len z9) = ( arity f) by CARD_1:def 7;

          hence z in ( dom f) by A2, A3, MARGREL1:def 22;

        end;

        hence ( dom f) = (( arity f) -tuples_on NAT );

      end;

      assume

       A4: ( dom f) = (( arity f) -tuples_on NAT );

      thus f is len-total

      proof

        let x,y be FinSequence of NAT ;

        assume that

         A5: ( len x) = ( len y) and

         A6: x in ( dom f);

        ( len x) = ( arity f) by A4, A6, CARD_1:def 7;

        then y is Element of (( arity f) -tuples_on NAT ) by A5, FINSEQ_2: 92;

        hence thesis by A4;

      end;

      thus thesis by A4;

    end;

    theorem :: COMPUT_1:24

    for f be non empty homogeneous PartFunc of (D * ), D, n st ( dom f) c= (n -tuples_on D) holds ( arity f) = n

    proof

      let f be non empty homogeneous PartFunc of (D * ), D, n;

      consider x be object such that

       A1: x in ( dom f) by XBOOLE_0:def 1;

      assume

       A2: ( dom f) c= (n -tuples_on D);

      then

       A3: for x be FinSequence st x in ( dom f) holds n = ( len x) by CARD_1:def 7;

      reconsider x as Element of (n -tuples_on D) by A2, A1;

      x in ( dom f) by A1;

      hence thesis by A3, MARGREL1:def 25;

    end;

    theorem :: COMPUT_1:25



     Th24: for f be homogeneous PartFunc of (D * ), D, n st ( dom f) = (n -tuples_on D) holds ( arity f) = n

    proof

      let f be homogeneous PartFunc of (D * ), D, n;

      consider x be object such that

       A1: x in (n -tuples_on D) by XBOOLE_0:def 1;

      reconsider x as Element of (n -tuples_on D) by A1;

      assume

       A2: ( dom f) = (n -tuples_on D);

      then

       A3: for x be FinSequence st x in ( dom f) holds ( len x) = n by CARD_1:def 7;

      x in ( dom f) by A2;

      hence thesis by A3, MARGREL1:def 25;

    end;

    definition

      let R be Relation;

      :: COMPUT_1:def3

      attr R is with_the_same_arity means

      : Def3: for f,g be Function st f in ( rng R) & g in ( rng R) holds (f is empty implies g is empty or ( dom g) = { {} }) & (f is non empty & g is non empty implies ex n be Element of NAT , X be non empty set st ( dom f) c= (n -tuples_on X) & ( dom g) c= (n -tuples_on X));

    end

    registration

      cluster empty -> with_the_same_arity for Relation;

      coherence ;

    end

    registration

      let X be set;

      cluster with_the_same_arity for FinSequence of X;

      existence

      proof

        take ( <*> X);

        thus thesis;

      end;

      cluster with_the_same_arity for Element of (X * );

      existence

      proof

        reconsider p = ( <*> X) as Element of (X * ) by FINSEQ_1:def 11;

        take p;

        thus thesis;

      end;

    end

    definition

      let F be with_the_same_arity Relation;

      :: COMPUT_1:def4

      func arity F -> Element of NAT means

      : Def4: for f be homogeneous Function st f in ( rng F) holds it = ( arity f) if ex f be homogeneous Function st f in ( rng F)

      otherwise it = 0 ;

      existence

      proof

        hereby

          given f be homogeneous Function such that

           A1: f in ( rng F);

          take i = ( arity f);

          let g be homogeneous Function;

          assume

           A2: g in ( rng F);

          per cases ;

            suppose

             A3: f is empty;

            thus i = ( arity g)

            proof

              per cases by A1, A2, A3, Def3;

                suppose g is empty;

                hence thesis by A3;

              end;

                suppose ( dom g) = { {} };

                hence thesis by A3, Th17, Th18;

              end;

            end;

          end;

            suppose

             A4: g is empty;

            thus i = ( arity g)

            proof

              per cases by A1, A2, A4, Def3;

                suppose f is empty;

                hence thesis by A4;

              end;

                suppose ( dom f) = { {} };

                hence thesis by A4, Th17, Th18;

              end;

            end;

          end;

            suppose

             A5: f is non empty & g is non empty;

            set a = the Element of ( dom f);

            ( dom f) <> {} by A5;

            then

             A6: a in ( dom f);

            consider n be Element of NAT , X be non empty set such that

             A7: ( dom f) c= (n -tuples_on X) and

             A8: ( dom g) c= (n -tuples_on X) by A1, A2, A5, Def3;

            reconsider a as Element of (n -tuples_on X) by A7, A6;



             A9: ( arity f) = ( len a) by A5, MARGREL1:def 25

            .= n by CARD_1:def 7;

            set a = the Element of ( dom g);

            ( dom g) <> {} by A5;

            then a in ( dom g);

            then

            reconsider a as Element of (n -tuples_on X) by A8;

            ( arity g) = ( len a) by A5, MARGREL1:def 25;

            hence i = ( arity g) by A9, CARD_1:def 7;

          end;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let i1,i2 be Element of NAT ;

        hereby

          given f be homogeneous Function such that

           A10: f in ( rng F);

          assume for f be homogeneous Function st f in ( rng F) holds i1 = ( arity f);

          then i1 = ( arity f) by A10;

          hence (for f be homogeneous Function st f in ( rng F) holds i2 = ( arity f)) implies i1 = i2 by A10;

        end;

        thus thesis;

      end;

      correctness ;

    end

    theorem :: COMPUT_1:26

    for F be with_the_same_arity FinSequence st ( len F) = 0 holds ( arity F) = 0

    proof

      let F be with_the_same_arity FinSequence;

      assume ( len F) = 0 ;

      then F = {} ;

      then for f be homogeneous Function holds not f in ( rng F);

      hence thesis by Def4;

    end;

    definition

      let X be set;

      :: COMPUT_1:def5

      func HFuncs X -> PFUNC_DOMAIN of (X * ), X equals { f where f be Element of ( PFuncs ((X * ),X)) : f is homogeneous };

      coherence

      proof

        set H = { f where f be Element of ( PFuncs ((X * ),X)) : f is homogeneous };

        H is non empty functional

        proof

           {} is PartFunc of (X * ), X by RELSET_1: 12;

          then {} in ( PFuncs ((X * ),X)) by PARTFUN1: 45;

          then {} in H;

          hence H is non empty;

          let x be object;

          assume x in H;

          then ex g be Element of ( PFuncs ((X * ),X)) st x = g & g is homogeneous;

          hence thesis;

        end;

        then

        reconsider H as non empty functional set;

        now

          let f be Element of H;

          f in H;

          then ex g be Element of ( PFuncs ((X * ),X)) st f = g & g is homogeneous;

          hence f is PartFunc of (X * ), X;

        end;

        hence thesis by RFUNCT_3:def 3;

      end;

    end

    theorem :: COMPUT_1:27

     {} in ( HFuncs X)

    proof

      set f = {} ;

      reconsider f as PartFunc of (X * ), X by XBOOLE_1: 2;

      reconsider f as Element of ( PFuncs ((X * ),X)) by PARTFUN1: 45;

      f in { g where g be Element of ( PFuncs ((X * ),X)) : g is homogeneous };

      hence thesis;

    end;

    registration

      let X be non empty set;

      cluster non empty homogeneous quasi_total for Element of ( HFuncs X);

      existence

      proof

        set p = ( <*> X);

        set x = the Element of X;

        p in (X * ) by FINSEQ_1:def 11;

        then

        reconsider Y = {p} as Subset of (X * ) by ZFMISC_1: 31;



         A1: (Y --> x) in ( PFuncs ((X * ),X));

        (p .--> x) is homogeneous;

        then ( {p} --> x) in { f where f be Element of ( PFuncs ((X * ),X)) : f is homogeneous } by A1;

        then

        reconsider f = (p .--> x) as Element of ( HFuncs X);

        take f;

        thus f is non empty homogeneous;

        let a,b be FinSequence of X such that

         A3: ( len a) = ( len b);

        assume a in ( dom f);

        then a = p by TARSKI:def 1;

        then b = {} by A3;

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      let X be set;

      cluster -> homogeneous for Element of ( HFuncs X);

      coherence

      proof

        let f be Element of ( HFuncs X);

        f in ( HFuncs X);

        then ex g be Element of ( PFuncs ((X * ),X)) st f = g & g is homogeneous;

        hence thesis;

      end;

    end

    registration

      let X be non empty set, S be non empty Subset of ( HFuncs X);

      cluster -> homogeneous for Element of S;

      coherence ;

    end

    theorem :: COMPUT_1:28



     Th27: for f be to-naturals homogeneous( NAT * ) -defined Function holds f is Element of ( HFuncs NAT )

    proof

      let f be to-naturals homogeneous( NAT * ) -defined Function;



       A1: ( rng f) c= NAT by VALUED_0:def 6;

      ( dom f) c= ( NAT * );

      then f is PartFunc of ( NAT * ), NAT by A1, RELSET_1: 4;

      then

      reconsider f9 = f as Element of ( PFuncs (( NAT * ), NAT )) by PARTFUN1: 45;

      f9 in { f1 where f1 be Element of ( PFuncs (( NAT * ), NAT )) : f1 is homogeneous };

      hence thesis;

    end;

    theorem :: COMPUT_1:29



     Th28: for f be len-total to-naturals homogeneous( NAT * ) -defined Function holds f is quasi_total Element of ( HFuncs NAT )

    proof

      let f be len-total to-naturals homogeneous( NAT * ) -defined Function;

      reconsider f9 = f as Element of ( HFuncs NAT ) by Th27;

      f9 is quasi_total by Def2;

      hence thesis;

    end;

    theorem :: COMPUT_1:30



     Th29: for X be non empty set, F be Relation st ( rng F) c= ( HFuncs X) & for f,g be homogeneous Function st f in ( rng F) & g in ( rng F) holds ( arity f) = ( arity g) holds F is with_the_same_arity

    proof

      let X be non empty set, R be Relation such that

       A1: ( rng R) c= ( HFuncs X) and

       A2: for f,g be homogeneous Function st f in ( rng R) & g in ( rng R) holds ( arity f) = ( arity g);

      let f,g be Function;

      assume that

       A3: f in ( rng R) and

       A4: g in ( rng R);

      reconsider f9 = f, g9 = g as Element of ( HFuncs X) by A1, A3, A4;



       A5: ( arity f9) = ( arity g9) by A2, A3, A4;

      hereby

        assume f is empty;

        then ( dom g9) c= ( 0 -tuples_on X) by A5, Th17, Th19;

        then ( dom g9) c= {( <*> X)} by FINSEQ_2: 94;

        hence g is empty or ( dom g) = { {} } by ZFMISC_1: 33;

      end;

      assume that

       A6: f is non empty and g is non empty;

      reconsider f9 as non empty Element of ( HFuncs X) by A6;

      take ( arity f9), X;

      thus thesis by A5, Th19;

    end;

    definition

      let n,m be Nat;

      :: COMPUT_1:def6

      func n const m -> homogeneous to-naturals( NAT * ) -defined Function equals ((n -tuples_on NAT ) --> m);

      coherence

      proof

        set X = NAT ;

        set f = ((n -tuples_on X) --> m);



         A1: (n -tuples_on X) c= (X * ) by FINSEQ_2: 142;

        f is homogeneous;

        hence thesis by A1, RELAT_1:def 18;

      end;

    end

    theorem :: COMPUT_1:31



     Th30: (n const m) in ( HFuncs NAT )

    proof

      set X = NAT ;

      set f = (n const m);



       A1: ( rng f) c= NAT by VALUED_0:def 6;

      ( dom f) c= ( NAT * );

      then f is PartFunc of (X * ), X by A1, RELSET_1: 4;

      then f is Element of ( PFuncs ((X * ),X)) by PARTFUN1: 45;

      hence thesis;

    end;

    registration

      let n,m be Element of NAT ;

      cluster (n const m) -> len-total non empty;

      coherence

      proof

        set X = NAT ;

        (n const m) is len-total

        proof

          let x,y be FinSequence of X;

          assume that

           A2: ( len x) = ( len y) and

           A3: x in ( dom (n const m));

          ( len x) = n by A3, CARD_1:def 7;

          then y is Element of (n -tuples_on X) by A2, FINSEQ_2: 92;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: COMPUT_1:32



     Th31: ( arity (n const m)) = n

    proof

      set X = NAT ;

      set d = the Element of (n -tuples_on X);



       A2: for x be FinSequence st x in ( dom (n const m)) holds n = ( len x) by CARD_1:def 7;

      d in ( dom (n const m));

      hence thesis by A2, MARGREL1:def 25;

    end;

    registration

      cluster -> homogeneous to-naturals( NAT * ) -defined for Element of ( HFuncs NAT );

      coherence ;

    end

    definition

      let n,i be Element of NAT ;

      :: COMPUT_1:def7

      func n succ i -> homogeneous to-naturals( NAT * ) -defined Function means

      : Def7: ( dom it ) = (n -tuples_on NAT ) & for p be Element of (n -tuples_on NAT ) holds (it . p) = ((p /. i) + 1);

      existence

      proof

        deffunc f( Element of ( NAT * )) = (($1 /. i) + 1);

        defpred p[ set] means $1 in (n -tuples_on NAT );

        consider f be PartFunc of ( NAT * ), NAT such that

         A1: for d be Element of ( NAT * ) holds d in ( dom f) iff p[d] and

         A2: for d be Element of ( NAT * ) st d in ( dom f) holds (f /. d) = f(d) from PARTFUN2:sch 2;



         A3: (n -tuples_on NAT ) c= ( NAT * ) by FINSEQ_2: 142;

        then

         A4: for x be object holds x in ( dom f) iff x in (n -tuples_on NAT ) by A1;

        then

         A5: ( dom f) = (n -tuples_on NAT ) by TARSKI: 2;

        reconsider f as Element of ( PFuncs (( NAT * ), NAT )) by PARTFUN1: 45;

        f is homogeneous by A5;

        then f in { g where g be Element of ( PFuncs (( NAT * ), NAT )) : g is homogeneous };

        then

        reconsider f as Element of ( HFuncs NAT );

        take f;

        thus ( dom f) = (n -tuples_on NAT ) by A4;

        let p be Element of (n -tuples_on NAT );

        reconsider p9 = p as Element of ( NAT * ) by A3;



        thus (f . p) = (f /. p9) by A5, PARTFUN1:def 6

        .= ((p /. i) + 1) by A2, A5;

      end;

      uniqueness

      proof

        let it1,it2 be homogeneous to-naturals( NAT * ) -defined Function such that

         A6: ( dom it1) = (n -tuples_on NAT ) and

         A7: for p be Element of (n -tuples_on NAT ) holds (it1 . p) = ((p /. i) + 1) and

         A8: ( dom it2) = (n -tuples_on NAT ) and

         A9: for p be Element of (n -tuples_on NAT ) holds (it2 . p) = ((p /. i) + 1);

        now

          let x be object;

          assume x in (n -tuples_on NAT );

          then

          reconsider x9 = x as Element of (n -tuples_on NAT );



          thus (it1 . x) = ((x9 /. i) + 1) by A7

          .= (it2 . x) by A9;

        end;

        hence thesis by A6, A8;

      end;

    end

    theorem :: COMPUT_1:33



     Th32: (n succ i) in ( HFuncs NAT )

    proof

      set X = NAT ;

      set f = (n succ i);



       A1: ( rng f) c= NAT by VALUED_0:def 6;

      ( dom f) c= ( NAT * );

      then f is PartFunc of (X * ), X by A1, RELSET_1: 4;

      then f is Element of ( PFuncs ((X * ),X)) by PARTFUN1: 45;

      hence thesis;

    end;

    registration

      let n,i be Element of NAT ;

      cluster (n succ i) -> len-total non empty;

      coherence

      proof



         A1: ( dom (n succ i)) = (n -tuples_on NAT ) by Def7;

        (n succ i) is len-total

        proof

          let x,y be FinSequence of NAT ;

          assume that

           A2: ( len x) = ( len y) and

           A3: x in ( dom (n succ i));

          ( len x) = n by A1, A3, CARD_1:def 7;

          then y is Element of (n -tuples_on NAT ) by A2, FINSEQ_2: 92;

          hence thesis by A1;

        end;

        hence thesis by A1;

      end;

    end

    theorem :: COMPUT_1:34



     Th33: ( arity (n succ i)) = n

    proof

      consider d be object such that

       A1: d in ( dom (n succ i)) by XBOOLE_0:def 1;

      reconsider d as Element of (n -tuples_on NAT ) by A1, Def7;

      ( dom (n succ i)) = (n -tuples_on NAT ) by Def7;

      then

       A2: for y be FinSequence st y in ( dom (n succ i)) holds n = ( len y) by CARD_1:def 7;

      d in ( dom (n succ i)) by A1;

      hence thesis by A2, MARGREL1:def 25;

    end;

    definition

      let n,i be Nat;

      :: COMPUT_1:def8

      func n proj i -> homogeneous to-naturals( NAT * ) -defined Function equals ( proj ((n |-> NAT ),i));

      correctness

      proof



         A1: ( dom ( proj ((n |-> NAT ),i))) = ( product (n |-> NAT )) by CARD_3:def 16

        .= (n -tuples_on NAT ) by FINSEQ_3: 131;

        now

          set P = ( proj ((n |-> NAT ),i));



           A2: ( rng P) c= NAT

          proof

            let x be object;

            assume x in ( rng P);

            then

            consider d be object such that

             A3: d in ( dom P) and

             A4: x = (P . d) by FUNCT_1:def 3;

            reconsider d as Element of (n -tuples_on NAT ) by A1, A3;

            reconsider d as FinSequence of NAT ;

            (P . d) = (d . i) by A3, CARD_3:def 16;

            hence thesis by A4;

          end;



           A5: P is homogeneous

          proof

            thus ( dom P) is with_common_domain;

          end;

          reconsider P as PartFunc of ( NAT * ), NAT by A1, A2, FINSEQ_2: 142, RELSET_1: 4;

          P is Element of ( PFuncs (( NAT * ), NAT )) by PARTFUN1: 45;

          then P in ( HFuncs NAT ) by A5;

          hence ( proj ((n |-> NAT ),i)) is Element of ( HFuncs NAT );

        end;

        hence thesis;

      end;

    end

    theorem :: COMPUT_1:35



     Th34: (n proj i) in ( HFuncs NAT )

    proof

      set X = NAT ;

      set f = (n proj i);



       A1: ( rng f) c= NAT by VALUED_0:def 6;

      ( dom f) c= ( NAT * );

      then f is PartFunc of (X * ), X by A1, RELSET_1: 4;

      then f is Element of ( PFuncs ((X * ),X)) by PARTFUN1: 45;

      hence thesis;

    end;

    theorem :: COMPUT_1:36



     Th35: ( dom (n proj i)) = (n -tuples_on NAT ) & (1 <= i & i <= n implies ( rng (n proj i)) = NAT )

    proof



      thus

       A1: ( dom (n proj i)) = ( product (n |-> NAT )) by CARD_3:def 16

      .= (n -tuples_on NAT ) by FINSEQ_3: 131;

      assume that

       A2: 1 <= i and

       A3: i <= n;

      now

        let x be object;

        thus x in ( rng (n proj i)) implies x in NAT by ORDINAL1:def 12;

        assume x in NAT ;

        then

        reconsider x9 = x as Element of NAT ;

        reconsider d = (n |-> x9) as FinSequence of NAT ;

        i in ( Seg n) by A2, A3, FINSEQ_1: 1;

        then

         A4: (d . i) = x9 by FUNCOP_1: 7;

        ((n proj i) . d) = (d . i) by A1, CARD_3:def 16;

        hence x in ( rng (n proj i)) by A1, A4, FUNCT_1:def 3;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let n,i be Element of NAT ;

      cluster (n proj i) -> len-total non empty;

      coherence

      proof



         A1: ( dom (n proj i)) = (n -tuples_on NAT ) by Th35;

        (n proj i) is len-total

        proof

          let x,y be FinSequence of NAT ;

          assume that

           A2: ( len x) = ( len y) and

           A3: x in ( dom (n proj i));

          ( len x) = n by A1, A3, CARD_1:def 7;

          then y is Element of (n -tuples_on NAT ) by A2, FINSEQ_2: 92;

          hence thesis by A1;

        end;

        hence thesis by A1;

      end;

    end

    theorem :: COMPUT_1:37



     Th36: ( arity (n proj i)) = n

    proof

      consider d be object such that

       A1: d in (n -tuples_on NAT ) by XBOOLE_0:def 1;

      reconsider d as Element of (n -tuples_on NAT ) by A1;



       A2: ( dom (n proj i)) = (n -tuples_on NAT ) by Th35;

      then

       A3: for x be FinSequence st x in ( dom (n proj i)) holds n = ( len x) by CARD_1:def 7;

      d in ( dom (n proj i)) by A2;

      hence thesis by A3, MARGREL1:def 25;

    end;

    theorem :: COMPUT_1:38



     Th37: for t be Element of (n -tuples_on NAT ) holds ((n proj i) . t) = (t . i)

    proof

      let t be Element of (n -tuples_on NAT );

      ( dom (n proj i)) = (n -tuples_on NAT ) by Th35;

      hence thesis by CARD_3:def 16;

    end;

    registration

      let X be set;

      cluster ( HFuncs X) -> functional;

      coherence ;

    end

    theorem :: COMPUT_1:39



     Th38: for F be Function of D, ( HFuncs E) st ( rng F) is compatible & for x be Element of D holds ( dom (F . x)) c= (n -tuples_on E) holds ex f be Element of ( HFuncs E) st f = ( Union F) & ( dom f) c= (n -tuples_on E)

    proof

      set X = D, Y = E;

      let F be Function of X, ( HFuncs Y);

      assume

       A1: ( rng F) is compatible;

      assume

       A2: for x be Element of X holds ( dom (F . x)) c= (n -tuples_on Y);



       A3: ( rng F) is functional

      proof

        let x be object;



         A4: ( rng F) c= ( HFuncs Y) by RELAT_1:def 19;

        assume x in ( rng F);

        hence thesis by A4;

      end;

      then

      reconsider rngF = ( rng F) as non empty functional compatible set by A1;

      set D = the set of all ( dom g) where g be Element of rngF;

      reconsider f = ( Union F) as Function by A1, A3;



       A5: ( rng f) c= Y

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A6: x in ( dom f) and

         A7: (f . x) = y by FUNCT_1:def 3;

        x in ( union D) by A6, Th11;

        then

        consider d be set such that

         A8: x in d and

         A9: d in D by TARSKI:def 4;

        consider g be Element of rngF such that

         A10: d = ( dom g) by A9;

        ( rng F) c= ( HFuncs Y) by RELAT_1:def 19;

        then

        reconsider g as Element of ( HFuncs Y);



         A11: (g . x) in ( rng g) by A8, A10, FUNCT_1: 3;



         A12: ( rng g) c= Y by RELAT_1:def 19;

        (f . x) = (g . x) by A8, A10, Th12;

        hence thesis by A7, A12, A11;

      end;



       A13: ( dom f) c= (n -tuples_on Y)

      proof

        let x be object;

        assume x in ( dom f);

        then x in ( union D) by Th11;

        then

        consider d be set such that

         A14: x in d and

         A15: d in D by TARSKI:def 4;

        consider g be Element of rngF such that

         A16: d = ( dom g) by A15;

        consider e be object such that

         A17: e in ( dom F) and

         A18: (F . e) = g by FUNCT_1:def 3;

        reconsider e as Element of X by A17;

        ( dom (F . e)) c= (n -tuples_on Y) by A2;

        hence thesis by A14, A16, A18;

      end;

      (n -tuples_on Y) c= (Y * ) by FINSEQ_2: 142;

      then ( dom f) c= (Y * ) by A13;

      then

      reconsider f as PartFunc of (Y * ), Y by A5, RELSET_1: 4;

      reconsider f as Element of ( PFuncs ((Y * ),Y)) by PARTFUN1: 45;

      f is homogeneous by A13;

      then f in { g where g be Element of ( PFuncs ((Y * ),Y)) : g is homogeneous };

      then

      reconsider f = ( Union F) as Element of ( HFuncs Y);

      take f;

      thus f = ( Union F);

      thus thesis by A13;

    end;

    theorem :: COMPUT_1:40

    for F be sequence of ( HFuncs D) st for i be Nat holds (F . i) c= (F . (i + 1)) holds ( Union F) in ( HFuncs D)

    proof

      set X = D;

      let F be sequence of ( HFuncs X) such that

       A1: for i be Nat holds (F . i) c= (F . (i + 1));

       A2:

      now

        let n be Element of NAT ;

        defpred p[ Nat] means (F . n) c= (F . (n + $1));

        let m be Element of NAT ;

         A3:

        now

          let i be Nat such that

           A4: p[i];

          (F . (n + i)) c= (F . ((n + i) + 1)) by A1;

          hence p[(i + 1)] by A4, XBOOLE_1: 1;

        end;



         A5: p[ 0 ];



         A6: for i be Nat holds p[i] from NAT_1:sch 2( A5, A3);

        assume n <= m;

        then

        consider i be Nat such that

         A7: m = (n + i) by NAT_1: 10;

        thus (F . n) c= (F . m) by A6, A7;

      end;

      reconsider Y = ( rng F) as non empty Subset of ( HFuncs X) by RELAT_1:def 19;



       A8: Y is compatible

      proof

        let f,g be Function;

        assume f in Y;

        then

        consider i be object such that

         A9: i in ( dom F) and

         A10: f = (F . i) by FUNCT_1:def 3;

        assume g in Y;

        then

        consider j be object such that

         A11: j in ( dom F) and

         A12: g = (F . j) by FUNCT_1:def 3;

        reconsider i, j as Element of NAT by A9, A11;

        i <= j or j <= i;

        hence thesis by A2, A10, A12, PARTFUN1: 54;

      end;

      Y is PartFunc-set of (X * ), X

      proof

        let f be Element of Y;

        f is Element of ( HFuncs X);

        hence thesis;

      end;

      then ( Union F) is PartFunc of (X * ), X by A8, Th14;

      then

      reconsider f = ( Union F) as Element of ( PFuncs ((X * ),X)) by PARTFUN1: 45;



       A13: ( dom f) = ( union the set of all ( dom g) where g be Element of Y) by A8, Th11;

      f is homogeneous

      proof

        thus ( dom f) is with_common_domain

        proof

          let x,y be FinSequence;

          assume x in ( dom f);

          then

          consider A1 be set such that

           A14: x in A1 and

           A15: A1 in the set of all ( dom g) where g be Element of Y by A13, TARSKI:def 4;

          consider g1 be Element of Y such that

           A16: A1 = ( dom g1) by A15;

          assume y in ( dom f);

          then

          consider A2 be set such that

           A17: y in A2 and

           A18: A2 in the set of all ( dom g) where g be Element of Y by A13, TARSKI:def 4;

          consider g2 be Element of Y such that

           A19: A2 = ( dom g2) by A18;

          consider i1 be object such that

           A20: i1 in ( dom F) and

           A21: g1 = (F . i1) by FUNCT_1:def 3;

          consider i2 be object such that

           A22: i2 in ( dom F) and

           A23: g2 = (F . i2) by FUNCT_1:def 3;

          reconsider i1, i2 as Element of NAT by A20, A22;

          i1 <= i2 or i2 <= i1;

          then g1 c= g2 or g2 c= g1 by A2, A21, A23;

          then ( dom g1) c= ( dom g2) or ( dom g2) c= ( dom g1) by GRFUNC_1: 2;

          then ( dom x) = ( dom y) by A14, A16, A17, A19, CARD_3:def 10;

          hence ( len x) = ( len y) by FINSEQ_3: 29;

        end;

      end;

      hence thesis;

    end;

    theorem :: COMPUT_1:41



     Th40: for F be with_the_same_arity FinSequence of ( HFuncs D) holds ( dom <:F:>) c= (( arity F) -tuples_on D)

    proof

      set X = D;

      let F be with_the_same_arity FinSequence of ( HFuncs X);

      thus ( dom <:F:>) c= (( arity F) -tuples_on X)

      proof



         A1: ( dom <:F:>) = ( meet ( doms F)) by FUNCT_6: 29

        .= ( meet ( rng ( doms F))) by FUNCT_6:def 4;

        let x be object such that

         A2: x in ( dom <:F:>);

        consider y be object such that

         A3: y in ( rng ( doms F)) by A2, A1, SETFAM_1: 1, XBOOLE_0:def 1;

        reconsider y as set by TARSKI: 1;



         A4: x in y by A2, A1, A3, SETFAM_1:def 1;

        consider z be object such that

         A5: z in ( dom ( doms F)) and

         A6: (( doms F) . z) = y by A3, FUNCT_1:def 3;



         A7: ( dom ( doms F)) = ( dom F) by FUNCT_6:def 2;

        then z in ( dom F) by A5;

        then

         A8: (F . z) in ( rng F) by FUNCT_1: 3;

        ( rng F) c= ( HFuncs X) by RELAT_1:def 19;

        then

        reconsider Fz = (F . z) as Element of ( HFuncs X) by A8;



         A9: ( dom Fz) c= (( arity Fz) -tuples_on X) by Th19;

        (( doms F) . z) = ( dom Fz) by A7, A5, FUNCT_6:def 2;

        then x in (( arity Fz) -tuples_on X) by A6, A4, A9;

        hence thesis by A8, Def4;

      end;

    end;

    registration

      let X be non empty set;

      let F be with_the_same_arity FinSequence of ( HFuncs X);

      cluster <:F:> -> homogeneous;

      coherence

      proof

        ( dom <:F:>) c= (( arity F) -tuples_on X) by Th40;

        hence ( dom <:F:>) is with_common_domain;

      end;

    end

    theorem :: COMPUT_1:42



     Th41: for f be Element of ( HFuncs D), F be with_the_same_arity FinSequence of ( HFuncs D) holds ( dom (f * <:F:>)) c= (( arity F) -tuples_on D) & ( rng (f * <:F:>)) c= D & (f * <:F:>) in ( HFuncs D)

    proof

      set X = D;

      let f be Element of ( HFuncs X);

      let F be with_the_same_arity FinSequence of ( HFuncs X);



       A1: ( dom (f * <:F:>)) c= ( dom <:F:>) by RELAT_1: 25;



       A2: (( arity F) -tuples_on X) c= (X * ) by FINSEQ_2: 142;

      ( dom <:F:>) c= (( arity F) -tuples_on X) by Th40;

      hence ( dom (f * <:F:>)) c= (( arity F) -tuples_on X) by A1;

      then

       A3: ( dom (f * <:F:>)) c= (X * ) by A2;

      thus ( rng (f * <:F:>)) c= X by RELAT_1:def 19;

      then (f * <:F:>) is PartFunc of (X * ), X by A3, RELSET_1: 4;

      then (f * <:F:>) in ( PFuncs ((X * ),X)) by PARTFUN1: 45;

      hence thesis;

    end;

    definition

      let X,Y be non empty set, P be PFUNC_DOMAIN of X, Y;

      let S be non empty Subset of P;

      :: original: Element

      redefine

      mode Element of S -> Element of P ;

      coherence

      proof

        let f be Element of S;

        thus thesis;

      end;

    end

    registration

      let f be homogeneous( NAT * ) -defined Function;

      cluster <*f*> -> with_the_same_arity;

      coherence

      proof

        let h,g be Function such that

         A1: h in ( rng <*f*>) and

         A2: g in ( rng <*f*>);



         A3: ( rng <*f*>) = {f} by FINSEQ_1: 39;

        then

         A4: h = f by A1, TARSKI:def 1;

        hence h is empty implies g is empty or ( dom g) = { {} } by A2, A3, TARSKI:def 1;

        assume that h is non empty and g is non empty;

        take ( arity f), NAT ;

        g = f by A2, A3, TARSKI:def 1;

        hence thesis by A4, Th20;

      end;

    end

    theorem :: COMPUT_1:43

    for f be homogeneous to-naturals( NAT * ) -defined Function holds ( arity <*f*>) = ( arity f)

    proof

      let f be homogeneous to-naturals( NAT * ) -defined Function;

      ( rng <*f*>) = {f} by FINSEQ_1: 38;

      then f in ( rng <*f*>) by TARSKI:def 1;

      hence thesis by Def4;

    end;

    theorem :: COMPUT_1:44



     Th43: for f,g be non empty Element of ( HFuncs NAT ), F be with_the_same_arity FinSequence of ( HFuncs NAT ) st g = (f * <:F:>) holds ( arity g) = ( arity F)

    proof

      let f,g be non empty Element of ( HFuncs NAT ), F be with_the_same_arity FinSequence of ( HFuncs NAT );

      assume g = (f * <:F:>);

      then

       A1: ( dom g) c= (( arity F) -tuples_on NAT ) by Th41;

      consider x be object such that

       A2: x in ( dom g) by XBOOLE_0:def 1;

      reconsider x as Element of (( arity F) -tuples_on NAT ) by A1, A2;

      ( len x) = ( arity F) by CARD_1:def 7;

      hence thesis by A2, MARGREL1:def 25;

    end;

    theorem :: COMPUT_1:45



     Th44: for f be non empty quasi_total Element of ( HFuncs D), F be with_the_same_arity FinSequence of ( HFuncs D) st ( arity f) = ( len F) & F is non empty & (for h be Element of ( HFuncs D) st h in ( rng F) holds h is quasi_total non empty) holds (f * <:F:>) is non empty quasi_total Element of ( HFuncs D) & ( dom (f * <:F:>)) = (( arity F) -tuples_on D)

    proof

      set X = D;

      let f be non empty quasi_total Element of ( HFuncs X), F be with_the_same_arity FinSequence of ( HFuncs X) such that

       A1: ( arity f) = ( len F) and

       A2: F is non empty and

       A3: for h be Element of ( HFuncs X) st h in ( rng F) holds h is quasi_total non empty;

      set n = ( arity F);

      set fF = (f * <:F:>);



       A4: ( dom fF) c= (n -tuples_on X) by Th41;



       A5: (n -tuples_on X) c= ( dom fF)

      proof

        let x be object;



         A6: ( product ( rngs F)) c= (( len F) -tuples_on X)

        proof

          let p be object;



           A7: ( dom ( rngs F)) = ( dom F) by FUNCT_6:def 3;

          assume p in ( product ( rngs F));

          then

          consider g be Function such that

           A8: p = g and

           A9: ( dom g) = ( dom ( rngs F)) and

           A10: for x be object st x in ( dom ( rngs F)) holds (g . x) in (( rngs F) . x) by CARD_3:def 5;



           A11: ( dom F) = ( Seg ( len F)) by FINSEQ_1:def 3;

          then

          reconsider g as FinSequence by A9, A7, FINSEQ_1:def 2;

          ( rng g) c= X

          proof

            let x be object;

            assume x in ( rng g);

            then

            consider d be object such that

             A12: d in ( dom g) and

             A13: (g . d) = x by FUNCT_1:def 3;



             A14: (g . d) in (( rngs F) . d) by A9, A10, A12;

            reconsider d as Element of NAT by A12;

            reconsider Fd = (F . d) as Element of ( HFuncs X) by A9, A7, A12, FINSEQ_2: 11;



             A15: ( rng Fd) c= X by RELAT_1:def 19;

            (( rngs F) . d) = ( rng Fd) by A9, A7, A12, FUNCT_6:def 3;

            hence thesis by A13, A14, A15;

          end;

          then

          reconsider g as FinSequence of X by FINSEQ_1:def 4;

          ( len g) = ( len F) by A9, A7, A11, FINSEQ_1:def 3;

          then p is Element of (( len F) -tuples_on X) by A8, FINSEQ_2: 92;

          hence thesis;

        end;

        ( rng <:F:>) c= ( product ( rngs F)) by FUNCT_6: 29;

        then

         A16: ( rng <:F:>) c= (( len F) -tuples_on X) by A6;



         A17: ( dom f) = (( arity f) -tuples_on X) by Th21;



         A18: (n -tuples_on X) c= ( dom <:F:>)

        proof

          let x be object;



           A19: ( dom ( doms F)) = ( dom F) by FUNCT_6:def 2;

          assume

           A20: x in (n -tuples_on X);

           A21:

          now

            let y be set;

            assume y in ( rng ( doms F));

            then

            consider w be object such that

             A22: w in ( dom ( doms F)) and

             A23: (( doms F) . w) = y by FUNCT_1:def 3;



             A24: w in ( dom F) by A19, A22;

            then

            reconsider w as Element of NAT ;

            reconsider Fw = (F . w) as Element of ( HFuncs X) by A24, FINSEQ_2: 11;



             A25: (( doms F) . w) = ( dom Fw) by A19, A22, FUNCT_6:def 2;



             A26: Fw in ( rng F) by A24, FUNCT_1: 3;

            then Fw is non empty quasi_total by A3;

            then ( dom Fw) = (( arity Fw) -tuples_on X) by Th21;

            hence x in y by A20, A23, A25, A26, Def4;

          end;

          consider z be object such that

           A27: z in ( dom F) by A2, XBOOLE_0:def 1;

          z in ( dom ( doms F)) by A27, A19;

          then

           A28: ( rng ( doms F)) <> {} by RELAT_1: 42;

          ( dom <:F:>) = ( meet ( doms F)) by FUNCT_6: 29

          .= ( meet ( rng ( doms F))) by FUNCT_6:def 4;

          hence thesis by A28, A21, SETFAM_1:def 1;

        end;

        assume

         A29: x in (n -tuples_on X);

        then ( <:F:> . x) in ( rng <:F:>) by A18, FUNCT_1: 3;

        hence thesis by A1, A29, A18, A17, A16, FUNCT_1: 11;

      end;

      then

       A30: ( dom fF) = (n -tuples_on X) by A4, XBOOLE_0:def 10;



       A31: ( rng fF) c= X by Th41;

      (( arity F) -tuples_on X) c= (X * ) by FINSEQ_2: 142;

      then ( dom fF) c= (X * ) by A4;

      then fF is Relation of (X * ), X by A31, RELSET_1: 4;

      then fF is Element of ( PFuncs ((X * ),X)) by PARTFUN1: 45;

      then fF in ( HFuncs X);

      then

      reconsider fF as Element of ( HFuncs X);

      fF is quasi_total

      proof

        let x,y be FinSequence of X such that

         A32: ( len x) = ( len y) and

         A33: x in ( dom fF);

        ( len x) = n by A4, A33, CARD_1:def 7;

        then y is Element of (n -tuples_on X) by A32, FINSEQ_2: 92;

        hence y in ( dom fF) by A30;

      end;

      hence (f * <:F:>) is non empty quasi_total Element of ( HFuncs X) by A5;

      thus thesis by A4, A5, XBOOLE_0:def 10;

    end;

    theorem :: COMPUT_1:46



     Th45: for f be quasi_total Element of ( HFuncs D), F be with_the_same_arity FinSequence of ( HFuncs D) st ( arity f) = ( len F) & for h be Element of ( HFuncs D) st h in ( rng F) holds h is quasi_total holds (f * <:F:>) is quasi_total Element of ( HFuncs D)

    proof

      set X = D;

      let f be quasi_total Element of ( HFuncs X), F be with_the_same_arity FinSequence of ( HFuncs X) such that

       A1: ( arity f) = ( len F) and

       A2: for h be Element of ( HFuncs X) st h in ( rng F) holds h is quasi_total;

      reconsider g = {} as PartFunc of (X * ), X by RELSET_1: 12;



       A3: g is quasi_total;

      g in ( PFuncs ((X * ),X)) by PARTFUN1: 45;

      then

       A4: g in { h where h be Element of ( PFuncs ((X * ),X)) : h is homogeneous };

      per cases ;

        suppose f = {} ;

        hence thesis;

      end;

        suppose F = {} ;

        hence thesis by A4, A3, FUNCT_6: 40;

      end;

        suppose ex h be set st h in ( rng F) & h = {} ;

        then <:F:> = {} by Th7;

        hence thesis by A4, A3;

      end;

        suppose

         A5: F <> {} & f <> {} & for h be set st h in ( rng F) holds h <> {} ;

        then for h be Element of ( HFuncs X) st h in ( rng F) holds h is quasi_total non empty by A2;

        hence thesis by A1, A5, Th44;

      end;

    end;

    theorem :: COMPUT_1:47



     Th46: for f,g be non empty quasi_total Element of ( HFuncs D) st ( arity f) = 0 & ( arity g) = 0 & (f . {} ) = (g . {} ) holds f = g

    proof

      set X = D;

      let f,g be non empty quasi_total Element of ( HFuncs X);

      assume that

       A1: ( arity f) = 0 and

       A2: ( arity g) = 0 and

       A3: (f . {} ) = (g . {} );

      now



        thus ( dom f) = ( 0 -tuples_on X) by A1, Th21

        .= {( <*> X)} by FINSEQ_2: 94;



        thus ( dom g) = ( 0 -tuples_on X) by A2, Th21

        .= {( <*> X)} by FINSEQ_2: 94;

        let x be object;

        assume x in {( <*> X)};

        then x = {} by TARSKI:def 1;

        hence (f . x) = (g . x) by A3;

      end;

      hence thesis;

    end;

    theorem :: COMPUT_1:48



     Th47: for f,g be non empty len-total homogeneous to-naturals( NAT * ) -defined Function st ( arity f) = 0 & ( arity g) = 0 & (f . {} ) = (g . {} ) holds f = g

    proof

      let f,g be non empty len-total homogeneous to-naturals( NAT * ) -defined Function;

      assume that

       A1: ( arity f) = 0 and

       A2: ( arity g) = 0 and

       A3: (f . {} ) = (g . {} );



       A4: g is non empty quasi_total Element of ( HFuncs NAT ) by Th28;

      f is non empty quasi_total Element of ( HFuncs NAT ) by Th28;

      hence thesis by A1, A2, A3, A4, Th46;

    end;

    begin

    reserve f1,f2 for non empty homogeneous to-naturals( NAT * ) -defined Function,

e1,e2 for homogeneous to-naturals( NAT * ) -defined Function,

p for Element of ((( arity f1) + 1) -tuples_on NAT );

    definition

      let g,f1,f2 be homogeneous to-naturals( NAT * ) -defined Function, i be Element of NAT ;

      :: COMPUT_1:def9

      pred g is_primitive-recursively_expressed_by f1,f2,i means ex n be Element of NAT st ( dom g) c= (n -tuples_on NAT ) & i >= 1 & i <= n & (( arity f1) + 1) = n & (n + 1) = ( arity f2) & for p be FinSequence of NAT st ( len p) = n holds ((p +* (i, 0 )) in ( dom g) iff ( Del (p,i)) in ( dom f1)) & ((p +* (i, 0 )) in ( dom g) implies (g . (p +* (i, 0 ))) = (f1 . ( Del (p,i)))) & for n be Nat holds ((p +* (i,(n + 1))) in ( dom g) iff (p +* (i,n)) in ( dom g) & ((p +* (i,n)) ^ <*(g . (p +* (i,n)))*>) in ( dom f2)) & ((p +* (i,(n + 1))) in ( dom g) implies (g . (p +* (i,(n + 1)))) = (f2 . ((p +* (i,n)) ^ <*(g . (p +* (i,n)))*>)));

    end

    defpred Q[ Nat, Element of ( HFuncs NAT ), Element of ( HFuncs NAT ), FinSequence of NAT , Nat, homogeneous Function] means ($5 in ( dom $4) & ($4 +* ($5,$1)) in ( dom $2) & (($4 +* ($5,$1)) ^ <*($2 . ($4 +* ($5,$1)))*>) in ( dom $6) implies $3 = ($2 +* (($4 +* ($5,($1 + 1))) .--> ($6 . (($4 +* ($5,$1)) ^ <*($2 . ($4 +* ($5,$1)))*>))))) & ( not $5 in ( dom $4) or not ($4 +* ($5,$1)) in ( dom $2) or not (($4 +* ($5,$1)) ^ <*($2 . ($4 +* ($5,$1)))*>) in ( dom $6) implies $3 = $2);

    definition

      let f1,f2 be homogeneous to-naturals( NAT * ) -defined Function;

      let i be Nat;

      let p be FinSequence of NAT ;

      :: COMPUT_1:def10

      func primrec (f1,f2,i,p) -> Element of ( HFuncs NAT ) means

      : Def10: ex F be sequence of ( HFuncs NAT ) st it = (F . (p /. i)) & (i in ( dom p) & ( Del (p,i)) in ( dom f1) implies (F . 0 ) = ((p +* (i, 0 )) .--> (f1 . ( Del (p,i))))) & ( not i in ( dom p) or not ( Del (p,i)) in ( dom f1) implies (F . 0 ) = {} ) & for m be Nat holds (i in ( dom p) & (p +* (i,m)) in ( dom (F . m)) & ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>) in ( dom f2) implies (F . (m + 1)) = ((F . m) +* ((p +* (i,(m + 1))) .--> (f2 . ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>))))) & ( not i in ( dom p) or not (p +* (i,m)) in ( dom (F . m)) or not ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>) in ( dom f2) implies (F . (m + 1)) = (F . m));

      existence

      proof

        reconsider ff1 = f1, ff2 = f2 as Element of ( HFuncs NAT ) by Th27;

        set n = ( len p);

        reconsider z = (ff1 . ( Del (p,i))) as Element of NAT ;

        defpred A[ Nat, Element of ( HFuncs NAT ), Element of ( HFuncs NAT )] means Q[$1, $2, $3, p, i, ff2];

        (p +* (i, 0 )) in ( NAT * ) by FINSEQ_1:def 11;

        then

        reconsider Ap = {(p +* (i, 0 ))} as non empty Subset of ( NAT * ) by ZFMISC_1: 31;

         {} is PartFunc of ( NAT * ), NAT by RELSET_1: 12;

        then {} in ( PFuncs (( NAT * ), NAT )) by PARTFUN1: 45;

        then

         A1: {} in ( HFuncs NAT );

        (Ap --> z) = ((p +* (i, 0 )) .--> z);

        then (Ap --> z) in ( HFuncs NAT );

        then

        reconsider t = (Ap --> z), e = {} as Element of ( HFuncs NAT ) by A1;

        i in ( dom p) & ( Del (p,i)) in ( dom f1) or not i in ( dom p) or not ( Del (p,i)) in ( dom f1);

        then

        consider A be Element of ( HFuncs NAT ) such that

         A2: i in ( dom p) & ( Del (p,i)) in ( dom f1) implies A = t and

         A3: not i in ( dom p) or not ( Del (p,i)) in ( dom f1) implies A = e;



         A4: for m be Nat holds for x be Element of ( HFuncs NAT ) holds ex y be Element of ( HFuncs NAT ) st A[m, x, y]

        proof

          let m be Nat, x be Element of ( HFuncs NAT );

          set f = (x +* ( {(p +* (i,(m + 1)))} --> (f2 . ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>))));

          reconsider z = (ff2 . ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>)) as Element of NAT ;

          i in ( dom p) & (p +* (i,m)) in ( dom x) & ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>) in ( dom f2) or not i in ( dom p) or not (p +* (i,m)) in ( dom x) or not ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>) in ( dom f2);

          then

          consider y be Function such that

           A5: i in ( dom p) & (p +* (i,m)) in ( dom x) & ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>) in ( dom f2) & y = (x +* ( {(p +* (i,(m + 1)))} --> (f2 . ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>)))) or ( not i in ( dom p) or not (p +* (i,m)) in ( dom x) or not ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>) in ( dom f2)) & y = x;

          (p +* (i,(m + 1))) in ( NAT * ) by FINSEQ_1:def 11;

          then

          reconsider B = {(p +* (i,(m + 1)))} as Subset of ( NAT * ) by ZFMISC_1: 31;

          ( dom (B --> z)) = B;

          then

           A6: ( dom f) = (( dom x) \/ B) by FUNCT_4:def 1;

          ( dom p) = ( dom (p +* (i,(m + 1)))) by FUNCT_7: 30;

          then ( len (p +* (i,(m + 1)))) = n by FINSEQ_3: 29;

          then (p +* (i,(m + 1))) is Element of (n -tuples_on NAT ) by FINSEQ_2: 92;

          then

           A7: B c= (n -tuples_on NAT ) by ZFMISC_1: 31;



           A8: f = (x +* (B --> z));

          now

            assume

             A9: (p +* (i,m)) in ( dom x);

            ( dom x) c= (n -tuples_on NAT )

            proof

              let a be object;



               A10: ( dom p) = ( dom (p +* (i,m))) by FUNCT_7: 30;

              assume

               A11: a in ( dom x);

              then

              reconsider q = a as Element of ( NAT * );

              ( len q) = ( len (p +* (i,m))) by A9, A11, MARGREL1:def 1;

              then ( len q) = n by A10, FINSEQ_3: 29;

              hence thesis;

            end;

            then

             A12: f is homogeneous by A7, A6, Th15, XBOOLE_1: 8;

            f in ( PFuncs (( NAT * ), NAT )) by A8, PARTFUN1: 45;

            hence f in ( HFuncs NAT ) by A12;

          end;

          then

          reconsider y as Element of ( HFuncs NAT ) by A5;

          take y;

          thus i in ( dom p) & (p +* (i,m)) in ( dom x) & ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>) in ( dom ff2) implies y = (x +* ((p +* (i,(m + 1))) .--> (ff2 . ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>)))) by A5;

          thus not i in ( dom p) or not (p +* (i,m)) in ( dom x) or not ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>) in ( dom ff2) implies y = x by A5;

        end;

        consider FF be sequence of ( HFuncs NAT ) such that

         A13: (FF . 0 ) = A and

         A14: for m be Nat holds A[m, (FF . m) qua Element of ( HFuncs NAT ), (FF . (m + 1)) qua Element of ( HFuncs NAT )] from RECDEF_1:sch 2( A4);

        take (FF . (p /. i)), FF;

        thus thesis by A2, A3, A13, A14;

      end;

      uniqueness

      proof

        reconsider ff2 = f2 as Element of ( HFuncs NAT ) by Th27;

        let g1,g2 be Element of ( HFuncs NAT );

        given F1 be sequence of ( HFuncs NAT ) such that

         A15: g1 = (F1 . (p /. i)) and

         A16: i in ( dom p) & ( Del (p,i)) in ( dom f1) implies (F1 . 0 ) = ((p +* (i, 0 )) .--> (f1 . ( Del (p,i)))) and

         A17: not i in ( dom p) or not ( Del (p,i)) in ( dom f1) implies (F1 . 0 ) = {} and

         A18: for m be Nat holds Q[m, (F1 . m) qua Element of ( HFuncs NAT ), (F1 . (m + 1)) qua Element of ( HFuncs NAT ), p, i, f2];

        given F2 be sequence of ( HFuncs NAT ) such that

         A19: g2 = (F2 . (p /. i)) and

         A20: i in ( dom p) & ( Del (p,i)) in ( dom f1) implies (F2 . 0 ) = ((p +* (i, 0 )) .--> (f1 . ( Del (p,i)))) and

         A21: not i in ( dom p) or not ( Del (p,i)) in ( dom f1) implies (F2 . 0 ) = {} and

         A22: for m be Nat holds Q[m, (F2 . m) qua Element of ( HFuncs NAT ), (F2 . (m + 1)) qua Element of ( HFuncs NAT ), p, i, f2];

        defpred p[ Nat] means (F1 . $1) = (F2 . $1);

         A23:

        now

          let m be Nat;

          assume p[m];

          then

           A24: Q[m, (F1 . m) qua Element of ( HFuncs NAT ), (F2 . (m + 1)) qua Element of ( HFuncs NAT ), p, i, ff2] by A22;

           Q[m, (F1 . m) qua Element of ( HFuncs NAT ), (F1 . (m + 1)) qua Element of ( HFuncs NAT ), p, i, f2] by A18;

          hence p[(m + 1)] by A24;

        end;



         A25: p[ 0 ] by A16, A17, A20, A21;

        for m be Nat holds p[m] from NAT_1:sch 2( A25, A23);

        hence thesis by A15, A19;

      end;

    end

    theorem :: COMPUT_1:49



     Th48: for i be Nat holds for p,q be FinSequence of NAT st q in ( dom ( primrec (e1,e2,i,p))) holds ex k st q = (p +* (i,k))

    proof

      let i be Nat;

      set f1 = e1, f2 = e2;

      let p,q be FinSequence of NAT such that

       A1: q in ( dom ( primrec (f1,f2,i,p)));

      consider F be sequence of ( HFuncs NAT ) such that

       A2: ( primrec (f1,f2,i,p)) = (F . (p /. i)) and

       A3: i in ( dom p) & ( Del (p,i)) in ( dom f1) implies (F . 0 ) = ((p +* (i, 0 )) .--> (f1 . ( Del (p,i)))) and

       A4: not i in ( dom p) or not ( Del (p,i)) in ( dom f1) implies (F . 0 ) = {} and

       A5: for m be Nat holds Q[m, (F . m) qua Element of ( HFuncs NAT ), (F . (m + 1)) qua Element of ( HFuncs NAT ), p, i, f2] by Def10;

      defpred p[ Nat] means q in ( dom (F . $1)) implies ex k be Element of NAT st q = (p +* (i,k));



       A6: for m be Nat st p[m] holds p[(m + 1)]

      proof

        let m be Nat such that

         A7: p[m] and

         A8: q in ( dom (F . (m + 1)));

        per cases ;

          suppose i in ( dom p) & (p +* (i,m)) in ( dom (F . m)) & ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>) in ( dom f2);

          then (F . (m + 1)) = ((F . m) +* ((p +* (i,(m + 1))) .--> (f2 . ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>)))) by A5;

          then ( dom (F . (m + 1))) = (( dom (F . m)) \/ ( dom ((p +* (i,(m + 1))) .--> (f2 . ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>))))) by FUNCT_4:def 1;

          then

           A9: ( dom (F . (m + 1))) = (( dom (F . m)) \/ {(p +* (i,(m + 1)))});

          thus ex k be Element of NAT st q = (p +* (i,k))

          proof

            per cases by A8, A9, XBOOLE_0:def 3;

              suppose q in ( dom (F . m));

              hence thesis by A7;

            end;

              suppose q in {(p +* (i,(m + 1)))};

              then q = (p +* (i,(m + 1))) by TARSKI:def 1;

              hence thesis;

            end;

          end;

        end;

          suppose not i in ( dom p) or not (p +* (i,m)) in ( dom (F . m)) or not ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>) in ( dom f2);

          hence thesis by A5, A7, A8;

        end;

      end;



       A10: p[ 0 ]

      proof

        assume

         A11: q in ( dom (F . 0 ));

        per cases ;

          suppose i in ( dom p) & ( Del (p,i)) in ( dom f1);

          then ( dom (F . 0 )) = {(p +* (i, 0 ))} by A3;

          then (p +* (i, 0 )) = q by A11, TARSKI:def 1;

          hence thesis;

        end;

          suppose not i in ( dom p) or not ( Del (p,i)) in ( dom f1);

          hence thesis by A4, A11;

        end;

      end;

      for n be Nat holds p[n] from NAT_1:sch 2( A10, A6);

      hence thesis by A1, A2;

    end;

    theorem :: COMPUT_1:50



     Th49: for i be Nat holds for p be FinSequence of NAT st not i in ( dom p) holds ( primrec (e1,e2,i,p)) = {}

    proof

      let i be Nat;

      set f1 = e1, f2 = e2;

      let p be FinSequence of NAT ;

      consider F be sequence of ( HFuncs NAT ) such that

       A1: ( primrec (f1,f2,i,p)) = (F . (p /. i)) and i in ( dom p) & ( Del (p,i)) in ( dom f1) implies (F . 0 ) = ((p +* (i, 0 )) .--> (f1 . ( Del (p,i)))) and

       A2: not i in ( dom p) or not ( Del (p,i)) in ( dom f1) implies (F . 0 ) = {} and

       A3: for m be Nat holds Q[m, (F . m) qua Element of ( HFuncs NAT ), (F . (m + 1)) qua Element of ( HFuncs NAT ), p, i, f2] by Def10;

      defpred p[ Nat] means (F . $1) = {} ;

      assume

       A4: not i in ( dom p);

      then

       A5: for m be Nat st p[m] holds p[(m + 1)] by A3;



       A6: p[ 0 ] by A4, A2;

      for m be Nat holds p[m] from NAT_1:sch 2( A6, A5);

      hence thesis by A1;

    end;

    theorem :: COMPUT_1:51



     Th50: for i be Nat holds for p,q be FinSequence of NAT holds ( primrec (e1,e2,i,p)) tolerates ( primrec (e1,e2,i,q))

    proof

      let i be Nat;

      set f1 = e1, f2 = e2;

      let p1,p2 be FinSequence of NAT ;

      per cases ;

        suppose not i in ( dom p1) or not i in ( dom p2);

        then ( primrec (f1,f2,i,p1)) = {} or ( primrec (f1,f2,i,p2)) = {} by Th49;

        hence thesis;

      end;

        suppose

         A1: i in ( dom p1) & i in ( dom p2);

        reconsider m = (p1 /. i), n = (p2 /. i) as Element of NAT ;

        consider F2 be sequence of ( HFuncs NAT ) such that

         A2: ( primrec (f1,f2,i,p2)) = (F2 . (p2 /. i)) and

         A3: i in ( dom p2) & ( Del (p2,i)) in ( dom f1) implies (F2 . 0 ) = ((p2 +* (i, 0 )) .--> (f1 . ( Del (p2,i)))) and

         A4: not i in ( dom p2) or not ( Del (p2,i)) in ( dom f1) implies (F2 . 0 ) = {} and

         A5: for m be Nat holds Q[m, (F2 . m) qua Element of ( HFuncs NAT ), (F2 . (m + 1)) qua Element of ( HFuncs NAT ), p2, i, f2] by Def10;

        consider F1 be sequence of ( HFuncs NAT ) such that

         A6: ( primrec (f1,f2,i,p1)) = (F1 . (p1 /. i)) and

         A7: i in ( dom p1) & ( Del (p1,i)) in ( dom f1) implies (F1 . 0 ) = ((p1 +* (i, 0 )) .--> (f1 . ( Del (p1,i)))) and

         A8: not i in ( dom p1) or not ( Del (p1,i)) in ( dom f1) implies (F1 . 0 ) = {} and

         A9: for m be Nat holds Q[m, (F1 . m) qua Element of ( HFuncs NAT ), (F1 . (m + 1)) qua Element of ( HFuncs NAT ), p1, i, f2] by Def10;

        defpred p[ Nat] means for x be set st x in ( dom (F1 . $1)) holds ex n be Element of NAT st x = (p1 +* (i,n)) & n <= $1;

         A10:

        now

          let m be Nat such that

           A11: p[m];

          thus p[(m + 1)]

          proof

            set p1c = ((p1 +* (i,m)) ^ <*((F1 . m) . (p1 +* (i,m)))*>);

            let x be set such that

             A12: x in ( dom (F1 . (m + 1)));



             A13: m <= (m + 1) by NAT_1: 11;

            per cases ;

              suppose i in ( dom p1) & (p1 +* (i,m)) in ( dom (F1 . m)) & p1c in ( dom f2);

              then (F1 . (m + 1)) = ((F1 . m) +* ((p1 +* (i,(m + 1))) .--> (f2 . p1c))) by A9;



              then ( dom (F1 . (m + 1))) = (( dom (F1 . m)) \/ ( dom ((p1 +* (i,(m + 1))) .--> (f2 . p1c)))) by FUNCT_4:def 1

              .= (( dom (F1 . m)) \/ {(p1 +* (i,(m + 1)))});

              then

               A14: x in ( dom (F1 . m)) or x in {(p1 +* (i,(m + 1)))} by A12, XBOOLE_0:def 3;

              thus ex n be Element of NAT st x = (p1 +* (i,n)) & n <= (m + 1)

              proof

                per cases by A14, TARSKI:def 1;

                  suppose x in ( dom (F1 . m));

                  then ex n be Element of NAT st x = (p1 +* (i,n)) & n <= m by A11;

                  hence thesis by A13, XXREAL_0: 2;

                end;

                  suppose x = (p1 +* (i,(m + 1)));

                  hence thesis;

                end;

              end;

            end;

              suppose not i in ( dom p1) or not (p1 +* (i,m)) in ( dom (F1 . m)) or not p1c in ( dom f2);

              then (F1 . (m + 1)) = (F1 . m) by A9;

              then ex n be Element of NAT st x = (p1 +* (i,n)) & n <= m by A11, A12;

              hence thesis by A13, XXREAL_0: 2;

            end;

          end;

        end;

         A15:

        now

          defpred r[ Nat] means (F1 . $1) = (F2 . $1);

          assume

           A16: (p1 +* (i, 0 )) = (p2 +* (i, 0 ));



           A17: r[ 0 ]

          proof

            per cases ;

              suppose i in ( dom p1) & ( Del (p1,i)) in ( dom f1);

              hence thesis by A1, A7, A3, A16, Th4;

            end;

              suppose not i in ( dom p1) or not ( Del (p1,i)) in ( dom f1);

              hence thesis by A1, A8, A4, A16, Th4;

            end;

          end;

           A18:

          now

            let m be Nat such that

             A19: r[m];



             A20: Q[m, (F1 . m) qua Element of ( HFuncs NAT ), (F1 . (m + 1)) qua Element of ( HFuncs NAT ), p1, i, f2] by A9;



             A21: Q[m, (F2 . m) qua Element of ( HFuncs NAT ), (F2 . (m + 1)) qua Element of ( HFuncs NAT ), p2, i, f2] by A5;

            (p1 +* (i,m)) = (p2 +* (i,m)) by A16, Th2;

            hence r[(m + 1)] by A1, A19, A20, A21, Th2;

          end;

          thus for m be Nat holds r[m] from NAT_1:sch 2( A17, A18);

        end;



         A22: p[ 0 ]

        proof

          let x be set such that

           A23: x in ( dom (F1 . 0 ));

          ( dom (F1 . 0 )) = {(p1 +* (i, 0 ))} by A7, A8, A23;

          then x = (p1 +* (i, 0 )) by A23, TARSKI:def 1;

          hence thesis;

        end;



         A24: for m be Nat holds p[m] from NAT_1:sch 2( A22, A10);



         A25: for m,n be Nat holds (F1 . m) c= (F1 . (m + n))

        proof

          let m be Nat;

          defpred r[ Nat] means (F1 . m) c= (F1 . (m + $1));

           A26:

          now

            let n be Nat such that

             A27: r[n];

            set k = (m + n);

            (F1 . k) qua set c= (F1 . (k + 1)) qua set

            proof

              set p1c = ((p1 +* (i,k)) ^ <*((F1 . k) . (p1 +* (i,k)))*>);

              let x be object such that

               A28: x in (F1 . k);

              per cases ;

                suppose

                 A29: i in ( dom p1) & (p1 +* (i,k)) in ( dom (F1 . k)) & p1c in ( dom f2);



                 A30: ( dom (F1 . k)) misses ( dom ((p1 +* (i,(k + 1))) .--> (f2 . p1c)))

                proof

                  assume not thesis;

                  then

                  consider x be object such that

                   A31: x in (( dom (F1 . k)) /\ ( dom ( {(p1 +* (i,(k + 1)))} --> (f2 . p1c)))) by XBOOLE_0: 4;

                  x in ( dom (F1 . k)) by A31, XBOOLE_0:def 4;

                  then

                  consider n1 be Element of NAT such that

                   A32: x = (p1 +* (i,n1)) and

                   A33: n1 <= k by A24;



                   A34: (k + 1) = ((p1 +* (i,(k + 1))) . i) by A1, FUNCT_7: 31;



                   A35: x = (p1 +* (i,(k + 1))) by A31, TARSKI:def 1;

                  n1 = ((p1 +* (i,n1)) . i) by A1, FUNCT_7: 31;

                  hence contradiction by A35, A32, A33, A34, NAT_1: 13;

                end;

                (F1 . (k + 1)) = ((F1 . k) +* ((p1 +* (i,(k + 1))) .--> (f2 . p1c))) by A9, A29;

                then (F1 . k) c= (F1 . (k + 1)) by A30, FUNCT_4: 32;

                hence thesis by A28;

              end;

                suppose not i in ( dom p1) or not (p1 +* (i,k)) in ( dom (F1 . k)) or not p1c in ( dom f2);

                hence thesis by A9, A28;

              end;

            end;

            hence r[(n + 1)] by A27, XBOOLE_1: 1;

          end;



           A36: r[ 0 ];

          thus for n be Nat holds r[n] from NAT_1:sch 2( A36, A26);

        end;

        defpred p[ Nat] means for x be set st x in ( dom (F2 . $1)) holds ex n be Element of NAT st x = (p2 +* (i,n)) & n <= $1;

         A37:

        now

          let m be Nat such that

           A38: p[m];

          thus p[(m + 1)]

          proof

            set p2c = ((p2 +* (i,m)) ^ <*((F2 . m) . (p2 +* (i,m)))*>);

            let x be set such that

             A39: x in ( dom (F2 . (m + 1)));



             A40: m <= (m + 1) by NAT_1: 11;

            per cases ;

              suppose i in ( dom p2) & (p2 +* (i,m)) in ( dom (F2 . m)) & p2c in ( dom f2);

              then (F2 . (m + 1)) = ((F2 . m) +* ((p2 +* (i,(m + 1))) .--> (f2 . p2c))) by A5;



              then ( dom (F2 . (m + 1))) = (( dom (F2 . m)) \/ ( dom ((p2 +* (i,(m + 1))) .--> (f2 . p2c)))) by FUNCT_4:def 1

              .= (( dom (F2 . m)) \/ {(p2 +* (i,(m + 1)))});

              then

               A41: x in ( dom (F2 . m)) or x in {(p2 +* (i,(m + 1)))} by A39, XBOOLE_0:def 3;

              thus ex n be Element of NAT st x = (p2 +* (i,n)) & n <= (m + 1)

              proof

                per cases by A41, TARSKI:def 1;

                  suppose x in ( dom (F2 . m));

                  then ex n be Element of NAT st x = (p2 +* (i,n)) & n <= m by A38;

                  hence thesis by A40, XXREAL_0: 2;

                end;

                  suppose x = (p2 +* (i,(m + 1)));

                  hence thesis;

                end;

              end;

            end;

              suppose not i in ( dom p2) or not (p2 +* (i,m)) in ( dom (F2 . m)) or not p2c in ( dom f2);

              then (F2 . (m + 1)) = (F2 . m) by A5;

              then ex n be Element of NAT st x = (p2 +* (i,n)) & n <= m by A38, A39;

              hence thesis by A40, XXREAL_0: 2;

            end;

          end;

        end;



         A42: p[ 0 ]

        proof

          let x be set such that

           A43: x in ( dom (F2 . 0 ));

          ( dom (F2 . 0 )) = {(p2 +* (i, 0 ))} by A3, A4, A43;

          then x = (p2 +* (i, 0 )) by A43, TARSKI:def 1;

          hence thesis;

        end;



         A44: for m be Nat holds p[m] from NAT_1:sch 2( A42, A37);



         A45: for m,n be Nat holds (F2 . m) c= (F2 . (m + n))

        proof

          let m be Nat;

          defpred r[ Nat] means (F2 . m) c= (F2 . (m + $1));

           A46:

          now

            let n be Nat such that

             A47: r[n];

            set k = (m + n);

            (F2 . k) c= (F2 . (k + 1))

            proof

              set p2c = ((p2 +* (i,k)) ^ <*((F2 . k) . (p2 +* (i,k)))*>);

              let x be object such that

               A48: x in (F2 . k);

              per cases ;

                suppose

                 A49: i in ( dom p2) & (p2 +* (i,k)) in ( dom (F2 . k)) & p2c in ( dom f2);



                 A50: ( dom (F2 . k)) misses ( dom ((p2 +* (i,(k + 1))) .--> (f2 . p2c)))

                proof

                  assume not thesis;

                  then

                  consider x be object such that

                   A51: x in (( dom (F2 . k)) /\ ( dom ( {(p2 +* (i,(k + 1)))} --> (f2 . p2c)))) by XBOOLE_0: 4;

                  x in ( dom (F2 . k)) by A51, XBOOLE_0:def 4;

                  then

                  consider n2 be Element of NAT such that

                   A52: x = (p2 +* (i,n2)) and

                   A53: n2 <= k by A44;



                   A54: (k + 1) = ((p2 +* (i,(k + 1))) . i) by A1, FUNCT_7: 31;



                   A55: x = (p2 +* (i,(k + 1))) by A51, TARSKI:def 1;

                  n2 = ((p2 +* (i,n2)) . i) by A1, FUNCT_7: 31;

                  hence contradiction by A55, A52, A53, A54, NAT_1: 13;

                end;

                (F2 . (k + 1)) = ((F2 . k) +* ((p2 +* (i,(k + 1))) .--> (f2 . p2c))) by A5, A49;

                then (F2 . k) c= (F2 . (k + 1)) by A50, FUNCT_4: 32;

                hence thesis by A48;

              end;

                suppose not i in ( dom p2) or not (p2 +* (i,k)) in ( dom (F2 . k)) or not p2c in ( dom f2);

                hence thesis by A5, A48;

              end;

            end;

            hence r[(n + 1)] by A47, XBOOLE_1: 1;

          end;



           A56: r[ 0 ];

          thus for n be Nat holds r[n] from NAT_1:sch 2( A56, A46);

        end;

        reconsider F1m = (F1 . m), F1n = (F1 . n), F2m = (F2 . m), F2n = (F2 . n) as Element of ( HFuncs NAT );

         A57:

        now

          assume

           A58: (p1 +* (i, 0 )) <> (p2 +* (i, 0 ));

          let m be Element of NAT ;

          assume (( dom (F1 . m)) /\ ( dom (F2 . m))) <> {} ;

          then

          consider x be object such that

           A59: x in (( dom (F1 . m)) /\ ( dom (F2 . m))) by XBOOLE_0:def 1;

          x in ( dom (F2 . m)) by A59, XBOOLE_0:def 4;

          then

           A60: ex n2 be Element of NAT st x = (p2 +* (i,n2)) & n2 <= m by A44;

          x in ( dom (F1 . m)) by A59, XBOOLE_0:def 4;

          then ex n1 be Element of NAT st x = (p1 +* (i,n1)) & n1 <= m by A24;

          hence contradiction by A58, A60, Th2;

        end;

        thus thesis

        proof

          per cases ;

            suppose m <= n;

            then

            consider k be Nat such that

             A61: n = (m + k) by NAT_1: 10;

            reconsider k as Element of NAT by ORDINAL1:def 12;



             A62: n = (m + k) by A61;

            thus ( primrec (f1,f2,i,p1)) tolerates ( primrec (f1,f2,i,p2))

            proof

              per cases by A15, A57;

                suppose F1n = F2n;

                hence thesis by A6, A2, A25, A62, PARTFUN1: 58;

              end;

                suppose (( dom F1n) /\ ( dom F2n)) = {} ;

                then ( dom F1n) misses ( dom F2n) by XBOOLE_0:def 7;

                then F1n tolerates F2n by PARTFUN1: 56;

                hence thesis by A6, A2, A25, A62, PARTFUN1: 58;

              end;

            end;

          end;

            suppose m >= n;

            then

            consider k be Nat such that

             A63: m = (n + k) by NAT_1: 10;

            reconsider k as Element of NAT by ORDINAL1:def 12;



             A64: m = (n + k) by A63;

            thus ( primrec (f1,f2,i,p1)) tolerates ( primrec (f1,f2,i,p2))

            proof

              per cases by A15, A57;

                suppose F1m = F2m;

                hence thesis by A6, A2, A45, A64, PARTFUN1: 58;

              end;

                suppose (( dom F1m) /\ ( dom F2m)) = {} ;

                then ( dom F1m) misses ( dom F2m) by XBOOLE_0:def 7;

                then F1m tolerates F2m by PARTFUN1: 56;

                hence thesis by A6, A2, A45, A64, PARTFUN1: 58;

              end;

            end;

          end;

        end;

      end;

    end;

    theorem :: COMPUT_1:52



     Th51: for i be Nat holds for p be FinSequence of NAT holds ( dom ( primrec (e1,e2,i,p))) c= ((1 + ( arity e1)) -tuples_on NAT )

    proof

      let i be Nat;

      set f1 = e1, f2 = e2;

      let p be FinSequence of NAT ;

      per cases ;

        suppose

         A1: i in ( dom p);

        consider F be sequence of ( HFuncs NAT ) such that

         A2: ( primrec (f1,f2,i,p)) = (F . (p /. i)) and

         A3: i in ( dom p) & ( Del (p,i)) in ( dom f1) implies (F . 0 ) = ((p +* (i, 0 )) .--> (f1 . ( Del (p,i)))) and

         A4: not i in ( dom p) or not ( Del (p,i)) in ( dom f1) implies (F . 0 ) = {} and

         A5: for m be Nat holds Q[m, (F . m) qua Element of ( HFuncs NAT ), (F . (m + 1)) qua Element of ( HFuncs NAT ), p, i, f2] by Def10;

        defpred p[ Nat] means ( dom (F . $1)) c= ((1 + ( arity f1)) -tuples_on NAT );

         A6:

        now

          let m be Nat such that

           A7: p[m];

          set pc = ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>);

          per cases ;

            suppose

             A8: (p +* (i,m)) in ( dom (F . m)) & pc in ( dom f2);

            ( dom (p +* (i,m))) = ( dom p) by FUNCT_7: 30

            .= ( dom (p +* (i,(m + 1)))) by FUNCT_7: 30;

            then

             A9: ( len (p +* (i,m))) = ( len (p +* (i,(m + 1)))) by FINSEQ_3: 29;

            ( len (p +* (i,m))) = (1 + ( arity f1)) by A7, A8, CARD_1:def 7;

            then (p +* (i,(m + 1))) is Element of ((1 + ( arity f1)) -tuples_on NAT ) by A9, FINSEQ_2: 92;

            then

             A10: {(p +* (i,(m + 1)))} c= ((1 + ( arity f1)) -tuples_on NAT ) by ZFMISC_1: 31;

            (F . (m + 1)) = ((F . m) +* ((p +* (i,(m + 1))) .--> (f2 . pc))) by A1, A5, A8;

            then ( dom (F . (m + 1))) = (( dom (F . m)) \/ ( dom ((p +* (i,(m + 1))) .--> (f2 . pc)))) by FUNCT_4:def 1;

            then ( dom (F . (m + 1))) = (( dom (F . m)) \/ {(p +* (i,(m + 1)))});

            hence p[(m + 1)] by A7, A10, XBOOLE_1: 8;

          end;

            suppose not (p +* (i,m)) in ( dom (F . m)) or not pc in ( dom f2);

            hence p[(m + 1)] by A5, A7;

          end;

        end;



         A11: p[ 0 ]

        proof

          per cases ;

            suppose

             A12: ( Del (p,i)) in ( dom f1);

            ( dom f1) c= (( arity f1) -tuples_on NAT ) by Th20;

            then

             A13: ( len ( Del (p,i))) = ( arity f1) by A12, CARD_1:def 7;



             A14: ( dom p) = ( dom (p +* (i, 0 ))) by FUNCT_7: 30;

            p <> ( <*> NAT ) by A1;

            then

            consider n be Nat such that

             A15: ( len p) = (n + 1) by NAT_1: 6;

            ( len ( Del (p,i))) = n by A1, A15, FINSEQ_3: 109;

            then ( len (p +* (i, 0 ))) = (1 + ( arity f1)) by A13, A15, A14, FINSEQ_3: 29;

            then

             A16: (p +* (i, 0 )) is Element of ((1 + ( arity f1)) -tuples_on NAT ) by FINSEQ_2: 92;

            ( dom (F . 0 )) = {(p +* (i, 0 ))} by A1, A3, A12;

            hence thesis by A16, ZFMISC_1: 31;

          end;

            suppose not ( Del (p,i)) in ( dom f1);

            hence thesis by A4, XBOOLE_1: 2;

          end;

        end;

        for m be Nat holds p[m] from NAT_1:sch 2( A11, A6);

        hence thesis by A2;

      end;

        suppose not i in ( dom p);

        then ( primrec (f1,f2,i,p)) = {} by Th49;

        hence thesis;

      end;

    end;

    theorem :: COMPUT_1:53



     Th52: for p be FinSequence of NAT st e1 is empty holds ( primrec (e1,e2,i,p)) is empty

    proof

      set f1 = e1, f2 = e2;

      let p be FinSequence of NAT ;

      consider F be sequence of ( HFuncs NAT ) such that

       A1: ( primrec (f1,f2,i,p)) = (F . (p /. i)) and i in ( dom p) & ( Del (p,i)) in ( dom f1) implies (F . 0 ) = ((p +* (i, 0 )) .--> (f1 . ( Del (p,i)))) and

       A2: not i in ( dom p) or not ( Del (p,i)) in ( dom f1) implies (F . 0 ) = {} and

       A3: for m be Nat holds (i in ( dom p) & (p +* (i,m)) in ( dom (F . m)) & ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>) in ( dom f2) implies (F . (m + 1)) = ((F . m) +* ((p +* (i,(m + 1))) .--> (f2 . ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>))))) & ( not i in ( dom p) or not (p +* (i,m)) in ( dom (F . m)) or not ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>) in ( dom f2) implies (F . (m + 1)) = (F . m)) by Def10;

      defpred p[ Nat] means (F . $1) = {} ;



       A4: for k be Nat st p[k] holds p[(k + 1)] by A3, RELAT_1: 38;

      assume f1 is empty;

      then

       A5: p[ 0 ] by A2;

      for k be Nat holds p[k] from NAT_1:sch 2( A5, A4);

      hence thesis by A1;

    end;

    theorem :: COMPUT_1:54



     Th53: f1 is len-total & f2 is len-total & (( arity f1) + 2) = ( arity f2) & 1 <= i & i <= (1 + ( arity f1)) implies p in ( dom ( primrec (f1,f2,i,p)))

    proof

      assume that

       A1: f1 is len-total and

       A2: f2 is len-total and

       A3: (( arity f1) + 2) = ( arity f2) and

       A4: 1 <= i and

       A5: i <= (1 + ( arity f1));



       A6: ( len p) = (1 + ( arity f1)) by CARD_1:def 7;

      then

       A7: i in ( dom p) by A4, A5, FINSEQ_3: 25;

      then

       A8: (p /. i) = (p . i) by PARTFUN1:def 6;

      consider F be sequence of ( HFuncs NAT ) such that

       A9: ( primrec (f1,f2,i,p)) = (F . (p /. i)) and

       A10: i in ( dom p) & ( Del (p,i)) in ( dom f1) implies (F . 0 ) = ((p +* (i, 0 )) .--> (f1 . ( Del (p,i)))) and not i in ( dom p) or not ( Del (p,i)) in ( dom f1) implies (F . 0 ) = {} and

       A11: for m be Nat holds (i in ( dom p) & (p +* (i,m)) in ( dom (F . m)) & ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>) in ( dom f2) implies (F . (m + 1)) = ((F . m) +* ((p +* (i,(m + 1))) .--> (f2 . ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>))))) & ( not i in ( dom p) or not (p +* (i,m)) in ( dom (F . m)) or not ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>) in ( dom f2) implies (F . (m + 1)) = (F . m)) by Def10;

      defpred p[ Nat] means (p +* (i,$1)) in ( dom (F . $1));



       A12: (p +* (i,(p . i))) = p by FUNCT_7: 35;

       A13:

      now

        let m be Nat such that

         A14: p[m];

        reconsider aa = ((F . m) . (p +* (i,m))) as Element of NAT ;

        reconsider mm = m as Element of NAT by ORDINAL1:def 12;

        set pc = ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>);

        reconsider p2 = <*aa*> as FinSequence of NAT ;

        reconsider p1 = ((p +* (i,mm)) ^ p2) as FinSequence of NAT ;



         A15: ( len p2) = 1 by CARD_1:def 7;

        ( len (p +* (i,mm))) = (1 + ( arity f1)) by CARD_1:def 7;



        then ( len p1) = ((( arity f1) + 1) + 1) by A15, FINSEQ_1: 22

        .= ( arity f2) by A3;

        then

         A16: p1 is Element of (( arity f2) -tuples_on NAT ) by FINSEQ_2: 92;

        (p +* (i,(m + 1))) in {(p +* (i,(m + 1)))} by TARSKI:def 1;

        then

         A17: (p +* (i,(m + 1))) in ( dom ( {(p +* (i,(m + 1)))} --> (f2 . pc)));

        ( dom f2) = (( arity f2) -tuples_on NAT ) by A2, Th22;

        then (F . (m + 1)) = ((F . m) +* ((p +* (i,(m + 1))) .--> (f2 . pc))) by A7, A11, A14, A16;

        then ( dom (F . (m + 1))) = (( dom (F . m)) \/ ( dom ( {(p +* (i,(m + 1)))} --> (f2 . pc)))) by FUNCT_4:def 1;

        hence p[(m + 1)] by A17, XBOOLE_0:def 3;

      end;

       A18:

      now

        reconsider Dpi = ( Del (p,i)) as FinSequence of NAT by FINSEQ_3: 105;

        reconsider Dpi9 = Dpi as Element of (( len Dpi) -tuples_on NAT ) by FINSEQ_2: 92;



         A19: ( dom f1) = (( arity f1) -tuples_on NAT ) by A1, Th22;

        ( len ( Del (p,i))) = ( arity f1) by A6, A7, FINSEQ_3: 109;

        then Dpi9 in ( dom f1) by A19;

        then ( dom (F . 0 )) = {(p +* (i, 0 ))} by A4, A5, A6, A10, FINSEQ_3: 25;

        hence p[ 0 ] by TARSKI:def 1;

      end;

      for m be Nat holds p[m] from NAT_1:sch 2( A18, A13);

      hence thesis by A8, A9, A12;

    end;

    definition

      let f1,f2 be homogeneous to-naturals( NAT * ) -defined Function;

      let i be Nat;

      :: COMPUT_1:def11

      func primrec (f1,f2,i) -> Element of ( HFuncs NAT ) means

      : Def11: ex G be Function of ((( arity f1) + 1) -tuples_on NAT ), ( HFuncs NAT ) st it = ( Union G) & for p be Element of ((( arity f1) + 1) -tuples_on NAT ) holds (G . p) = ( primrec (f1,f2,i,p));

      existence

      proof

        deffunc f( FinSequence of NAT ) = ( primrec (f1,f2,i,$1));

        reconsider ff1 = f1, ff2 = f2 as Element of ( HFuncs NAT ) by Th27;

        set n = (( arity f1) + 1);

        consider G be Function of (n -tuples_on NAT ), ( HFuncs NAT ) such that

         A1: for p be Element of (n -tuples_on NAT ) holds (G . p) = f(p) from FUNCT_2:sch 4;

        reconsider Y = ( rng G) as non empty Subset of ( HFuncs NAT ) by RELAT_1:def 19;

        Y is PartFunc-set of ( NAT * ), NAT

        proof

          let f be Element of Y;

          thus thesis;

        end;

        then

        reconsider Y as PFUNC_DOMAIN of ( NAT * ), NAT ;



         A2: Y is compatible

        proof

          let f,g be Function;

          assume f in Y;

          then

          consider x be object such that

           A3: x in ( dom G) and

           A4: f = (G . x) by FUNCT_1:def 3;

          assume g in Y;

          then

          consider y be object such that

           A5: y in ( dom G) and

           A6: g = (G . y) by FUNCT_1:def 3;

          reconsider x, y as Element of (n -tuples_on NAT ) by A3, A5;



           A7: g = ( primrec (ff1,ff2,i,y)) by A1, A6;

          f = ( primrec (ff1,ff2,i,x)) by A1, A4;

          hence thesis by A7, Th50;

        end;

        now

          let x be Element of (n -tuples_on NAT );

          (G . x) = ( primrec (ff1,ff2,i,x)) by A1;

          hence ( dom (G . x)) c= (n -tuples_on NAT ) by Th51;

        end;

        then

        consider g be Element of ( HFuncs NAT ) such that

         A8: g = ( Union G) and ( dom g) c= (n -tuples_on NAT ) by A2, Th38;

        take g, G;

        thus thesis by A1, A8;

      end;

      uniqueness

      proof

        let g1,g2 be Element of ( HFuncs NAT );

        given G1 be Function of ((( arity f1) + 1) -tuples_on NAT ), ( HFuncs NAT ) such that

         A9: g1 = ( Union G1) and

         A10: for p be Element of ((( arity f1) + 1) -tuples_on NAT ) holds (G1 . p) = ( primrec (f1,f2,i,p));

        given G2 be Function of ((( arity f1) + 1) -tuples_on NAT ), ( HFuncs NAT ) such that

         A11: g2 = ( Union G2) and

         A12: for p be Element of ((( arity f1) + 1) -tuples_on NAT ) holds (G2 . p) = ( primrec (f1,f2,i,p));

        now

          let p be Element of ((( arity f1) + 1) -tuples_on NAT );



          thus (G1 . p) = ( primrec (f1,f2,i,p)) by A10

          .= (G2 . p) by A12;

        end;

        hence thesis by A9, A11, FUNCT_2: 63;

      end;

    end

    theorem :: COMPUT_1:55



     Th54: e1 is empty implies ( primrec (e1,e2,i)) is empty

    proof

      set f1 = e1, f2 = e2;

      assume

       A1: f1 is empty;

      consider G be Function of ((( arity f1) + 1) -tuples_on NAT ), ( HFuncs NAT ) such that

       A2: ( primrec (f1,f2,i)) = ( Union G) and

       A3: for p be Element of ((( arity f1) + 1) -tuples_on NAT ) holds (G . p) = ( primrec (f1,f2,i,p)) by Def11;



       A4: ( dom G) = ((( arity f1) + 1) -tuples_on NAT ) by FUNCT_2:def 1;

      now

        set p = the Element of ((( arity f1) + 1) -tuples_on NAT );

        let y be object;

        hereby

          assume y in ( rng G);

          then

          consider x be object such that

           A5: x in ( dom G) and

           A6: (G . x) = y by FUNCT_1:def 3;

          reconsider p = x as Element of ((( arity f1) + 1) -tuples_on NAT ) by A5;

          (G . p) = ( primrec (f1,f2,i,p)) by A3

          .= {} by A1, Th52;

          hence y in { {} } by A6, TARSKI:def 1;

        end;

        assume y in { {} };

        then

         A7: y = {} by TARSKI:def 1;

        (G . p) = ( primrec (f1,f2,i,p)) by A3

        .= {} by A1, Th52;

        hence y in ( rng G) by A4, A7, FUNCT_1: 3;

      end;

      then

       A8: ( rng G) = { {} } by TARSKI: 2;

      ( Union G) = ( union ( rng G))

      .= {} by A8, ZFMISC_1: 25;

      hence thesis by A2;

    end;

    theorem :: COMPUT_1:56



     Th55: ( dom ( primrec (f1,f2,i))) c= ((( arity f1) + 1) -tuples_on NAT )

    proof

      let x be object such that

       A1: x in ( dom ( primrec (f1,f2,i)));

      consider G be Function of ((( arity f1) + 1) -tuples_on NAT ), ( HFuncs NAT ) such that

       A2: ( primrec (f1,f2,i)) = ( Union G) and

       A3: for p be Element of ((( arity f1) + 1) -tuples_on NAT ) holds (G . p) = ( primrec (f1,f2,i,p)) by Def11;



       A4: ( rng G) is compatible

      proof

        let f,g be Function such that

         A5: f in ( rng G) and

         A6: g in ( rng G);

        consider fx be object such that

         A7: fx in ( dom G) and

         A8: f = (G . fx) by A5, FUNCT_1:def 3;

        reconsider fx as Element of ((( arity f1) + 1) -tuples_on NAT ) by A7;

        consider gx be object such that

         A9: gx in ( dom G) and

         A10: g = (G . gx) by A6, FUNCT_1:def 3;

        reconsider gx as Element of ((( arity f1) + 1) -tuples_on NAT ) by A9;



         A11: (G . gx) = ( primrec (f1,f2,i,gx)) by A3;

        (G . fx) = ( primrec (f1,f2,i,fx)) by A3;

        hence thesis by A8, A10, A11, Th50;

      end;

      now

        let x be Element of ((( arity f1) + 1) -tuples_on NAT );

        (G . x) = ( primrec (f1,f2,i,x)) by A3;

        hence ( dom (G . x)) c= ((( arity f1) + 1) -tuples_on NAT ) by Th51;

      end;

      then ex F be Element of ( HFuncs NAT ) st F = ( Union G) & ( dom F) c= ((( arity f1) + 1) -tuples_on NAT ) by A4, Th38;

      hence thesis by A1, A2;

    end;

    theorem :: COMPUT_1:57



     Th56: f1 is len-total & f2 is len-total & (( arity f1) + 2) = ( arity f2) & 1 <= i & i <= (1 + ( arity f1)) implies ( dom ( primrec (f1,f2,i))) = ((( arity f1) + 1) -tuples_on NAT ) & ( arity ( primrec (f1,f2,i))) = (( arity f1) + 1)

    proof

      assume that

       A1: f1 is len-total and

       A2: f2 is len-total and

       A3: (( arity f1) + 2) = ( arity f2) and

       A4: 1 <= i and

       A5: i <= (1 + ( arity f1));

      set n = (( arity f1) + 1);



       A6: (n -tuples_on NAT ) c= ( dom ( primrec (f1,f2,i)))

      proof

        let x be object;

        assume x in (n -tuples_on NAT );

        then

        reconsider x9 = x as Element of (n -tuples_on NAT );

        consider G be Function of (n -tuples_on NAT ), ( HFuncs NAT ) such that

         A7: ( primrec (f1,f2,i)) = ( Union G) and

         A8: for p be Element of (n -tuples_on NAT ) holds (G . p) = ( primrec (f1,f2,i,p)) by Def11;

        reconsider rngG = ( rng G) as non empty functional compatible set by A7, Th10;



         A9: ( dom ( union rngG)) = ( union the set of all ( dom f) where f be Element of rngG) by Th11;

        ( dom G) = (n -tuples_on NAT ) by FUNCT_2:def 1;

        then (G . x9) in ( rng G) by FUNCT_1: 3;

        then

         A10: ( dom (G . x9)) in the set of all ( dom f) where f be Element of rngG;



         A11: x9 in ( dom ( primrec (f1,f2,i,x9))) by A1, A2, A3, A4, A5, Th53;

        (G . x9) = ( primrec (f1,f2,i,x9)) by A8;

        hence thesis by A7, A11, A9, A10, TARSKI:def 4;

      end;

      ( dom ( primrec (f1,f2,i))) c= ((( arity f1) + 1) -tuples_on NAT ) by Th55;

      hence ( dom ( primrec (f1,f2,i))) = ((( arity f1) + 1) -tuples_on NAT ) by A6;

      hence thesis by Th24;

    end;

     Lm2:

    now

      let f1,f2 be non empty homogeneous to-naturals( NAT * ) -defined Function;

      let p be Element of ((( arity f1) + 1) -tuples_on NAT );

      let i be Nat, m be Element of NAT ;

      set pm1 = (p +* (i,(m + 1))), pm = (p +* (i,m));

      let F1,F be sequence of ( HFuncs NAT ) such that

       A1: i in ( dom pm1) & ( Del (pm1,i)) in ( dom f1) implies (F1 . 0 ) = ( {(pm1 +* (i, 0 ))} --> (f1 . ( Del (pm1,i)))) and

       A2: not i in ( dom pm1) or not ( Del (pm1,i)) in ( dom f1) implies (F1 . 0 ) = {} and

       A3: for M be Nat holds Q[M, (F1 . M) qua Element of ( HFuncs NAT ), (F1 . (M + 1)) qua Element of ( HFuncs NAT ), pm1, i, f2] and

       A4: i in ( dom pm) & ( Del (pm,i)) in ( dom f1) implies (F . 0 ) = ( {(pm +* (i, 0 ))} --> (f1 . ( Del (pm,i)))) and

       A5: not i in ( dom pm) or not ( Del (pm,i)) in ( dom f1) implies (F . 0 ) = {} and

       A6: for M be Nat holds Q[M, (F . M) qua Element of ( HFuncs NAT ), (F . (M + 1)) qua Element of ( HFuncs NAT ), pm, i, f2];



       A7: ( dom p) = ( dom pm) by FUNCT_7: 30;



       A8: (pm +* (i, 0 )) = (p +* (i, 0 )) by FUNCT_7: 34

      .= (pm1 +* (i, 0 )) by FUNCT_7: 34;



       A9: ( dom p) = ( dom pm1) by FUNCT_7: 30;



       A10: ( Del (pm,i)) = ( Del (p,i)) by Th3

      .= ( Del (pm1,i)) by Th3;

      for x be object st x in NAT holds (F . x) = (F1 . x)

      proof

        let x be object;

        defpred p[ Nat] means (F . $1) = (F1 . $1);



         A11: for k be Nat st p[k] holds p[(k + 1)]

        proof

          let k be Nat such that

           A12: p[k];



           A13: (pm +* (i,(k + 1))) = (p +* (i,(k + 1))) by FUNCT_7: 34

          .= (pm1 +* (i,(k + 1))) by FUNCT_7: 34;



           A14: (pm +* (i,k)) = (p +* (i,k)) by FUNCT_7: 34

          .= (pm1 +* (i,k)) by FUNCT_7: 34;

          per cases ;

            suppose

             A15: i in ( dom pm) & (pm +* (i,k)) in ( dom (F . k)) & ((pm +* (i,k)) ^ <*((F . k) . (pm +* (i,k)))*>) in ( dom f2);



            hence (F . (k + 1)) = ((F . k) +* ((pm +* (i,(k + 1))) .--> (f2 . ((pm +* (i,k)) ^ <*((F . k) . (pm +* (i,k)))*>)))) by A6

            .= (F1 . (k + 1)) by A3, A7, A9, A12, A14, A13, A15;

          end;

            suppose

             A16: not i in ( dom pm) or not (pm +* (i,k)) in ( dom (F . k)) or not ((pm +* (i,k)) ^ <*((F . k) . (pm +* (i,k)))*>) in ( dom f2);



            hence (F . (k + 1)) = (F . k) by A6

            .= (F1 . (k + 1)) by A3, A7, A9, A12, A14, A16;

          end;

        end;



         A17: p[ 0 ] by A1, A2, A4, A5, A7, A8, A10, FUNCT_7: 30;



         A18: for k be Nat holds p[k] from NAT_1:sch 2( A17, A11);

        assume x in NAT ;

        hence thesis by A18;

      end;

      hence F1 = F by FUNCT_2: 12;

    end;

     Lm3:

    now

      let f1,f2 be non empty homogeneous to-naturals( NAT * ) -defined Function;

      let p be Element of ((( arity f1) + 1) -tuples_on NAT );

      let i,m be Element of NAT such that

       A1: i in ( dom p);

      set pm = (p +* (i,m)), pm1 = (p +* (i,(m + 1)));

      let F be sequence of ( HFuncs NAT ) such that

       A2: i in ( dom pm1) & ( Del (pm1,i)) in ( dom f1) implies (F . 0 ) = ( {(pm1 +* (i, 0 ))} --> (f1 . ( Del (pm1,i)))) and

       A3: not i in ( dom pm1) or not ( Del (pm1,i)) in ( dom f1) implies (F . 0 ) = {} and

       A4: for M be Nat holds Q[M, (F . M) qua Element of ( HFuncs NAT ), (F . (M + 1)) qua Element of ( HFuncs NAT ), pm1, i, f2];

      thus ((F . (m + 1)) . pm) = ((F . m) . pm)

      proof

        per cases ;

          suppose

           A5: i in ( dom pm1) & (pm1 +* (i,m)) in ( dom (F . m)) & ((pm1 +* (i,m)) ^ <*((F . m) . (pm1 +* (i,m)))*>) in ( dom f2);



           A6: pm1 = (pm1 +* (i,(m + 1))) by FUNCT_7: 34;



           A7: (pm1 . i) = (m + 1) by A1, FUNCT_7: 31;

          (pm . i) = m by A1, FUNCT_7: 31;

          then pm <> pm1 by A7;

          then

           A8: not pm in ( dom ( {(pm1 +* (i,(m + 1)))} --> (f2 . ((pm1 +* (i,m)) ^ <*((F . m) . (pm1 +* (i,m)))*>)))) by A6, TARSKI:def 1;

          (F . (m + 1)) = ((F . m) +* ((pm1 +* (i,(m + 1))) .--> (f2 . ((pm1 +* (i,m)) ^ <*((F . m) . (pm1 +* (i,m)))*>)))) by A4, A5;

          hence thesis by A8, FUNCT_4: 11;

        end;

          suppose not i in ( dom pm1) or not (pm1 +* (i,m)) in ( dom (F . m)) or not ((pm1 +* (i,m)) ^ <*((F . m) . (pm1 +* (i,m)))*>) in ( dom f2);

          hence thesis by A4;

        end;

      end;



       A9: for m,k be Nat st (p +* (i,k)) in ( dom (F . m)) holds k <= m

      proof

        defpred p[ Nat] means for k be Nat st (p +* (i,k)) in ( dom (F . $1)) holds k <= $1;



         A10: for m be Nat st p[m] holds p[(m + 1)]

        proof

          let m be Nat such that

           A11: p[m];

          let k be Nat such that

           A12: (p +* (i,k)) in ( dom (F . (m + 1)));

          per cases ;

            suppose i in ( dom pm1) & (pm1 +* (i,m)) in ( dom (F . m)) & ((pm1 +* (i,m)) ^ <*((F . m) . (pm1 +* (i,m)))*>) in ( dom f2);

            then (F . (m + 1)) = ((F . m) +* ((pm1 +* (i,(m + 1))) .--> (f2 . ((pm1 +* (i,m)) ^ <*((F . m) . (pm1 +* (i,m)))*>)))) by A4;

            then ( dom (F . (m + 1))) = (( dom (F . m)) \/ ( dom ( {(pm1 +* (i,(m + 1)))} --> (f2 . ((pm1 +* (i,m)) ^ <*((F . m) . (pm1 +* (i,m)))*>))))) by FUNCT_4:def 1;

            then

             A13: ( dom (F . (m + 1))) = (( dom (F . m)) \/ {(pm1 +* (i,(m + 1)))});

            thus k <= (m + 1)

            proof

              per cases by A12, A13, XBOOLE_0:def 3;

                suppose

                 A14: (p +* (i,k)) in ( dom (F . m));



                 A15: m <= (m + 1) by NAT_1: 11;

                k <= m by A11, A14;

                hence thesis by A15, XXREAL_0: 2;

              end;

                suppose (p +* (i,k)) in {(pm1 +* (i,(m + 1)))};



                then

                 A16: (p +* (i,k)) = (pm1 +* (i,(m + 1))) by TARSKI:def 1

                .= (p +* (i,(m + 1))) by FUNCT_7: 34;

                k = ((p +* (i,k)) . i) by A1, FUNCT_7: 31

                .= (m + 1) by A1, A16, FUNCT_7: 31;

                hence thesis;

              end;

            end;

          end;

            suppose not i in ( dom pm1) or not (pm1 +* (i,m)) in ( dom (F . m)) or not ((pm1 +* (i,m)) ^ <*((F . m) . (pm1 +* (i,m)))*>) in ( dom f2);

            then (F . (m + 1)) = (F . m) by A4;

            then

             A17: k <= m by A11, A12;

            m <= (m + 1) by NAT_1: 11;

            hence thesis by A17, XXREAL_0: 2;

          end;

        end;



         A18: p[ 0 ]

        proof

          let k be Nat such that

           A19: (p +* (i,k)) in ( dom (F . 0 ));

          per cases ;

            suppose i in ( dom pm1) & ( Del (pm1,i)) in ( dom f1);

            then ( dom (F . 0 )) = {(pm1 +* (i, 0 ))} by A2;



            then

             A20: (p +* (i,k)) = (pm1 +* (i, 0 )) by A19, TARSKI:def 1

            .= (p +* (i, 0 )) by FUNCT_7: 34;

            k = ((p +* (i,k)) . i) by A1, FUNCT_7: 31

            .= 0 by A1, A20, FUNCT_7: 31;

            hence thesis;

          end;

            suppose not i in ( dom pm1) or not ( Del (pm1,i)) in ( dom f1);

            hence thesis by A3, A19;

          end;

        end;

        thus for n be Nat holds p[n] from NAT_1:sch 2( A18, A10);

      end;

      thus not pm1 in ( dom (F . m))

      proof

        assume not thesis;

        then (m + 1) <= m by A9;

        hence contradiction by NAT_1: 13;

      end;

    end;

    definition

      let n be Nat, p be Element of (n -tuples_on NAT );

      let i,k be Element of NAT ;

      :: original: +*

      redefine

      func p +* (i,k) -> Element of (n -tuples_on NAT ) ;

      coherence

      proof

        thus (p +* (i,k)) is Element of (n -tuples_on NAT );

      end;

    end

     Lm4:

    now

      let f1,f2 be non empty homogeneous to-naturals( NAT * ) -defined Function;

      let p be Element of ((( arity f1) + 1) -tuples_on NAT );

      let i,m be Element of NAT such that

       A1: i in ( dom p);

      let G be Function of ((( arity f1) + 1) -tuples_on NAT ), ( HFuncs NAT ) such that

       A2: for p be Element of ((( arity f1) + 1) -tuples_on NAT ) holds (G . p) = ( primrec (f1,f2,i,p));

      thus for k,n be Nat holds ( dom (G . (p +* (i,k)))) c= ( dom (G . (p +* (i,(k + n)))))

      proof

        let k be Nat;

        set pk = (p +* (i,k));

        defpred p[ Nat] means ( dom (G . pk)) c= ( dom (G . (p +* (i,(k + $1)))));

         A3:

        now

          let n be Nat such that

           A4: p[n];

          reconsider m = (k + n) as Element of NAT by ORDINAL1:def 12;

          set pkn1 = (p +* (i,(m + 1)));

          set pkn = (p +* (i,m));

          consider F be sequence of ( HFuncs NAT ) such that

           A5: ( primrec (f1,f2,i,pkn)) = (F . (pkn /. i)) and

           A6: i in ( dom pkn) & ( Del (pkn,i)) in ( dom f1) implies (F . 0 ) = ((pkn +* (i, 0 )) .--> (f1 . ( Del (pkn,i)))) and

           A7: not i in ( dom pkn) or not ( Del (pkn,i)) in ( dom f1) implies (F . 0 ) = {} and

           A8: for M be Nat holds Q[M, (F . M) qua Element of ( HFuncs NAT ), (F . (M + 1)) qua Element of ( HFuncs NAT ), pkn, i, f2] by Def10;

          ( dom p) = ( dom pkn1) by FUNCT_7: 30;



          then

           A9: (pkn1 /. i) = (pkn1 . i) by A1, PARTFUN1:def 6

          .= (m + 1) by A1, FUNCT_7: 31;

          consider F1 be sequence of ( HFuncs NAT ) such that

           A10: ( primrec (f1,f2,i,pkn1)) = (F1 . (pkn1 /. i)) and

           A11: i in ( dom pkn1) & ( Del (pkn1,i)) in ( dom f1) implies (F1 . 0 ) = ((pkn1 +* (i, 0 )) .--> (f1 . ( Del (pkn1,i)))) and

           A12: not i in ( dom pkn1) or not ( Del (pkn1,i)) in ( dom f1) implies (F1 . 0 ) = {} and

           A13: for M be Nat holds Q[M, (F1 . M) qua Element of ( HFuncs NAT ), (F1 . (M + 1)) qua Element of ( HFuncs NAT ), pkn1, i, f2] by Def10;

          F1 = F by A6, A7, A8, A11, A12, A13, Lm2;

          then

           A14: (G . (p +* (i,(k + (n + 1))))) = (F . (m + 1)) by A2, A10, A9;

          ( dom p) = ( dom pkn) by FUNCT_7: 30;



          then (pkn /. i) = (pkn . i) by A1, PARTFUN1:def 6

          .= m by A1, FUNCT_7: 31;

          then

           A15: (G . (p +* (i,(k + n)))) = (F . m) by A2, A5;

          per cases ;

            suppose i in ( dom pkn) & (pkn +* (i,m)) in ( dom (F . m)) & ((pkn +* (i,m)) ^ <*((F . m) . (pkn +* (i,m)))*>) in ( dom f2);

            then (F . (m + 1)) = ((F . m) +* ((pkn +* (i,(m + 1))) .--> (f2 . ((pkn +* (i,m)) ^ <*((F . m) . (pkn +* (i,m)))*>)))) by A8;

            then ( dom (F . (m + 1))) = (( dom (F . m)) \/ ( dom ( {(pkn +* (i,(m + 1)))} --> (f2 . ((pkn +* (i,m)) ^ <*((F . m) . (pkn +* (i,m)))*>))))) by FUNCT_4:def 1;

            then ( dom (F . m)) c= ( dom (F . (m + 1))) by XBOOLE_1: 7;

            hence p[(n + 1)] by A4, A14, A15, XBOOLE_1: 1;

          end;

            suppose not i in ( dom pkn) or not (pkn +* (i,m)) in ( dom (F . m)) or not ((pkn +* (i,m)) ^ <*((F . m) . (pkn +* (i,m)))*>) in ( dom f2);

            hence p[(n + 1)] by A4, A8, A14, A15;

          end;

        end;



         A16: p[ 0 ];

        thus for n be Nat holds p[n] from NAT_1:sch 2( A16, A3);

      end;

    end;

     Lm5:

    now

      let f1,f2 be non empty homogeneous to-naturals( NAT * ) -defined Function;

      let p be Element of ((( arity f1) + 1) -tuples_on NAT );

      let i,m be Element of NAT such that

       A1: i in ( dom p);

      let G be Function of ((( arity f1) + 1) -tuples_on NAT ), ( HFuncs NAT ) such that

       A2: for p be Element of ((( arity f1) + 1) -tuples_on NAT ) holds (G . p) = ( primrec (f1,f2,i,p));

      thus for k,n be Nat st not (p +* (i,k)) in ( dom (G . (p +* (i,k)))) holds not (p +* (i,k)) in ( dom (G . (p +* (i,(k + n)))))

      proof

        let k be Nat;

        set pk = (p +* (i,k));

        defpred p[ Nat] means not pk in ( dom (G . pk)) implies not pk in ( dom (G . (p +* (i,(k + $1)))));



         A3: for n be Nat st p[n] holds p[(n + 1)]

        proof

          let n be Nat such that

           A4: p[n] and

           A5: not pk in ( dom (G . pk));

          reconsider m = (k + n) as Element of NAT by ORDINAL1:def 12;

          set pkn = (p +* (i,m));

          consider F be sequence of ( HFuncs NAT ) such that

           A6: ( primrec (f1,f2,i,pkn)) = (F . (pkn /. i)) and

           A7: i in ( dom pkn) & ( Del (pkn,i)) in ( dom f1) implies (F . 0 ) = ((pkn +* (i, 0 )) .--> (f1 . ( Del (pkn,i)))) and

           A8: not i in ( dom pkn) or not ( Del (pkn,i)) in ( dom f1) implies (F . 0 ) = {} and

           A9: for M be Nat holds Q[M, (F . M) qua Element of ( HFuncs NAT ), (F . (M + 1)) qua Element of ( HFuncs NAT ), pkn, i, f2] by Def10;



           A10: ( dom p) = ( dom pkn) by FUNCT_7: 30;



          then (pkn /. i) = (pkn . i) by A1, PARTFUN1:def 6

          .= m by A1, FUNCT_7: 31;

          then

           A11: not pk in ( dom (F . m)) by A2, A4, A5, A6;

          set pkn1 = (p +* (i,((k + n) + 1)));

          consider F1 be sequence of ( HFuncs NAT ) such that

           A12: ( primrec (f1,f2,i,pkn1)) = (F1 . (pkn1 /. i)) and

           A13: i in ( dom pkn1) & ( Del (pkn1,i)) in ( dom f1) implies (F1 . 0 ) = ((pkn1 +* (i, 0 )) .--> (f1 . ( Del (pkn1,i)))) and

           A14: not i in ( dom pkn1) or not ( Del (pkn1,i)) in ( dom f1) implies (F1 . 0 ) = {} and

           A15: for M be Nat holds Q[M, (F1 . M) qua Element of ( HFuncs NAT ), (F1 . (M + 1)) qua Element of ( HFuncs NAT ), pkn1, i, f2] by Def10;

          ( dom p) = ( dom pkn1) by FUNCT_7: 30;



          then

           A16: (pkn1 /. i) = (pkn1 . i) by A1, PARTFUN1:def 6

          .= (m + 1) by A1, FUNCT_7: 31;

          F1 = F by A7, A8, A9, A13, A14, A15, Lm2;

          then

           A17: (G . (p +* (i,(k + (n + 1))))) = (F . (m + 1)) by A2, A12, A16;

          per cases ;

            suppose i in ( dom pkn) & (pkn +* (i,m)) in ( dom (F . m)) & ((pkn +* (i,m)) ^ <*((F . m) . (pkn +* (i,m)))*>) in ( dom f2);

            then (F . (m + 1)) = ((F . m) +* ((pkn +* (i,(m + 1))) .--> (f2 . ((pkn +* (i,m)) ^ <*((F . m) . (pkn +* (i,m)))*>)))) by A9;

            then ( dom (F . (m + 1))) = (( dom (F . m)) \/ ( dom ( {(pkn +* (i,(m + 1)))} --> (f2 . ((pkn +* (i,m)) ^ <*((F . m) . (pkn +* (i,m)))*>))))) by FUNCT_4:def 1;

            then

             A18: ( dom (F . (m + 1))) = (( dom (F . m)) \/ {(pkn +* (i,(m + 1)))});

            k <= (k + n) by NAT_1: 11;

            then

             A19: k <> (m + 1) by NAT_1: 13;



             A20: (pk . i) = k by A1, FUNCT_7: 31;

            ((pkn +* (i,(m + 1))) . i) = (m + 1) by A1, A10, FUNCT_7: 31;

            then not pk in {(pkn +* (i,(m + 1)))} by A19, A20, TARSKI:def 1;

            hence thesis by A11, A17, A18, XBOOLE_0:def 3;

          end;

            suppose not i in ( dom pkn) or not (pkn +* (i,m)) in ( dom (F . m)) or not ((pkn +* (i,m)) ^ <*((F . m) . (pkn +* (i,m)))*>) in ( dom f2);

            hence thesis by A9, A11, A17;

          end;

        end;



         A21: p[ 0 ];

        thus for n be Nat holds p[n] from NAT_1:sch 2( A21, A3);

      end;

    end;



     Lm6: for i,m be Nat holds i in ( dom p) implies ((p +* (i, 0 )) in ( dom ( primrec (f1,f2,i))) iff ( Del (p,i)) in ( dom f1)) & ((p +* (i, 0 )) in ( dom ( primrec (f1,f2,i))) implies (( primrec (f1,f2,i)) . (p +* (i, 0 ))) = (f1 . ( Del (p,i)))) & ((p +* (i,(m + 1))) in ( dom ( primrec (f1,f2,i))) iff (p +* (i,m)) in ( dom ( primrec (f1,f2,i))) & ((p +* (i,m)) ^ <*(( primrec (f1,f2,i)) . (p +* (i,m)))*>) in ( dom f2)) & ((p +* (i,(m + 1))) in ( dom ( primrec (f1,f2,i))) implies (( primrec (f1,f2,i)) . (p +* (i,(m + 1)))) = (f2 . ((p +* (i,m)) ^ <*(( primrec (f1,f2,i)) . (p +* (i,m)))*>)))

    proof

      let i,m be Nat;

      set p0 = (p +* (i, 0 ));

      consider G be Function of ((( arity f1) + 1) -tuples_on NAT ), ( HFuncs NAT ) such that

       A1: ( primrec (f1,f2,i)) = ( Union G) and

       A2: for p be Element of ((( arity f1) + 1) -tuples_on NAT ) holds (G . p) = ( primrec (f1,f2,i,p)) by Def11;

      reconsider rngG = ( rng G) as functional compatible set by A1, Th10;

      assume

       A3: i in ( dom p);

       A4:

      now

        let k be Element of NAT such that

         A5: (p +* (i,k)) in ( dom ( primrec (f1,f2,i))) and

         A6: not (p +* (i,k)) in ( dom (G . (p +* (i,k))));

        ( union rngG) <> {} by A1, A5;

        then

        reconsider rngG = ( rng G) as non empty functional compatible set;

        set pk = (p +* (i,k));

        ( dom ( union rngG)) = ( union the set of all ( dom f) where f be Element of rngG) by Th11;

        then

        consider X be set such that

         A7: pk in X and

         A8: X in the set of all ( dom f) where f be Element of rngG by A1, A5, TARSKI:def 4;

        consider f be Element of rngG such that

         A9: X = ( dom f) by A8;

        consider pp be object such that

         A10: pp in ( dom G) and

         A11: f = (G . pp) by FUNCT_1:def 3;

        reconsider pp as Element of ((( arity f1) + 1) -tuples_on NAT ) by A10;

        (G . pp) = ( primrec (f1,f2,i,pp)) by A2;

        then

         A12: ex m be Element of NAT st pk = (pp +* (i,m)) by A7, A9, A11, Th48;

        set ppi = (pp . i);



         A13: (p +* (i,ppi)) = (pk +* (i,ppi)) by FUNCT_7: 34

        .= (pp +* (i,ppi)) by A12, FUNCT_7: 34

        .= pp by FUNCT_7: 35;

        per cases by XXREAL_0: 1;

          suppose k = ppi;

          hence contradiction by A6, A7, A9, A11, A13;

        end;

          suppose ppi < k;

          then

          consider m be Nat such that

           A14: k = (ppi + m) by NAT_1: 10;

          reconsider m as Element of NAT by ORDINAL1:def 12;

          k = (ppi + m) by A14;

          then ( dom (G . pp)) c= ( dom (G . pk)) by A3, A2, A13, Lm4;

          hence contradiction by A6, A7, A9, A11;

        end;

          suppose ppi > k;

          then

          consider m be Nat such that

           A15: ppi = (k + m) by NAT_1: 10;

          reconsider m as Element of NAT by ORDINAL1:def 12;

          ppi = (k + m) by A15;

          hence contradiction by A3, A2, A6, A7, A9, A11, A13, Lm5;

        end;

      end;



       A16: ( dom p) = ( dom p0) by FUNCT_7: 30;

       A17:

      now



         A18: p0 in {p0} by TARSKI:def 1;



         A19: (p0 /. i) = (p0 . i) by A3, A16, PARTFUN1:def 6

        .= 0 by A3, FUNCT_7: 31;

        consider F be sequence of ( HFuncs NAT ) such that

         A20: ( primrec (f1,f2,i,p0)) = (F . (p0 /. i)) and

         A21: i in ( dom p0) & ( Del (p0,i)) in ( dom f1) implies (F . 0 ) = ((p0 +* (i, 0 )) .--> (f1 . ( Del (p0,i)))) and

         A22: not i in ( dom p0) or not ( Del (p0,i)) in ( dom f1) implies (F . 0 ) = {} and for m be Nat holds Q[m, (F . m) qua Element of ( HFuncs NAT ), (F . (m + 1)) qua Element of ( HFuncs NAT ), p0, i, f2] by Def10;



         A23: (G . p0) = ( primrec (f1,f2,i,p0)) by A2;

        thus p0 in ( dom (G . p0)) iff ( Del (p,i)) in ( dom f1)

        proof

          thus p0 in ( dom (G . p0)) implies ( Del (p,i)) in ( dom f1) by A2, A20, A22, A19, Th3;

          assume ( Del (p,i)) in ( dom f1);



          then ( dom (F . 0 )) = {(p0 +* (i, 0 ))} by A3, A21, Th3, FUNCT_7: 30

          .= {p0} by FUNCT_7: 34;

          hence thesis by A23, A20, A19, TARSKI:def 1;

        end;

        assume p0 in ( dom (G . p0));

        then (F . 0 ) = ( {p0} --> (f1 . ( Del (p0,i)))) by A2, A20, A21, A22, A19, FUNCT_7: 34;

        then (F . 0 ) = ( {p0} --> (f1 . ( Del (p,i)))) by Th3;

        hence ((G . p0) . p0) = (f1 . ( Del (p,i))) by A23, A20, A19, A18, FUNCOP_1: 7;

      end;

      reconsider mm = m as Element of NAT by ORDINAL1:def 12;

      set pm1 = (p +* (i,(mm + 1))), pm = (p +* (i,mm)), pc = <*((G . pm1) . (pm1 +* (i,m)))*>;



       A24: ( dom G) = ((( arity f1) + 1) -tuples_on NAT ) by FUNCT_2:def 1;

      then

       A25: (G . pm1) in ( rng G) by FUNCT_1:def 3;

      reconsider rngG as non empty functional compatible set;



       A26: (G . p0) in ( rng G) by A24, FUNCT_1:def 3;

      thus (p +* (i, 0 )) in ( dom ( primrec (f1,f2,i))) iff ( Del (p,i)) in ( dom f1)

      proof

        thus (p +* (i, 0 )) in ( dom ( primrec (f1,f2,i))) implies ( Del (p,i)) in ( dom f1) by A4, A17;

        assume

         A27: ( Del (p,i)) in ( dom f1);

        ( dom (G . p0)) in the set of all ( dom f) where f be Element of rngG by A26;

        then p0 in ( union the set of all ( dom f) where f be Element of rngG) by A17, A27, TARSKI:def 4;

        hence thesis by A1, Th11;

      end;

      hereby

        assume

         A28: (p +* (i, 0 )) in ( dom ( primrec (f1,f2,i)));

        then p0 in ( dom (G . p0)) by A4;

        then (( union rngG) . p0) = ((G . p0) . p0) by A26, Th12;

        hence (( primrec (f1,f2,i)) . (p +* (i, 0 ))) = (f1 . ( Del (p,i))) by A1, A4, A17, A28;

      end;



       A29: ( dom p) = ( dom pm1) by FUNCT_7: 30;



       A30: (pm1 +* (i,(m + 1))) = pm1 by FUNCT_7: 34;



       A31: (pm1 +* (i,m)) = pm by FUNCT_7: 34;



       A32: ( dom p) = ( dom pm) by FUNCT_7: 30;

       A33:

      now



         A34: (pm /. i) = (pm . i) by A3, A32, PARTFUN1:def 6

        .= m by A3, FUNCT_7: 31;

        consider F be sequence of ( HFuncs NAT ) such that

         A35: ( primrec (f1,f2,i,pm)) = (F . (pm /. i)) and

         A36: i in ( dom pm) & ( Del (pm,i)) in ( dom f1) implies (F . 0 ) = ((pm +* (i, 0 )) .--> (f1 . ( Del (pm,i)))) and

         A37: not i in ( dom pm) or not ( Del (pm,i)) in ( dom f1) implies (F . 0 ) = {} and

         A38: for M be Nat holds Q[M, (F . M) qua Element of ( HFuncs NAT ), (F . (M + 1)) qua Element of ( HFuncs NAT ), pm, i, f2] by Def10;



         A39: (G . pm1) = ( primrec (f1,f2,i,pm1)) by A2;

        consider F1 be sequence of ( HFuncs NAT ) such that

         A40: ( primrec (f1,f2,i,pm1)) = (F1 . (pm1 /. i)) and

         A41: i in ( dom pm1) & ( Del (pm1,i)) in ( dom f1) implies (F1 . 0 ) = ((pm1 +* (i, 0 )) .--> (f1 . ( Del (pm1,i)))) and

         A42: not i in ( dom pm1) or not ( Del (pm1,i)) in ( dom f1) implies (F1 . 0 ) = {} and

         A43: for M be Nat holds Q[M, (F1 . M) qua Element of ( HFuncs NAT ), (F1 . (M + 1)) qua Element of ( HFuncs NAT ), pm1, i, f2] by Def10;



         A44: ((F1 . (m + 1)) . pm) = ((F1 . m) . pm) by A3, A41, A42, A43, Lm3;



         A45: pm1 in {pm1} by TARSKI:def 1;

        then

         A46: pm1 in ( dom ( {pm1} --> (f2 . (pm ^ <*((F1 . m) . pm)*>))));



         A47: (G . pm) = ( primrec (f1,f2,i,pm)) by A2;



         A48: (pm1 /. i) = (pm1 . i) by A3, A29, PARTFUN1:def 6

        .= (m + 1) by A3, FUNCT_7: 31;



         A49: (F1 . m) = (F . m) by A41, A42, A43, A36, A37, A38, Lm2;



         A50: not pm1 in ( dom (F1 . m)) by A3, A41, A42, A43, Lm3;

        thus

         A51: pm1 in ( dom (G . pm1)) iff pm in ( dom (G . pm)) & (pm ^ pc) in ( dom f2)

        proof

          hereby

            assume

             A52: pm1 in ( dom (G . pm1));

            then

             A53: pm1 in ( dom (F1 . (m + 1))) by A2, A40, A48;

            assume

             A54: not (pm in ( dom (G . pm)) & (pm ^ pc) in ( dom f2));

            per cases by A54;

              suppose not pm in ( dom (G . pm));

              then not pm in ( dom (F1 . m)) by A2, A35, A34, A49;

              hence contradiction by A31, A43, A50, A53;

            end;

              suppose not (pm ^ pc) in ( dom f2);

              hence contradiction by A31, A39, A40, A43, A48, A44, A50, A52;

            end;

          end;

          assume that

           A55: pm in ( dom (G . pm)) and

           A56: (pm ^ pc) in ( dom f2);

          pm1 in {pm1} by TARSKI:def 1;

          then pm1 in ( dom ( {pm1} --> (f2 . (pm ^ <*((F1 . m) . pm)*>))));

          then

           A57: pm1 in (( dom (F1 . m)) \/ ( dom ( {pm1} --> (f2 . (pm ^ <*((F1 . m) . pm)*>))))) by XBOOLE_0:def 3;

          (F1 . (m + 1)) = ((F1 . m) +* (pm1 .--> (f2 . (pm ^ <*((F1 . m) . pm)*>)))) by A3, A29, A31, A30, A39, A47, A40, A43, A35, A48, A34, A49, A44, A55, A56;

          hence thesis by A39, A40, A48, A57, FUNCT_4:def 1;

        end;

        assume

         A58: pm1 in ( dom (G . pm1));

        then (pm ^ <*((F1 . m) . pm)*>) in ( dom f2) by A31, A39, A40, A43, A48, A51;

        then (F1 . (m + 1)) = ((F1 . m) +* (pm1 .--> (f2 . (pm ^ <*((F1 . m) . pm)*>)))) by A3, A29, A31, A30, A47, A43, A35, A34, A49, A51, A58;



        hence ((G . pm1) . pm1) = (( {pm1} --> (f2 . (pm ^ <*((F1 . m) . pm)*>))) . pm1) by A39, A40, A48, A46, FUNCT_4: 13

        .= (f2 . (pm ^ pc)) by A31, A39, A40, A48, A44, A45, FUNCOP_1: 7;

      end;

      thus (p +* (i,(m + 1))) in ( dom ( primrec (f1,f2,i))) iff (p +* (i,m)) in ( dom ( primrec (f1,f2,i))) & ((p +* (i,m)) ^ <*(( primrec (f1,f2,i)) . (p +* (i,m)))*>) in ( dom f2)

      proof

        hereby

          assume

           A59: (p +* (i,(m + 1))) in ( dom ( primrec (f1,f2,i)));

          (G . pm) in ( rng G) by A24, FUNCT_1:def 3;

          then ( dom (G . pm)) in the set of all ( dom f) where f be Element of rngG;

          then pm in ( union the set of all ( dom f) where f be Element of rngG) by A4, A33, A59, TARSKI:def 4;

          hence (p +* (i,m)) in ( dom ( primrec (f1,f2,i))) by A1, Th11;



           A60: (G . pm1) in ( rng G) by A24, FUNCT_1:def 3;

          ( dom (G . pm)) c= ( dom (G . pm1)) by A3, A2, Lm4;

          then (( union rngG) . pm) = ((G . pm1) . pm) by A4, A33, A59, A60, Th12;

          hence ((p +* (i,m)) ^ <*(( primrec (f1,f2,i)) . (p +* (i,m)))*>) in ( dom f2) by A1, A4, A33, A59, FUNCT_7: 34;

        end;

        assume that

         A61: (p +* (i,m)) in ( dom ( primrec (f1,f2,i))) and

         A62: ((p +* (i,m)) ^ <*(( primrec (f1,f2,i)) . (p +* (i,m)))*>) in ( dom f2);



         A63: (G . pm1) in ( rng G) by A24, FUNCT_1:def 3;

        (G . pm1) in ( rng G) by A24, FUNCT_1:def 3;

        then

         A64: ( dom (G . pm1)) in the set of all ( dom f) where f be Element of rngG;



         A65: ( dom (G . pm)) c= ( dom (G . pm1)) by A3, A2, Lm4;

        pm in ( dom (G . pm)) by A4, A61;

        then pm1 in ( union the set of all ( dom f) where f be Element of rngG) by A1, A31, A33, A62, A64, A63, A65, Th12, TARSKI:def 4;

        hence thesis by A1, Th11;

      end;

      assume

       A66: (p +* (i,(m + 1))) in ( dom ( primrec (f1,f2,i)));



       A67: ( dom (G . pm)) c= ( dom (G . pm1)) by A3, A2, Lm4;

      then

       A68: (( union rngG) . pm1) = ((G . pm1) . pm1) by A4, A66, A25, Th12;

      (( union rngG) . pm) = ((G . pm1) . pm) by A4, A33, A66, A25, A67, Th12;

      hence thesis by A1, A4, A33, A66, A68, FUNCT_7: 34;

    end;

    theorem :: COMPUT_1:58

    i in ( dom p) implies ((p +* (i, 0 )) in ( dom ( primrec (f1,f2,i))) iff ( Del (p,i)) in ( dom f1)) by Lm6;

    theorem :: COMPUT_1:59

    i in ( dom p) & (p +* (i, 0 )) in ( dom ( primrec (f1,f2,i))) implies (( primrec (f1,f2,i)) . (p +* (i, 0 ))) = (f1 . ( Del (p,i))) by Lm6;

    theorem :: COMPUT_1:60



     Th59: i in ( dom p) & f1 is len-total implies (( primrec (f1,f2,i)) . (p +* (i, 0 ))) = (f1 . ( Del (p,i)))

    proof

      assume that

       A1: i in ( dom p) and

       A2: f1 is len-total;



       A3: ( Del (p,i)) is FinSequence of NAT by FINSEQ_3: 105;

      ( len p) = (( arity f1) + 1) by CARD_1:def 7;

      then ( len ( Del (p,i))) = ( arity f1) by A1, FINSEQ_3: 109;

      then

       A4: ( Del (p,i)) is Element of (( arity f1) -tuples_on NAT ) by A3, FINSEQ_2: 92;

      ( dom f1) = (( arity f1) -tuples_on NAT ) by A2, Th22;

      then (p +* (i, 0 )) in ( dom ( primrec (f1,f2,i))) by A1, A4, Lm6;

      hence thesis by A1, Lm6;

    end;

    theorem :: COMPUT_1:61

    i in ( dom p) implies ((p +* (i,(m + 1))) in ( dom ( primrec (f1,f2,i))) iff (p +* (i,m)) in ( dom ( primrec (f1,f2,i))) & ((p +* (i,m)) ^ <*(( primrec (f1,f2,i)) . (p +* (i,m)))*>) in ( dom f2)) by Lm6;

    theorem :: COMPUT_1:62

    i in ( dom p) & (p +* (i,(m + 1))) in ( dom ( primrec (f1,f2,i))) implies (( primrec (f1,f2,i)) . (p +* (i,(m + 1)))) = (f2 . ((p +* (i,m)) ^ <*(( primrec (f1,f2,i)) . (p +* (i,m)))*>)) by Lm6;

    theorem :: COMPUT_1:63



     Th62: f1 is len-total & f2 is len-total & (( arity f1) + 2) = ( arity f2) & 1 <= i & i <= (1 + ( arity f1)) implies (( primrec (f1,f2,i)) . (p +* (i,(m + 1)))) = (f2 . ((p +* (i,m)) ^ <*(( primrec (f1,f2,i)) . (p +* (i,m)))*>))

    proof

      assume that

       A1: f1 is len-total and

       A2: f2 is len-total and

       A3: (( arity f1) + 2) = ( arity f2) and

       A4: 1 <= i and

       A5: i <= (1 + ( arity f1));

      ( len p) = (( arity f1) + 1) by CARD_1:def 7;

      then

       A6: i in ( dom p) by A4, A5, FINSEQ_3: 25;

      (p +* (i,(m + 1))) in ((( arity f1) + 1) -tuples_on NAT );

      then (p +* (i,(m + 1))) in ( dom ( primrec (f1,f2,i))) by A1, A2, A3, A4, A5, Th56;

      hence thesis by A6, Lm6;

    end;

    theorem :: COMPUT_1:64



     Th63: (( arity f1) + 2) = ( arity f2) & 1 <= i & i <= (( arity f1) + 1) implies ( primrec (f1,f2,i)) is_primitive-recursively_expressed_by (f1,f2,i)

    proof

      assume that

       A1: (( arity f1) + 2) = ( arity f2) and

       A2: 1 <= i and

       A3: i <= (( arity f1) + 1);

      take n = (( arity f1) + 1);

      set g = ( primrec (f1,f2,i));

      thus ( dom g) c= (n -tuples_on NAT ) by Th55;

      thus i >= 1 & i <= n by A2, A3;

      thus (( arity f1) + 1) = n;

      thus (n + 1) = ( arity f2) by A1;

      let p be FinSequence of NAT ;

      assume

       A4: ( len p) = n;

      then

       A5: i in ( dom p) by A2, A3, FINSEQ_3: 25;



       A6: p is Element of (n -tuples_on NAT ) by A4, FINSEQ_2: 92;

      hence (p +* (i, 0 )) in ( dom g) iff ( Del (p,i)) in ( dom f1) by A5, Lm6;

      thus (p +* (i, 0 )) in ( dom g) implies (g . (p +* (i, 0 ))) = (f1 . ( Del (p,i))) by A6, A5, Lm6;

      let m be Nat;

      thus (p +* (i,(m + 1))) in ( dom g) iff (p +* (i,m)) in ( dom g) & ((p +* (i,m)) ^ <*(g . (p +* (i,m)))*>) in ( dom f2) by A6, A5, Lm6;

      thus (p +* (i,(m + 1))) in ( dom g) implies (g . (p +* (i,(m + 1)))) = (f2 . ((p +* (i,m)) ^ <*(g . (p +* (i,m)))*>)) by A6, A5, Lm6;

    end;

    theorem :: COMPUT_1:65

    1 <= i & i <= (( arity f1) + 1) implies for g be Element of ( HFuncs NAT ) st g is_primitive-recursively_expressed_by (f1,f2,i) holds g = ( primrec (f1,f2,i))

    proof

      assume that

       A1: i >= 1 and

       A2: i <= (( arity f1) + 1);

      let g be Element of ( HFuncs NAT );

      set n = (( arity f1) + 1), h = ( primrec (f1,f2,i));

      given n9 be Element of NAT such that

       A3: ( dom g) c= (n9 -tuples_on NAT ) and i >= 1 and i <= n9 and

       A4: (( arity f1) + 1) = n9 and (n9 + 1) = ( arity f2) and

       A5: for p be FinSequence of NAT st ( len p) = n9 holds ((p +* (i, 0 )) in ( dom g) iff ( Del (p,i)) in ( dom f1)) & ((p +* (i, 0 )) in ( dom g) implies (g . (p +* (i, 0 ))) = (f1 . ( Del (p,i)))) & for n be Nat holds ((p +* (i,(n + 1))) in ( dom g) iff (p +* (i,n)) in ( dom g) & ((p +* (i,n)) ^ <*(g . (p +* (i,n)))*>) in ( dom f2)) & ((p +* (i,(n + 1))) in ( dom g) implies (g . (p +* (i,(n + 1)))) = (f2 . ((p +* (i,n)) ^ <*(g . (p +* (i,n)))*>)));

       A6:

      now

        let p be Element of (n -tuples_on NAT );

        defpred p[ Nat] means ((p +* (i,$1)) in ( dom g) iff (p +* (i,$1)) in ( dom h)) & ((p +* (i,$1)) in ( dom g) implies (g . (p +* (i,$1))) = (h . (p +* (i,$1))));

        set k = (p /. i);



         A7: p = (p +* (i,k)) by FUNCT_7: 38;



         A8: ( len p) = n by CARD_1:def 7;

        then

         A9: i in ( dom p) by A1, A2, FINSEQ_3: 25;



         A10: for m be Nat st p[m] holds p[(m + 1)]

        proof

          let m be Nat such that

           A11: (p +* (i,m)) in ( dom g) iff (p +* (i,m)) in ( dom h) and

           A12: (p +* (i,m)) in ( dom g) implies (g . (p +* (i,m))) = (h . (p +* (i,m)));

          (p +* (i,(m + 1))) in ( dom g) iff (p +* (i,m)) in ( dom g) & ((p +* (i,m)) ^ <*(g . (p +* (i,m)))*>) in ( dom f2) by A4, A5, A8;

          hence (p +* (i,(m + 1))) in ( dom g) iff (p +* (i,(m + 1))) in ( dom h) by A9, A11, A12, Lm6;



           A13: (p +* (i,(m + 1))) in ( dom h) iff (p +* (i,m)) in ( dom h) & ((p +* (i,m)) ^ <*(h . (p +* (i,m)))*>) in ( dom f2) by A9, Lm6;

          assume

           A14: (p +* (i,(m + 1))) in ( dom g);

          then (g . (p +* (i,(m + 1)))) = (f2 . ((p +* (i,m)) ^ <*(g . (p +* (i,m)))*>)) by A4, A5, A8;

          hence thesis by A4, A5, A8, A9, A11, A12, A13, A14, Lm6;

        end;



         A15: (p +* (i, 0 )) in ( dom h) iff ( Del (p,i)) in ( dom f1) by A9, Lm6;

        then (p +* (i, 0 )) in ( dom g) implies (g . (p +* (i, 0 ))) = (f1 . ( Del (p,i))) & (h . (p +* (i, 0 ))) = (f1 . ( Del (p,i))) by A4, A5, A8, A9, Lm6;

        then

         A16: p[ 0 ] by A4, A5, A8, A15;

        for m be Nat holds p[m] from NAT_1:sch 2( A16, A10);

        hence (p in ( dom g) iff p in ( dom h)) & (p in ( dom g) implies (g . p) = (h . p)) by A7;

      end;



       A17: ( dom h) c= (n -tuples_on NAT ) by Th55;

      then

       A18: ( dom g) = ( dom h) by A3, A4, A6;

      for x be object st x in ( dom h) holds (g . x) = (h . x) by A17, A6;

      hence thesis by A18;

    end;

    begin

    definition

      let X be set;

      :: COMPUT_1:def12

      attr X is composition_closed means for f be Element of ( HFuncs NAT ), F be with_the_same_arity FinSequence of ( HFuncs NAT ) st f in X & ( arity f) = ( len F) & ( rng F) c= X holds (f * <:F:>) in X;

      :: COMPUT_1:def13

      attr X is primitive-recursion_closed means for g,f1,f2 be Element of ( HFuncs NAT ), i be Element of NAT st g is_primitive-recursively_expressed_by (f1,f2,i) & f1 in X & f2 in X holds g in X;

    end

    definition

      let X be set;

      :: COMPUT_1:def14

      attr X is primitive-recursively_closed means

      : Def14: ( 0 const 0 ) in X & (1 succ 1) in X & (for n,i be Element of NAT st 1 <= i & i <= n holds (n proj i) in X) & X is composition_closed & X is primitive-recursion_closed;

    end

    theorem :: COMPUT_1:66



     Th65: ( HFuncs NAT ) is primitive-recursively_closed

    proof

      set X = ( HFuncs NAT );

      thus ( 0 const 0 ) in X & (1 succ 1) in X & for n,i be Element of NAT st 1 <= i & i <= n holds (n proj i) in X by Th30, Th32, Th34;

      thus for f be Element of ( HFuncs NAT ) holds for F be with_the_same_arity FinSequence of ( HFuncs NAT ) st f in X & ( arity f) = ( len F) & ( rng F) c= X holds (f * <:F:>) in X by Th41;

      let g be Element of ( HFuncs NAT );

      thus thesis;

    end;

    registration

      cluster primitive-recursively_closed non empty for Subset of ( HFuncs NAT );

      existence

      proof

        ( HFuncs NAT ) c= ( HFuncs NAT );

        then

        reconsider X = ( HFuncs NAT ) as non empty Subset of ( HFuncs NAT );

        take X;

        thus thesis by Th65;

      end;

    end

    reserve P for primitive-recursively_closed non empty Subset of ( HFuncs NAT );



     Lm7: for X be non empty set, n,i be Element of NAT st 1 <= i & i <= n holds for x be Element of X holds for p be Element of (n -tuples_on X) holds (p +* (i,x)) in (n -tuples_on X);

    theorem :: COMPUT_1:67



     Th66: for g be Element of ( HFuncs NAT ) st e1 = {} & g is_primitive-recursively_expressed_by (e1,e2,i) holds g = {}

    proof

      set f1 = e1, f2 = e2;

      let g be Element of ( HFuncs NAT );

      assume

       A1: f1 = {} ;

      assume g is_primitive-recursively_expressed_by (f1,f2,i);

      then

      consider n be Element of NAT such that

       A2: ( dom g) c= (n -tuples_on NAT ) and i >= 1 and i <= n and (( arity f1) + 1) = n and (n + 1) = ( arity f2) and

       A3: for p be FinSequence of NAT st ( len p) = n holds ((p +* (i, 0 )) in ( dom g) iff ( Del (p,i)) in ( dom f1)) & ((p +* (i, 0 )) in ( dom g) implies (g . (p +* (i, 0 ))) = (f1 . ( Del (p,i)))) & for n be Nat holds ((p +* (i,(n + 1))) in ( dom g) iff (p +* (i,n)) in ( dom g) & ((p +* (i,n)) ^ <*(g . (p +* (i,n)))*>) in ( dom f2)) & ((p +* (i,(n + 1))) in ( dom g) implies (g . (p +* (i,(n + 1)))) = (f2 . ((p +* (i,n)) ^ <*(g . (p +* (i,n)))*>)));

       A4:

      now

        let y be Element of (n -tuples_on NAT );

        defpred p[ Nat] means not (y +* (i,$1)) in ( dom g);



         A5: ( len y) = n by CARD_1:def 7;

        then

         A6: for k be Nat st p[k] holds p[(k + 1)] by A3;



         A7: p[ 0 ] by A1, A3, A5;

        thus for k be Nat holds p[k] from NAT_1:sch 2( A7, A6);

      end;

      assume g <> {} ;

      then

      consider x be object such that

       A8: x in ( dom g) by XBOOLE_0:def 1;

      reconsider x as Element of (n -tuples_on NAT ) by A2, A8;

      set xi = (x . i);

      x = (x +* (i,xi)) by FUNCT_7: 35;

      hence contradiction by A4, A8;

    end;

    theorem :: COMPUT_1:68



     Th67: for g be Element of ( HFuncs NAT ), f1,f2 be quasi_total Element of ( HFuncs NAT ), i be Element of NAT st g is_primitive-recursively_expressed_by (f1,f2,i) holds g is quasi_total & (f1 is non empty implies g is non empty)

    proof

      let g be Element of ( HFuncs NAT ), f1,f2 be quasi_total Element of ( HFuncs NAT ), i be Element of NAT ;

      assume

       A1: g is_primitive-recursively_expressed_by (f1,f2,i);

      then

      consider n be Element of NAT such that

       A2: ( dom g) c= (n -tuples_on NAT ) and

       A3: i >= 1 and

       A4: i <= n and

       A5: (( arity f1) + 1) = n and

       A6: (n + 1) = ( arity f2) and

       A7: for p be FinSequence of NAT st ( len p) = n holds ((p +* (i, 0 )) in ( dom g) iff ( Del (p,i)) in ( dom f1)) & ((p +* (i, 0 )) in ( dom g) implies (g . (p +* (i, 0 ))) = (f1 . ( Del (p,i)))) & for n be Nat holds ((p +* (i,(n + 1))) in ( dom g) iff (p +* (i,n)) in ( dom g) & ((p +* (i,n)) ^ <*(g . (p +* (i,n)))*>) in ( dom f2)) & ((p +* (i,(n + 1))) in ( dom g) implies (g . (p +* (i,(n + 1)))) = (f2 . ((p +* (i,n)) ^ <*(g . (p +* (i,n)))*>)));

      reconsider f29 = f2 as non empty quasi_total Element of ( HFuncs NAT ) by A6, Th17;

      per cases ;

        suppose f1 is empty;

        hence thesis by A1, Th66;

      end;

        suppose f1 is non empty;

        then

         A8: ( dom f1) = (( arity f1) -tuples_on NAT ) by Th21;



         A9: g is quasi_total

        proof

          let x,y be FinSequence of NAT such that

           A10: ( len x) = ( len y) and

           A11: x in ( dom g);

          defpred p[ Nat] means (y +* (i,$1)) in ( dom g);



           A12: ( len x) = n by A2, A11, CARD_1:def 7;

           A13:

          now

            let k be Nat such that

             A14: p[k];



             A15: ( dom f29) = (( arity f2) -tuples_on NAT ) by Th21;

            reconsider kk = k as Element of NAT by ORDINAL1:def 12;

            ( len ((y +* (i,k)) ^ <*(g . (y +* (i,k)))*>)) = (( len (y +* (i,k))) + ( len <*(g . (y +* (i,k)))*>)) by FINSEQ_1: 22

            .= (n + ( len <*(g . (y +* (i,k)))*>)) by A10, A12, FUNCT_7: 97

            .= (n + 1) by FINSEQ_1: 39;

            then ((y +* (i,kk)) ^ <*(g . (y +* (i,kk)))*>) is Element of ( dom f2) by A6, A15, FINSEQ_2: 92;

            then ((y +* (i,k)) ^ <*(g . (y +* (i,k)))*>) in ( dom f29);

            hence p[(k + 1)] by A7, A10, A12, A14;

          end;

          y is Element of (( len y) -tuples_on NAT ) by FINSEQ_2: 92;

          then ( Del (y,i)) in (( arity f1) -tuples_on NAT ) by A3, A4, A5, A10, A12, Th9;

          then

           A16: p[ 0 ] by A7, A8, A10, A12;

          for k be Nat holds p[k] from NAT_1:sch 2( A16, A13);

          then

           A17: (y +* (i,(y /. i))) in ( dom g);

          i in ( dom y) by A3, A4, A10, A12, FINSEQ_3: 25;

          then (y . i) = (y /. i) by PARTFUN1:def 6;

          hence y in ( dom g) by A17, FUNCT_7: 35;

        end;

        consider pp be object such that

         A18: pp in (n -tuples_on NAT ) by XBOOLE_0:def 1;

        pp is Element of (n -tuples_on NAT ) by A18;

        then

        reconsider p = pp as FinSequence of NAT ;



         A19: ( len p) = n by A18, CARD_1:def 7;

        ( Del (p,i)) in (( arity f1) -tuples_on NAT ) by A3, A4, A5, A18, Th9;

        hence thesis by A7, A19, A8, A9;

      end;

    end;

    theorem :: COMPUT_1:69



     Th68: (n const c) in P

    proof

      defpred p[ Nat] means ( 0 const $1) in P;

      defpred r[ Nat] means for c be Element of NAT holds ($1 const c) in P;



       A1: P is composition_closed by Def14;



       A2: for i be Nat st p[i] holds p[(i + 1)]

      proof

        reconsider 1succ1 = (1 succ 1) as quasi_total Element of ( HFuncs NAT ) by Th28;

        let i be Nat;



         A3: (1 succ 1) in P by Def14;



         A4: ( <*> NAT ) is Element of ( 0 -tuples_on NAT ) by FINSEQ_2: 131;

        then

         A5: (( 0 const i) . {} ) = i;

        reconsider 0consti = ( 0 const i) as Element of ( HFuncs NAT ) by Th27;

        set F = <*( 0 const i)*>;

         <*0consti*> is FinSequence of ( HFuncs NAT );

        then

        reconsider F as with_the_same_arity FinSequence of ( HFuncs NAT );

        assume ( 0 const i) in P;

        then

         A6: {( 0 const i)} c= P by ZFMISC_1: 31;



         A7: ( arity (1 succ 1)) = 1 by Th33

        .= ( len F) by FINSEQ_1: 39;



         A8: ( rng F) = {( 0 const i)} by FINSEQ_1: 39;

        reconsider i1 = i as Element of NAT by ORDINAL1:def 12;

        now

          let h be Element of ( HFuncs NAT );

          assume h in ( rng F);

          then h = ( 0 const i1) by A8, TARSKI:def 1;

          hence h is quasi_total by Th28;

        end;

        then

        reconsider g = (1succ1 * <:F:>) as quasi_total Element of ( HFuncs NAT ) by A7, Th45;



         A9: ( arity ( 0 const (i + 1))) = 0 by Th31;



         A10: (( 0 const (i + 1)) . {} ) = (i + 1) by A4;



         A11: ( dom (1 succ 1)) = (1 -tuples_on NAT ) by Def7;



         A12: ( arity ( 0 const i1)) = 0 by Th31;

        ( dom ( 0 const i1)) = ( 0 -tuples_on NAT );

        then

         A14: ( <:F:> . {} ) = <*i*> by A4, A5, FINSEQ_3: 141;

        reconsider ii = <*i1*> as Element of (1 -tuples_on NAT ) by FINSEQ_2: 131;



         A15: ( dom <: <*( 0 const i)*>:>) = ( dom ( 0 const i)) by FINSEQ_3: 141;

        then (g . {} ) = ((1 succ 1) . ( <:F:> . {} )) by A4, FUNCT_1: 13;



        then

         A16: (g . {} ) = ((ii /. 1) + 1) by A14, Def7

        .= (i1 + 1) by FINSEQ_4: 16;

        ( dom ( 0 const i)) = ( 0 -tuples_on NAT );

        then ( <: <*( 0 const i)*>:> . {} ) = ii by A4, A5, FINSEQ_3: 141;

        then

         A18: {} in ( dom g) by A4, A15, A11, FUNCT_1: 11;

        ( 0 const i) in ( rng F) by A8, TARSKI:def 1;

        then ( arity F) = 0 by A12, Def4;

        then ( arity g) = 0 by A18, Th43, RELAT_1: 38;

        then ( 0 const (i + 1)) = ((1 succ 1) * <: <*( 0 const i)*>:>) by A9, A10, A18, A16, Th47, RELAT_1: 38;

        hence thesis by A1, A6, A8, A3, A7;

      end;



       A19: P is primitive-recursion_closed by Def14;

       A20:

      now

        let n be Nat such that

         A21: r[n];

        thus r[(n + 1)]

        proof

          let i be Element of NAT ;

          reconsider nn = n as Element of NAT by ORDINAL1:def 12;

          set g = ((nn + 1) const i), f1 = (nn const i), j = (n + 1), f2 = ((nn + 2) proj (nn + 2));



           A23: (n + (1 + 1)) = (j + 1);

          then 1 <= (n + 2) by NAT_1: 11;

          then

           A24: f2 in P by Def14;



           A25: ( arity f2) = (n + 2) by Th36;



           A26: ( dom f2) = ((n + 2) -tuples_on NAT ) by Th35;



           A27: ( arity f1) = n by Th31;



           A29: ( arity g) = j by Th31;



           A30: g is_primitive-recursively_expressed_by (f1,f2,(n + 1))

          proof

            take m = ( arity g);

            thus ( dom g) c= (m -tuples_on NAT ) by Th20;

            thus j >= 1 & j <= m by Th31, NAT_1: 11;

            thus (( arity f1) + 1) = m & (m + 1) = ( arity f2) by A27, A25, A23, Th31;

            let p be FinSequence of NAT ;

            assume ( len p) = m;

            then

             A31: p is Element of (j -tuples_on NAT ) by A29, FINSEQ_2: 92;



             A32: j >= 1 by NAT_1: 11;

            hence (p +* (j, 0 )) in ( dom g) implies ( Del (p,j)) in ( dom f1) by A31, Th9;

            thus ( Del (p,j)) in ( dom f1) implies (p +* (j, 0 )) in ( dom g) by A31, A32, Lm7;

            (f1 . ( Del (p,j))) = i by A31, A32, Th9, FUNCOP_1: 7;

            hence (p +* (j, 0 )) in ( dom g) implies (g . (p +* (j, 0 ))) = (f1 . ( Del (p,j))) by FUNCOP_1: 7;

            let m be Nat;

            reconsider mm = m as Element of NAT by ORDINAL1:def 12;



             A33: (p +* (j,mm)) in (j -tuples_on NAT ) by A31, A32, Lm7;

            then

             A34: ((p +* (j,mm)) ^ <*i*>) is Tuple of (n + 2), NAT by A23;

            then

             A35: ((p +* (j,m)) ^ <*i*>) is Element of ((n + 2) -tuples_on NAT ) by FINSEQ_2: 131;

            hereby

              hereby

                assume (p +* (j,(m + 1))) in ( dom g);

                (p +* (j,mm)) in ( dom g) by A31, A32, Lm7;

                hence (p +* (j,m)) in ( dom g);

                (g . (p +* (j,mm))) = i by A31, A32, Lm7, FUNCOP_1: 7;

                hence ((p +* (j,m)) ^ <*(g . (p +* (j,m)))*>) in ( dom f2) by A26, A34, FINSEQ_2: 131;

              end;

              thus (p +* (j,m)) in ( dom g) & ((p +* (j,m)) ^ <*(g . (p +* (j,m)))*>) in ( dom f2) implies (p +* (j,(m + 1))) in ( dom g) by A31, A32, Lm7;

            end;

            assume (p +* (j,(m + 1))) in ( dom g);

            ( len (p +* (j,m))) = j by A33, CARD_1:def 7;

            then

             A36: (((p +* (j,m)) ^ <*i*>) . (j + 1)) = i by FINSEQ_1: 42;



            thus (g . (p +* (j,(m + 1)))) = i by A31, A32, Lm7, FUNCOP_1: 7

            .= (f2 . ((p +* (j,m)) ^ <*i*>)) by A36, A35, Th37

            .= (f2 . ((p +* (j,mm)) ^ <*(g . (p +* (j,mm)))*>)) by A31, A32, Lm7, FUNCOP_1: 7

            .= (f2 . ((p +* (j,m)) ^ <*(g . (p +* (j,m)))*>));

          end;



           A37: f1 in P by A21;

          ((n + 1) const i) is Element of ( HFuncs NAT ) by Th27;

          hence thesis by A19, A30, A37, A24;

        end;

      end;



       A38: p[ 0 ] by Def14;

      for i be Nat holds p[i] from NAT_1:sch 2( A38, A2);

      then

       A39: r[ 0 ];

      for n be Nat holds r[n] from NAT_1:sch 2( A39, A20);

      hence thesis;

    end;

    theorem :: COMPUT_1:70



     Th69: 1 <= i & i <= n implies (n succ i) in P

    proof



       A1: (1 succ 1) in P by Def14;



       A2: ( arity (1 succ 1)) = 1 by Th33

      .= ( len <*(n proj i)*>) by FINSEQ_1: 39;

      reconsider nproji = (n proj i) as Element of ( HFuncs NAT ) by Th27;

      assume that

       A3: 1 <= i and

       A4: i <= n;



       A5: <*nproji*> is with_the_same_arity FinSequence of ( HFuncs NAT );

      now

        ( rng (n proj i)) = NAT by A3, A4, Th35;

        then

         A6: ( rng <: <*(n proj i)*>:>) = (1 -tuples_on NAT ) by Th8;

        thus ( dom (n succ i)) = (n -tuples_on NAT ) by Def7;



         A7: ( dom (n proj i)) = (n -tuples_on NAT ) by Th35;

        then

         A8: ( dom <: <*(n proj i)*>:>) = (n -tuples_on NAT ) by FINSEQ_3: 141;

        ( dom (1 succ 1)) = (1 -tuples_on NAT ) by Def7;

        hence ( dom ((1 succ 1) * <: <*(n proj i)*>:>)) = (n -tuples_on NAT ) by A8, A6, RELAT_1: 27;

        let x be object;

        assume x in (n -tuples_on NAT );

        then

        reconsider x9 = x as Element of (n -tuples_on NAT );

        set xi = (x9 . i);

        ( len x9) = n by CARD_1:def 7;

        then

         A9: i in ( dom x9) by A3, A4, FINSEQ_3: 25;



         A10: ((n succ i) . x) = ((x9 /. i) + 1) by Def7

        .= (xi + 1) by A9, PARTFUN1:def 6;

        reconsider ii = <*xi*> as Element of (1 -tuples_on NAT ) by FINSEQ_2: 131;

        (((1 succ 1) * <: <*(n proj i)*>:>) . x9) = ((1 succ 1) . ( <: <*(n proj i)*>:> . x9)) by A8, FUNCT_1: 13

        .= ((1 succ 1) . <*((n proj i) . x9)*>) by A7, FINSEQ_3: 141

        .= ((1 succ 1) . <*(x9 . i)*>) by Th37

        .= ((ii /. 1) + 1) by Def7

        .= (xi + 1) by FINSEQ_4: 16;

        hence ((n succ i) . x) = (((1 succ 1) * <: <*(n proj i)*>:>) . x) by A10;

      end;

      then

       A11: (n succ i) = ((1 succ 1) * <: <*(n proj i)*>:>);



       A12: ( rng <*(n proj i)*>) c= P

      proof

        let x be object;

        assume x in ( rng <*(n proj i)*>);

        then x in {(n proj i)} by FINSEQ_1: 39;

        then x = (n proj i) by TARSKI:def 1;

        hence thesis by A3, A4, Def14;

      end;

      P is composition_closed by Def14;

      hence thesis by A11, A1, A2, A12, A5;

    end;

    theorem :: COMPUT_1:71



     Th70: {} in P

    proof

      reconsider F = {} as with_the_same_arity Element of (( HFuncs NAT ) * ) by FINSEQ_1: 49;

      set f = ( 0 const 0 );



       A1: ( rng {} ) c= P;



       A2: ( arity f) = 0 by Th31;



       A3: P is composition_closed by Def14;

      f in P by Th68;

      then (f * <:F:>) in P by A2, A1, A3, CARD_1: 27;

      hence thesis by FUNCT_6: 40;

    end;

    theorem :: COMPUT_1:72



     Th71: for f be Element of P, F be with_the_same_arity FinSequence of P st ( arity f) = ( len F) holds (f * <:F:>) in P

    proof

      let f be Element of P, F be with_the_same_arity FinSequence of P;

      assume

       A1: ( arity f) = ( len F);



       A2: ( rng F) c= P by FINSEQ_1:def 4;

      per cases ;

        suppose f is empty;

        then (f * <:F:>) = {} ;

        hence thesis by Th70;

      end;

        suppose f is non empty;

        then

        reconsider f9 = f as non empty Element of ( HFuncs NAT );



         A3: (P * ) c= (( HFuncs NAT ) * ) by FINSEQ_1: 62;

        F in (P * ) by FINSEQ_1:def 11;

        then

        reconsider F9 = F as with_the_same_arity Element of (( HFuncs NAT ) * ) by A3;

        P is composition_closed by Def14;

        then (f9 * <:F9:>) in P by A1, A2;

        hence thesis;

      end;

    end;

    theorem :: COMPUT_1:73



     Th72: for f1,f2 be Element of P st (( arity f1) + 2) = ( arity f2) holds for i be Element of NAT st 1 <= i & i <= (( arity f1) + 1) holds ( primrec (f1,f2,i)) in P

    proof

      let f1,f2 be Element of P;

      assume

       A1: (( arity f1) + 2) = ( arity f2);

      let i be Element of NAT ;

      assume that

       A2: 1 <= i and

       A3: i <= (( arity f1) + 1);



       A4: P is primitive-recursion_closed by Def14;

      per cases ;

        suppose f1 is empty;

        then ( primrec (f1,f2,i)) is empty by Th54;

        hence thesis by Th70;

      end;

        suppose f1 is non empty;

        then ( primrec (f1,f2,i)) is_primitive-recursively_expressed_by (f1,f2,i) by A1, A2, A3, Th17, Th63;

        hence thesis by A4;

      end;

    end;

    definition

      :: COMPUT_1:def15

      func PrimRec -> Subset of ( HFuncs NAT ) equals ( meet { R where R be Subset of ( HFuncs NAT ) : R is primitive-recursively_closed });

      coherence

      proof

        set S = { R where R be Subset of ( HFuncs NAT ) : R is primitive-recursively_closed };

        set T = ( meet S);



         A1: {( HFuncs NAT )} c= ( bool ( HFuncs NAT )) by ZFMISC_1: 68;

        ( HFuncs NAT ) in {( HFuncs NAT )} by TARSKI:def 1;

        then

         A2: ( HFuncs NAT ) in S by A1, Th65;

        T c= ( HFuncs NAT ) by A2, SETFAM_1:def 1;

        hence thesis;

      end;

    end

    theorem :: COMPUT_1:74



     Th73: for X be Subset of ( HFuncs NAT ) st X is primitive-recursively_closed holds PrimRec c= X

    proof

      let X be Subset of ( HFuncs NAT );

      set S = { R where R be Subset of ( HFuncs NAT ) : R is primitive-recursively_closed };

      assume X is primitive-recursively_closed;

      then

       A1: X in S;

      let x be object;

      assume x in PrimRec ;

      hence thesis by A1, SETFAM_1:def 1;

    end;

    registration

      cluster PrimRec -> non empty primitive-recursively_closed;

      coherence

      proof

        set S = { R where R be Subset of ( HFuncs NAT ) : R is primitive-recursively_closed };



         A1: {( HFuncs NAT )} c= ( bool ( HFuncs NAT )) by ZFMISC_1: 68;

        ( HFuncs NAT ) in {( HFuncs NAT )} by TARSKI:def 1;

        then

         A2: ( HFuncs NAT ) in S by A1, Th65;

         A3:

        now

          let Y be set;

          assume Y in S;

          then ex R be Subset of ( HFuncs NAT ) st R = Y & R is primitive-recursively_closed;

          hence ( 0 const 0 ) in Y;

        end;

        hence PrimRec is non empty by A2, SETFAM_1:def 1;

        thus PrimRec is primitive-recursively_closed

        proof

          thus ( 0 const 0 ) in PrimRec by A2, A3, SETFAM_1:def 1;

          now

            let Y be set;

            assume Y in S;

            then ex R be Subset of ( HFuncs NAT ) st R = Y & R is primitive-recursively_closed;

            hence (1 succ 1) in Y;

          end;

          hence (1 succ 1) in PrimRec by A2, SETFAM_1:def 1;

          hereby

            let n,i be Element of NAT ;

            assume that

             A4: 1 <= i and

             A5: i <= n;

            now

              let Y be set;

              assume Y in S;

              then ex R be Subset of ( HFuncs NAT ) st R = Y & R is primitive-recursively_closed;

              hence (n proj i) in Y by A4, A5;

            end;

            hence (n proj i) in PrimRec by A2, SETFAM_1:def 1;

          end;

          hereby

            let f be Element of ( HFuncs NAT ), F be with_the_same_arity FinSequence of ( HFuncs NAT ) such that

             A6: f in PrimRec and

             A7: ( arity f) = ( len F) and

             A8: ( rng F) c= PrimRec ;

            now

              let Y be set;

              assume

               A9: Y in S;

              then

              consider R be Subset of ( HFuncs NAT ) such that

               A10: R = Y and

               A11: R is primitive-recursively_closed;



               A12: R is composition_closed by A11;



               A13: PrimRec c= R by A9, A10, SETFAM_1: 3;

              then ( rng F) c= R by A8;

              hence (f * <:F:>) in Y by A6, A7, A10, A12, A13;

            end;

            hence (f * <:F:>) in PrimRec by A2, SETFAM_1:def 1;

          end;

          hereby

            let g,f1,f2 be Element of ( HFuncs NAT ), i be Element of NAT such that

             A14: g is_primitive-recursively_expressed_by (f1,f2,i) and

             A15: f1 in PrimRec and

             A16: f2 in PrimRec ;

            now

              let Y be set;

              assume

               A17: Y in S;

              then

              consider R be Subset of ( HFuncs NAT ) such that

               A18: R = Y and

               A19: R is primitive-recursively_closed;



               A20: f2 in R by A16, A17, A18, SETFAM_1:def 1;



               A21: R is primitive-recursion_closed by A19;

              f1 in R by A15, A17, A18, SETFAM_1:def 1;

              hence g in Y by A14, A18, A21, A20;

            end;

            hence g in PrimRec by A2, SETFAM_1:def 1;

          end;

        end;

      end;

    end

    registration

      cluster -> homogeneous for Element of PrimRec ;

      coherence ;

    end

    definition

      let x be set;

      :: COMPUT_1:def16

      attr x is primitive-recursive means

      : Def16: x in PrimRec ;

    end

    registration

      cluster primitive-recursive -> Relation-like Function-like for set;

      coherence ;

    end

    registration

      cluster primitive-recursive -> homogeneous to-naturals( NAT * ) -defined for Relation;

      coherence ;

    end

    registration

      cluster -> primitive-recursive for Element of PrimRec ;

      coherence ;

    end

    registration

      cluster primitive-recursive for Function;

      existence

      proof

        set x = the Element of PrimRec ;

        take x;

        thus thesis;

      end;

      cluster primitive-recursive for Element of ( HFuncs NAT );

      existence

      proof

        set x = the Element of PrimRec ;

        take x;

        thus thesis;

      end;

    end

    definition

      :: COMPUT_1:def17

      func initial-funcs -> Subset of ( HFuncs NAT ) equals ( {( 0 const 0 ), (1 succ 1)} \/ { (n proj i) where n,i be Element of NAT : 1 <= i & i <= n });

      coherence

      proof

        set Q1 = {( 0 const 0 ), (1 succ 1)}, Q2 = { (n proj i) where n,i be Element of NAT : 1 <= i & i <= n };



         A1: Q2 c= ( HFuncs NAT )

        proof

          let x be object;

          assume x in Q2;

          then ex n,i be Element of NAT st x = (n proj i) & 1 <= i & i <= n;

          hence thesis by Th34;

        end;

        Q1 c= ( HFuncs NAT )

        proof

          let x be object;

          assume x in Q1;

          then x = ( 0 const 0 ) or x = (1 succ 1) by TARSKI:def 2;

          hence thesis by Th30, Th32;

        end;

        hence thesis by A1, XBOOLE_1: 8;

      end;

      let Q be Subset of ( HFuncs NAT );

      :: COMPUT_1:def18

      func PR-closure Q -> Subset of ( HFuncs NAT ) equals (Q \/ { g where g be Element of ( HFuncs NAT ) : ex f1,f2 be Element of ( HFuncs NAT ), i be Element of NAT st f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by (f1,f2,i) });

      coherence

      proof

        set Q1 = { g where g be Element of ( HFuncs NAT ) : ex f1,f2 be Element of ( HFuncs NAT ), i be Element of NAT st f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by (f1,f2,i) };

        Q1 c= ( HFuncs NAT )

        proof

          let x be object;

          assume x in Q1;

          then ex g be Element of ( HFuncs NAT ) st x = g & ex f1,f2 be Element of ( HFuncs NAT ), i be Element of NAT st f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by (f1,f2,i);

          hence thesis;

        end;

        hence thesis by XBOOLE_1: 8;

      end;

      :: COMPUT_1:def19

      func composition-closure Q -> Subset of ( HFuncs NAT ) equals (Q \/ { (f * <:F:>) where f be Element of ( HFuncs NAT ), F be with_the_same_arity Element of (( HFuncs NAT ) * ) : f in Q & ( arity f) = ( len F) & ( rng F) c= Q });

      coherence

      proof

        set Q1 = { (f * <:F:>) where f be Element of ( HFuncs NAT ), F be with_the_same_arity Element of (( HFuncs NAT ) * ) : f in Q & ( arity f) = ( len F) & ( rng F) c= Q };

        Q1 c= ( HFuncs NAT )

        proof

          let x be object;

          assume x in Q1;

          then ex f be Element of ( HFuncs NAT ), F be with_the_same_arity Element of (( HFuncs NAT ) * ) st x = (f * <:F:>) & f in Q & ( arity f) = ( len F) & ( rng F) c= Q;

          hence thesis by Th41;

        end;

        hence thesis by XBOOLE_1: 8;

      end;

    end

    definition

      :: COMPUT_1:def20

      func PrimRec-Approximation -> sequence of ( bool ( HFuncs NAT )) means

      : Def20: (it . 0 ) = initial-funcs & for m be Nat holds (it . (m + 1)) = (( PR-closure (it . m)) \/ ( composition-closure (it . m)));

      existence

      proof

        deffunc f( set, Subset of ( HFuncs NAT )) = (( PR-closure $2) \/ ( composition-closure $2));

        consider A be sequence of ( bool ( HFuncs NAT )) such that

         A1: (A . 0 ) = initial-funcs and

         A2: for m be Nat holds (A . (m + 1)) = f(m,.) from NAT_1:sch 12;

        take A;

        thus (A . 0 ) = initial-funcs by A1;

        let m be Nat;

        thus thesis by A2;

      end;

      uniqueness

      proof

        deffunc f( set, Subset of ( HFuncs NAT )) = (( PR-closure $2) \/ ( composition-closure $2));

        let it1,it2 be sequence of ( bool ( HFuncs NAT )) such that

         A3: (it1 . 0 ) = initial-funcs and

         A4: for m be Nat holds (it1 . (m + 1)) = (( PR-closure (it1 . m)) \/ ( composition-closure (it1 . m))) and

         A5: (it2 . 0 ) = initial-funcs and

         A6: for m be Nat holds (it2 . (m + 1)) = (( PR-closure (it2 . m)) \/ ( composition-closure (it2 . m)));



         A7: for m be Nat holds (it1 . (m + 1)) = f(m,.) by A4;



         A8: for m be Nat holds (it2 . (m + 1)) = f(m,.) by A6;



         A9: (it2 . 0 ) = initial-funcs by A5;



         A10: (it1 . 0 ) = initial-funcs by A3;

        thus it1 = it2 from NAT_1:sch 16( A10, A7, A9, A8);

      end;

    end

    theorem :: COMPUT_1:75



     Th74: m <= n implies ( PrimRec-Approximation . m) c= ( PrimRec-Approximation . n)

    proof

      set prd = PrimRec-Approximation ;

      defpred p[ Nat] means m <= $1 implies (prd . m) c= (prd . $1);



       A1: for n be Nat st p[n] holds p[(n + 1)]

      proof

        let n be Nat such that

         A2: p[n] and

         A3: m <= (n + 1);

        (prd . (n + 1)) = (( PR-closure (prd . n)) \/ ( composition-closure (prd . n))) by Def20;

        then

         A4: ( PR-closure (prd . n)) c= (prd . (n + 1)) by XBOOLE_1: 7;

        (prd . n) c= ( PR-closure (prd . n)) by XBOOLE_1: 7;

        then

         A5: (prd . n) c= (prd . (n + 1)) by A4;

        per cases by A3, XXREAL_0: 1;

          suppose m < (n + 1);

          hence thesis by A2, A5, NAT_1: 13;

        end;

          suppose m = (n + 1);

          hence thesis;

        end;

      end;



       A6: p[ 0 ];

      for n be Nat holds p[n] from NAT_1:sch 2( A6, A1);

      hence thesis;

    end;

    theorem :: COMPUT_1:76



     Th75: ( Union PrimRec-Approximation ) is primitive-recursively_closed

    proof

      set PROJ = { (n proj i) where n,i be Element of NAT : 1 <= i & i <= n };

      set prd = PrimRec-Approximation ;

      set UP = ( Union prd);



       A1: ( dom prd) = NAT by FUNCT_2:def 1;



       A2: (prd . 0 ) = ( {( 0 const 0 ), (1 succ 1)} \/ PROJ) by Def20;

      ( 0 const 0 ) in {( 0 const 0 ), (1 succ 1)} by TARSKI:def 2;

      then ( 0 const 0 ) in (prd . 0 ) by A2, XBOOLE_0:def 3;

      hence ( 0 const 0 ) in UP by A1, CARD_5: 2;

      (1 succ 1) in {( 0 const 0 ), (1 succ 1)} by TARSKI:def 2;

      then (1 succ 1) in (prd . 0 ) by A2, XBOOLE_0:def 3;

      hence (1 succ 1) in UP by A1, CARD_5: 2;

      hereby

        let n,i be Element of NAT ;

        assume that

         A3: 1 <= i and

         A4: i <= n;

        (n proj i) in PROJ by A3, A4;

        then (n proj i) in (prd . 0 ) by A2, XBOOLE_0:def 3;

        hence (n proj i) in UP by A1, CARD_5: 2;

      end;

      hereby

        deffunc mcocl( Element of NAT ) = { (f * <:F:>) where f be Element of ( HFuncs NAT ), F be with_the_same_arity Element of (( HFuncs NAT ) * ) : f in (prd . $1) & ( arity f) = ( len F) & ( rng F) c= (prd . $1) };

        let f be Element of ( HFuncs NAT ), F be with_the_same_arity FinSequence of ( HFuncs NAT ) such that

         A5: f in UP and

         A6: ( arity f) = ( len F) and

         A7: ( rng F) c= UP;

        consider kf be object such that

         A8: kf in ( dom prd) and

         A9: f in (prd . kf) by A5, CARD_5: 2;

        reconsider kf as Element of NAT by A8;

        per cases ;

          suppose ( arity f) = 0 ;

          then F = {} by A6;

          then

           A10: ( rng F) c= (prd . kf);

          F is with_the_same_arity Element of (( HFuncs NAT ) * ) by FINSEQ_1:def 11;

          then (f * <:F:>) in mcocl(kf) by A6, A9, A10;

          then (f * <:F:>) in ((prd . kf) \/ mcocl(kf)) by XBOOLE_0:def 3;

          then (f * <:F:>) in (( PR-closure (prd . kf)) \/ ( composition-closure (prd . kf))) by XBOOLE_0:def 3;

          then (f * <:F:>) in (prd . (kf + 1)) by Def20;

          hence (f * <:F:>) in UP by A1, CARD_5: 2;

        end;

          suppose

           A11: ( arity f) <> 0 ;

          defpred B[ object, object] means ex k be Element of NAT st (F . $1) in (prd . k) & $2 = k;



           A12: for x be object st x in ( Seg ( len F)) holds ex y be Element of NAT st B[x, y]

          proof

            let x be object;

            assume x in ( Seg ( len F));

            then x in ( dom F) by FINSEQ_1:def 3;

            then (F . x) in ( rng F) by FUNCT_1:def 3;

            then

            consider k be object such that

             A13: k in ( dom prd) and

             A14: (F . x) in (prd . k) by A7, CARD_5: 2;

            reconsider k as Element of NAT by A13;

            take k;

            take k1 = k;

            thus (F . x) in (prd . k1) by A14;

            thus thesis;

          end;

          consider fKF be Function of ( Seg ( len F)), NAT such that

           A15: for x be object st x in ( Seg ( len F)) holds B[x, (fKF . x)] from MONOID_1:sch 1( A12);

          set KF = ( rng fKF);

          reconsider KF as non empty finite Subset of NAT by A6, A11, RELAT_1:def 19;

          set K = ( max KF);

          set k = ( max (kf,K));

          reconsider k as Element of NAT by ORDINAL1:def 12;



           A16: ( dom fKF) = ( Seg ( len F)) by FUNCT_2:def 1;



           A17: ( rng F) c= (prd . k)

          proof

            let x be object;



             A18: K <= k by XXREAL_0: 25;

            assume x in ( rng F);

            then

            consider d be object such that

             A19: d in ( dom F) and

             A20: x = (F . d) by FUNCT_1:def 3;



             A21: d in ( Seg ( len F)) by A19, FINSEQ_1:def 3;

            then

            consider m be Element of NAT such that

             A22: (F . d) in (prd . m) and

             A23: (fKF . d) = m by A15;

            m in KF by A16, A21, A23, FUNCT_1: 3;

            then m <= K by XXREAL_2:def 8;

            then (prd . m) c= (prd . k) by A18, Th74, XXREAL_0: 2;

            hence thesis by A20, A22;

          end;



           A24: F is with_the_same_arity Element of (( HFuncs NAT ) * ) by FINSEQ_1:def 11;

          (prd . kf) c= (prd . k) by Th74, XXREAL_0: 25;

          then (f * <:F:>) in mcocl(k) by A6, A9, A17, A24;

          then (f * <:F:>) in ((prd . k) \/ mcocl(k)) by XBOOLE_0:def 3;

          then (f * <:F:>) in (( PR-closure (prd . k)) \/ ( composition-closure (prd . k))) by XBOOLE_0:def 3;

          then (f * <:F:>) in (prd . (k + 1)) by Def20;

          hence (f * <:F:>) in UP by A1, CARD_5: 2;

        end;

      end;

      deffunc mprcl( Element of NAT ) = { g where g be Element of ( HFuncs NAT ) : ex f1,f2 be Element of ( HFuncs NAT ), i be Element of NAT st f1 in (prd . $1) & f2 in (prd . $1) & g is_primitive-recursively_expressed_by (f1,f2,i) };

      let g,f1,f2 be Element of ( HFuncs NAT ), i be Element of NAT such that

       A25: g is_primitive-recursively_expressed_by (f1,f2,i) and

       A26: f1 in UP and

       A27: f2 in UP;

      consider k2 be object such that

       A28: k2 in ( dom prd) and

       A29: f2 in (prd . k2) by A27, CARD_5: 2;

      reconsider k2 as Element of NAT by A28;

      consider k1 be object such that

       A30: k1 in ( dom prd) and

       A31: f1 in (prd . k1) by A26, CARD_5: 2;

      reconsider k1 as Element of NAT by A30;

      per cases ;

        suppose k1 <= k2;

        then (prd . k1) c= (prd . k2) by Th74;

        then g in mprcl(k2) by A25, A31, A29;

        then g in ((prd . k2) \/ mprcl(k2)) by XBOOLE_0:def 3;

        then g in (( PR-closure (prd . k2)) \/ ( composition-closure (prd . k2))) by XBOOLE_0:def 3;

        then g in (prd . (k2 + 1)) by Def20;

        hence thesis by A1, CARD_5: 2;

      end;

        suppose k2 <= k1;

        then (prd . k2) c= (prd . k1) by Th74;

        then g in mprcl(k1) by A25, A31, A29;

        then g in ((prd . k1) \/ mprcl(k1)) by XBOOLE_0:def 3;

        then g in (( PR-closure (prd . k1)) \/ ( composition-closure (prd . k1))) by XBOOLE_0:def 3;

        then g in (prd . (k1 + 1)) by Def20;

        hence thesis by A1, CARD_5: 2;

      end;

    end;

    theorem :: COMPUT_1:77



     Th76: PrimRec = ( Union PrimRec-Approximation )

    proof

      set prd = PrimRec-Approximation ;

      defpred p[ Nat] means (prd . $1) c= PrimRec ;

       A1:

      now

        let m be Nat such that

         A2: p[m];

        thus p[(m + 1)]

        proof

          set mcocl = { (f * <:F:>) where f be Element of ( HFuncs NAT ), F be with_the_same_arity Element of (( HFuncs NAT ) * ) : f in (prd . m) & ( arity f) = ( len F) & ( rng F) c= (prd . m) };

          set mprcl = { g where g be Element of ( HFuncs NAT ) : ex f1,f2 be Element of ( HFuncs NAT ), i be Element of NAT st f1 in (prd . m) & f2 in (prd . m) & g is_primitive-recursively_expressed_by (f1,f2,i) };

          let x be object;



           A3: (prd . (m + 1)) = (( PR-closure (prd . m)) \/ ( composition-closure (prd . m))) by Def20;

          assume

           A4: x in (prd . (m + 1));

          per cases by A4, A3, XBOOLE_0:def 3;

            suppose

             A5: x in ( PR-closure (prd . m));

            thus thesis

            proof

              per cases by A5, XBOOLE_0:def 3;

                suppose x in (prd . m);

                hence thesis by A2;

              end;

                suppose

                 A6: x in mprcl;



                 A7: PrimRec is primitive-recursion_closed by Def14;

                ex g be Element of ( HFuncs NAT ) st x = g & ex f1,f2 be Element of ( HFuncs NAT ), i be Element of NAT st f1 in (prd . m) & f2 in (prd . m) & g is_primitive-recursively_expressed_by (f1,f2,i) by A6;

                hence thesis by A2, A7;

              end;

            end;

          end;

            suppose

             A8: x in ( composition-closure (prd . m));

            thus thesis

            proof

              per cases by A8, XBOOLE_0:def 3;

                suppose x in (prd . m);

                hence thesis by A2;

              end;

                suppose

                 A9: x in mcocl;



                 A10: PrimRec is composition_closed by Def14;

                consider f be Element of ( HFuncs NAT ), F be with_the_same_arity Element of (( HFuncs NAT ) * ) such that

                 A11: x = (f * <:F:>) and

                 A12: f in (prd . m) and

                 A13: ( arity f) = ( len F) and

                 A14: ( rng F) c= (prd . m) by A9;

                ( rng F) c= PrimRec by A2, A14, XBOOLE_1: 1;

                hence thesis by A2, A11, A12, A13, A10;

              end;

            end;

          end;

        end;

      end;



       A15: p[ 0 ]

      proof

        let x be object;

        assume

         A16: x in (prd . 0 );

        (prd . 0 ) = ( {( 0 const 0 ), (1 succ 1)} \/ { (n proj i) where n,i be Element of NAT : 1 <= i & i <= n }) by Def20;

        then

         A17: x in {( 0 const 0 ), (1 succ 1)} or x in { (n proj i) where n,i be Element of NAT : 1 <= i & i <= n } by A16, XBOOLE_0:def 3;

        per cases by A17, TARSKI:def 2;

          suppose x = ( 0 const 0 );

          hence thesis by Def14;

        end;

          suppose x = (1 succ 1);

          hence thesis by Def14;

        end;

          suppose x in { (n proj i) where n,i be Element of NAT : 1 <= i & i <= n };

          then ex n,i be Element of NAT st x = (n proj i) & 1 <= i & i <= n;

          hence thesis by Def14;

        end;

      end;



       A18: for k be Nat holds p[k] from NAT_1:sch 2( A15, A1);



       A19: ( Union prd) c= PrimRec

      proof

        let x be object;

        assume that

         A20: x in ( Union prd) and

         A21: not x in PrimRec ;

        consider X be set such that

         A22: x in X and

         A23: X in ( rng prd) by A20, TARSKI:def 4;

        consider m be object such that

         A24: m in ( dom prd) and

         A25: (prd . m) = X by A23, FUNCT_1:def 3;

        reconsider m as Element of NAT by A24;

        (prd . m) c= PrimRec by A18;

        hence contradiction by A21, A22, A25;

      end;

       PrimRec c= ( Union prd) by Th73, Th75;

      hence thesis by A19, XBOOLE_0:def 10;

    end;

    theorem :: COMPUT_1:78



     Th77: for f be Element of ( HFuncs NAT ) st f in ( PrimRec-Approximation . m) holds f is quasi_total

    proof

      defpred p[ Nat] means for f be Element of ( HFuncs NAT ) st f in ( PrimRec-Approximation . $1) holds f is quasi_total;

      set prd = PrimRec-Approximation ;



       A1: for m be Nat st p[m] holds p[(m + 1)]

      proof

        let m be Nat;

        assume

         A2: p[m];

        let f be Element of ( HFuncs NAT );

        assume f in (prd . (m + 1));

        then

         A3: f in (( PR-closure (prd . m)) \/ ( composition-closure (prd . m))) by Def20;

        per cases by A3, XBOOLE_0:def 3;

          suppose

           A4: f in ( PR-closure (prd . m));

          thus f is quasi_total

          proof

            per cases by A4, XBOOLE_0:def 3;

              suppose f in (prd . m);

              hence thesis by A2;

            end;

              suppose f in { g where g be Element of ( HFuncs NAT ) : ex f1,f2 be Element of ( HFuncs NAT ), i be Element of NAT st f1 in (prd . m) & f2 in (prd . m) & g is_primitive-recursively_expressed_by (f1,f2,i) };

              then

              consider g be Element of ( HFuncs NAT ) such that

               A5: f = g and

               A6: ex f1,f2 be Element of ( HFuncs NAT ), i be Element of NAT st f1 in (prd . m) & f2 in (prd . m) & g is_primitive-recursively_expressed_by (f1,f2,i);

              consider f1,f2 be Element of ( HFuncs NAT ), i be Element of NAT such that

               A7: f1 in (prd . m) and

               A8: f2 in (prd . m) and

               A9: g is_primitive-recursively_expressed_by (f1,f2,i) by A6;



               A10: f2 is quasi_total by A2, A8;

              f1 is quasi_total by A2, A7;

              hence thesis by A5, A9, A10, Th67;

            end;

          end;

        end;

          suppose

           A11: f in ( composition-closure (prd . m));

          thus f is quasi_total

          proof

            per cases by A11, XBOOLE_0:def 3;

              suppose f in (prd . m);

              hence thesis by A2;

            end;

              suppose f in { (h * <:F:>) where h be Element of ( HFuncs NAT ), F be with_the_same_arity Element of (( HFuncs NAT ) * ) : h in (prd . m) & ( arity h) = ( len F) & ( rng F) c= (prd . m) };

              then

              consider h be Element of ( HFuncs NAT ), F be with_the_same_arity Element of (( HFuncs NAT ) * ) such that

               A12: f = (h * <:F:>) and

               A13: h in (prd . m) and

               A14: ( arity h) = ( len F) and

               A15: ( rng F) c= (prd . m);



               A16: for h be Element of ( HFuncs NAT ) st h in ( rng F) holds h is quasi_total by A2, A15;

              h is quasi_total by A2, A13;

              hence thesis by A12, A14, A16, Th45;

            end;

          end;

        end;

      end;



       A17: p[ 0 ]

      proof

        let f be Element of ( HFuncs NAT );

        assume f in (prd . 0 );

        then f in initial-funcs by Def20;

        then

         A18: f in {( 0 const 0 ), (1 succ 1)} or f in { (n proj i) where n,i be Element of NAT : 1 <= i & i <= n } by XBOOLE_0:def 3;

        per cases by A18, TARSKI:def 2;

          suppose f = ( 0 const 0 );

          hence thesis by Th28;

        end;

          suppose f = (1 succ 1);

          hence thesis by Th28;

        end;

          suppose f in { (n proj i) where n,i be Element of NAT : 1 <= i & i <= n };

          then ex n,i be Element of NAT st f = (n proj i) & 1 <= i & i <= n;

          hence thesis by Th28;

        end;

      end;

      for m be Nat holds p[m] from NAT_1:sch 2( A17, A1);

      hence thesis;

    end;

    registration

      cluster -> quasi_total homogeneous for Element of PrimRec ;

      coherence

      proof

        set prd = PrimRec-Approximation ;

        let f be Element of PrimRec ;

        consider X be set such that

         A1: f in X and

         A2: X in ( rng prd) by Th76, TARSKI:def 4;

        ex m be object st m in ( dom prd) & (prd . m) = X by A2, FUNCT_1:def 3;

        hence thesis by A1, Th77;

      end;

    end

    registration

      cluster primitive-recursive -> quasi_total for Element of ( HFuncs NAT );

      coherence ;

    end

    registration

      cluster primitive-recursive -> len-total for ( NAT * ) -defined Function;

      coherence

      proof

        let x be ( NAT * ) -defined Function;

        assume x in PrimRec ;

        then x is Element of PrimRec ;

        hence thesis;

      end;

      cluster non empty for Element of PrimRec ;

      existence

      proof

        ( 0 const 0 ) in PrimRec by Th68;

        hence thesis;

      end;

    end

    begin

    definition

      let n be set;

      let f be homogeneous Relation;

      :: COMPUT_1:def21

      attr f is n -ary means

      : Def21: ( arity f) = n;

    end

    registration

      cluster 1 -ary -> non empty for homogeneous Function;

      coherence

      proof

        let f be homogeneous Function;

        assume ( arity f) = 1;

        then ex x be FinSequence st x in ( dom f) by MARGREL1:def 25;

        hence thesis;

      end;

      cluster 2 -ary -> non empty for homogeneous Function;

      coherence

      proof

        let f be homogeneous Function;

        assume ( arity f) = 2;

        then ex x be FinSequence st x in ( dom f) by MARGREL1:def 25;

        hence thesis;

      end;

      cluster 3 -ary -> non empty for homogeneous Function;

      coherence

      proof

        let f be homogeneous Function;

        assume ( arity f) = 3;

        then ex x be FinSequence st x in ( dom f) by MARGREL1:def 25;

        hence thesis;

      end;

    end

    registration

      let n be non zero Element of NAT ;

      cluster (n proj 1) -> primitive-recursive;

      coherence

      proof

        1 <= n by NAT_1: 14;

        then (n proj 1) in PrimRec by Def14;

        hence thesis;

      end;

    end

    registration

      cluster (2 proj 2) -> primitive-recursive;

      coherence by Def14;

      cluster (1 succ 1) -> primitive-recursive;

      coherence by Th69;

      cluster (3 succ 3) -> primitive-recursive;

      coherence by Th69;

      let i be Element of NAT ;

      cluster ( 0 const i) -> 0 -ary;

      coherence by Th31;

      cluster (1 const i) -> 1 -ary;

      coherence by Th31;

      cluster (2 const i) -> 2 -ary;

      coherence by Th31;

      cluster (3 const i) -> 3 -ary;

      coherence by Th31;

      cluster (1 proj i) -> 1 -ary;

      coherence by Th36;

      cluster (2 proj i) -> 2 -ary;

      coherence by Th36;

      cluster (3 proj i) -> 3 -ary;

      coherence by Th36;

      cluster (1 succ i) -> 1 -ary;

      coherence by Th33;

      cluster (2 succ i) -> 2 -ary;

      coherence by Th33;

      cluster (3 succ i) -> 3 -ary;

      coherence by Th33;

      let j be Element of NAT ;

      cluster (i const j) -> primitive-recursive;

      coherence by Th68;

    end

    registration

      cluster 0 -ary primitive-recursive non empty for homogeneous Function;

      existence by Def14;

      cluster 1 -ary primitive-recursive for homogeneous Function;

      existence by Def14;

      cluster 2 -ary primitive-recursive for homogeneous Function;

      existence

      proof

        take f = (2 proj 1);

        thus f is 2 -ary;

        thus f in PrimRec by Def14;

      end;

      cluster 3 -ary primitive-recursive for homogeneous Function;

      existence

      proof

        take f = (3 proj 1);

        thus f is 3 -ary;

        thus f in PrimRec by Def14;

      end;

    end

    registration

      cluster non empty 0 -ary len-total to-naturals for homogeneous( NAT * ) -defined Function;

      existence

      proof

        ( 0 const 0 ) is 0 -ary;

        hence thesis;

      end;

      cluster non empty1 -ary len-total to-naturals for homogeneous( NAT * ) -defined Function;

      existence

      proof

        (1 const 0 ) is 1 -ary;

        hence thesis;

      end;

      cluster non empty2 -ary len-total to-naturals for homogeneous( NAT * ) -defined Function;

      existence

      proof

        (2 const 0 ) is 2 -ary;

        hence thesis;

      end;

      cluster non empty3 -ary len-total to-naturals for homogeneous( NAT * ) -defined Function;

      existence

      proof

        (3 const 0 ) is 3 -ary;

        hence thesis;

      end;

    end

    registration

      let f be 0 -ary non empty primitive-recursive Function;

      let g be 2 -ary primitive-recursive Function;

      cluster ( primrec (f,g,1)) -> primitive-recursive1 -ary;

      coherence

      proof



         A1: g in PrimRec by Def16;



         A2: ( arity f) = 0 by Def21;

        f is Element of PrimRec by Def16;



        then ( dom f) = ( 0 -tuples_on NAT ) by A2, Th21

        .= {( <*> NAT )} by FINSEQ_2: 94;

        then

         A3: {} in ( dom f) by TARSKI:def 1;



         A4: f in PrimRec by Def16;



         A5: 1 <= ( 0 + 1);

        ( arity g) = ( 0 + 2) by Def21;

        hence ( primrec (f,g,1)) in PrimRec by A5, A2, A4, A1, Th72;

        reconsider ii = <* 0 *> as Element of (1 -tuples_on NAT ) by FINSEQ_2: 131;

        ( dom <* 0 *>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then

         A6: 1 in ( dom <* 0 *>) by TARSKI:def 1;

        ( Del ( <* 0 *>,1)) = {} by WSIERP_1: 19;

        then (ii +* (1, 0 )) in ( dom ( primrec (f,g,1))) by A5, A2, A3, A6, Lm6;

        then

         A7: <* 0 *> in ( dom ( primrec (f,g,1))) by FUNCT_7: 95;

        ( len <* 0 *>) = 1 by FINSEQ_1: 39;

        hence ( arity ( primrec (f,g,1))) = 1 by A7, MARGREL1:def 25;

      end;

    end

    registration

      let f be 1 -ary primitive-recursive Function;

      let g be 3 -ary primitive-recursive Function;

      cluster ( primrec (f,g,1)) -> primitive-recursive2 -ary;

      coherence

      proof



         A1: g in PrimRec by Def16;



         A2: 1 <= (1 + 1);



         A3: ( arity g) = (1 + 2) by Def21;



         A4: ( arity f) = 1 by Def21;

        f in PrimRec by Def16;

        hence ( primrec (f,g,1)) in PrimRec by A2, A4, A3, A1, Th72;

        thus ( arity ( primrec (f,g,1))) = 2 by A2, A4, A3, Th56;

      end;

      cluster ( primrec (f,g,2)) -> primitive-recursive2 -ary;

      coherence

      proof



         A5: g in PrimRec by Def16;



         A6: 2 <= (1 + 1);



         A7: ( arity g) = (1 + 2) by Def21;



         A8: ( arity f) = 1 by Def21;

        f in PrimRec by Def16;

        hence ( primrec (f,g,2)) in PrimRec by A6, A8, A7, A5, Th72;

        thus ( arity ( primrec (f,g,2))) = 2 by A6, A8, A7, Th56;

      end;

    end

    theorem :: COMPUT_1:79



     Th78: for f1 be 1 -ary len-total to-naturals homogeneous( NAT * ) -defined Function, f2 be non empty to-naturals homogeneous( NAT * ) -defined Function holds (( primrec (f1,f2,2)) . <*i, 0 *>) = (f1 . <*i*>)

    proof

      let f1 be 1 -ary len-total to-naturals homogeneous( NAT * ) -defined Function, f2 be non empty to-naturals homogeneous( NAT * ) -defined Function;

      ( arity f1) = 1 by Def21;

      then

      reconsider p = <*i, 0 *> as Element of ((( arity f1) + 1) -tuples_on NAT ) by FINSEQ_2: 101;

      ( len p) = 2 by FINSEQ_1: 44;

      then

       A1: 2 in ( dom p) by FINSEQ_3: 25;

      (p +* (2, 0 )) = p by Th1;



      hence (( primrec (f1,f2,2)) . <*i, 0 *>) = (f1 . ( Del (p,2))) by A1, Th59

      .= (f1 . <*i*>) by WSIERP_1: 19;

    end;

    theorem :: COMPUT_1:80



     Th79: f1 is len-total & ( arity f1) = 0 implies (( primrec (f1,f2,1)) . <* 0 *>) = (f1 . {} )

    proof

      assume that

       A1: f1 is len-total and

       A2: ( arity f1) = 0 ;

      reconsider p = <* 0 *> as Element of ((( arity f1) + 1) -tuples_on NAT ) by A2, FINSEQ_2: 131;

      ( len p) = 1 by FINSEQ_1: 39;

      then

       A3: 1 in ( dom p) by FINSEQ_3: 25;

      (p +* (1, 0 )) = p by FUNCT_7: 95;



      hence (( primrec (f1,f2,1)) . <* 0 *>) = (f1 . ( Del (p,1))) by A1, A3, Th59

      .= (f1 . {} ) by WSIERP_1: 19;

    end;

    theorem :: COMPUT_1:81



     Th80: for f1 be 1 -ary len-total to-naturals homogeneous( NAT * ) -defined Function, f2 be 3 -ary len-total to-naturals homogeneous( NAT * ) -defined Function holds (( primrec (f1,f2,2)) . <*i, (j + 1)*>) = (f2 . <*i, j, (( primrec (f1,f2,2)) . <*i, j*>)*>)

    proof

      let f1 be 1 -ary len-total to-naturals homogeneous( NAT * ) -defined Function, f2 be 3 -ary len-total to-naturals homogeneous( NAT * ) -defined Function;



       A1: ( arity f1) = 1 by Def21;

      then

      reconsider p = <*i, j*> as Element of ((( arity f1) + 1) -tuples_on NAT ) by FINSEQ_2: 101;



       A2: (p +* (2,(j + 1))) = <*i, (j + 1)*> by Th1;



       A3: (p +* (2,j)) = <*i, j*> by Th1;

      (( arity f1) + 2) = ( arity f2) by A1, Def21;



      hence (( primrec (f1,f2,2)) . <*i, (j + 1)*>) = (f2 . ((p +* (2,j)) ^ <*(( primrec (f1,f2,2)) . (p +* (2,j)))*>)) by A1, A2, Th62

      .= (f2 . <*i, j, (( primrec (f1,f2,2)) . <*i, j*>)*>) by A3, FINSEQ_1: 43;

    end;

    theorem :: COMPUT_1:82



     Th81: f1 is len-total & f2 is len-total & ( arity f1) = 0 & ( arity f2) = 2 implies (( primrec (f1,f2,1)) . <*(i + 1)*>) = (f2 . <*i, (( primrec (f1,f2,1)) . <*i*>)*>)

    proof

      assume that

       A1: f1 is len-total and

       A2: f2 is len-total and

       A3: ( arity f1) = 0 and

       A4: ( arity f2) = 2;

      reconsider p = <*i*> as Element of ((( arity f1) + 1) -tuples_on NAT ) by A3, FINSEQ_2: 131;



       A5: (p +* (1,(i + 1))) = <*(i + 1)*> by FUNCT_7: 95;



       A6: (p +* (1,i)) = <*i*> by FUNCT_7: 95;

      (( arity f1) + 2) = ( arity f2) by A3, A4;



      hence (( primrec (f1,f2,1)) . <*(i + 1)*>) = (f2 . ((p +* (1,i)) ^ <*(( primrec (f1,f2,1)) . (p +* (1,i)))*>)) by A1, A2, A3, A5, Th62

      .= (f2 . <*i, (( primrec (f1,f2,1)) . <*i*>)*>) by A6, FINSEQ_1:def 9;

    end;

     Lm8:

    now

      reconsider z3 = <* 0 , 0 , 0 *> as FinSequence of NAT ;

      let g be quasi_total homogeneous non empty PartFunc of ( NAT * ), NAT ;

      set G = (g * <: <*(3 proj 1), (3 proj 3)*>:>);



       A1: ( rng G) c= NAT by RELAT_1:def 19;

      assume

       A2: ( arity g) = 2;

      then

       A3: ( dom g) = (2 -tuples_on NAT ) by Th21;

      thus

       A4: ( dom <: <*(3 proj 1), (3 proj 3)*>:>) = (( dom (3 proj 1)) /\ ( dom (3 proj 3))) by FINSEQ_3: 142;



      hence

       A5: ( dom <: <*(3 proj 1), (3 proj 3)*>:>) = ((3 -tuples_on NAT ) /\ ( dom (3 proj 3))) by Th35

      .= ((3 -tuples_on NAT ) /\ (3 -tuples_on NAT )) by Th35

      .= (3 -tuples_on NAT );

      now

        set f = <*(3 proj 1), (3 proj 3)*>;

        let x be object;

        set F = <:f:>;



         A6: ( product ( rngs f)) = ( product <*( rng (3 proj 1)), ( rng (3 proj 3))*>) by FINSEQ_3: 133

        .= ( product <* NAT , ( rng (3 proj 3))*>) by Th35

        .= ( product <* NAT , NAT *>) by Th35

        .= (2 -tuples_on NAT ) by FINSEQ_3: 128;

        hereby



           A7: ( rng F) c= ( product ( rngs f)) by FUNCT_6: 29;

          assume x in ( rng F);

          hence x in ( dom g) by A3, A6, A7;

        end;

        assume x in ( dom g);

        then x is Element of (2 -tuples_on NAT ) by A2, Th21;

        then

        consider d1,d2 be Element of NAT such that

         A8: x = <*d1, d2*> by FINSEQ_2: 100;

        reconsider x9 = <*d1, 0 , d2*> as Element of (3 -tuples_on NAT ) by FINSEQ_2: 104;

        (F . x9) = <*((3 proj 1) . x9), ((3 proj 3) . x9)*> by A4, A5, FINSEQ_3: 142

        .= <*(x9 . 1), ((3 proj 3) . x9)*> by Th37

        .= <*(x9 . 1), (x9 . 3)*> by Th37

        .= <*d1, (x9 . 3)*> by FINSEQ_1: 45

        .= x by A8, FINSEQ_1: 45;

        hence x in ( rng F) by A5, FUNCT_1:def 3;

      end;

      then ( rng <: <*(3 proj 1), (3 proj 3)*>:>) = ( dom g) by TARSKI: 2;

      hence

       A9: ( dom (g * <: <*(3 proj 1), (3 proj 3)*>:>)) = (3 -tuples_on NAT ) by A5, RELAT_1: 27;

      then

      reconsider G as PartFunc of ( NAT * ), NAT by A1, FINSEQ_2: 142, RELSET_1: 4;

      reconsider G as homogeneous PartFunc of ( NAT * ), NAT by A9, MARGREL1:def 21;

      take G;

      thus G = (g * <: <*(3 proj 1), (3 proj 3)*>:>);

      G is Element of ( PFuncs (( NAT * ), NAT )) by PARTFUN1: 45;

      then G in ( HFuncs NAT );

      hence G is Element of ( HFuncs NAT );

      ( len z3) = 3 by FINSEQ_1: 45;

      then

       A10: z3 is Element of (3 -tuples_on NAT ) by FINSEQ_2: 92;

      for x be FinSequence st x in ( dom G) holds 3 = ( len x) by A9, CARD_1:def 7;

      hence ( arity G) = 3 by A10, A9, MARGREL1:def 25;

      hence G is quasi_total non empty by A9, Th21;

    end;

    definition

      let g be Function;

      :: COMPUT_1:def22

      func (1,2)->(1,?,2) g -> Function equals (g * <: <*(3 proj 1), (3 proj 3)*>:>);

      coherence ;

    end

    registration

      let g be to-naturals( NAT * ) -defined Function;

      cluster ( (1,2)->(1,?,2) g) -> to-naturals( NAT * ) -defined;

      coherence

      proof

        set G = ( (1,2)->(1,?,2) g);



         A1: (3 -tuples_on NAT ) c= ( NAT * ) by FINSEQ_2: 142;

        ( dom <: <*(3 proj 1), (3 proj 3)*>:>) = (( dom (3 proj 1)) /\ ( dom (3 proj 3))) by FINSEQ_3: 142;



        then

         A2: ( dom <: <*(3 proj 1), (3 proj 3)*>:>) = ((3 -tuples_on NAT ) /\ ( dom (3 proj 3))) by Th35

        .= ((3 -tuples_on NAT ) /\ (3 -tuples_on NAT )) by Th35

        .= (3 -tuples_on NAT );

        ( dom G) c= ( dom <: <*(3 proj 1), (3 proj 3)*>:>) by RELAT_1: 25;

        then ( dom G) c= ( NAT * ) by A2, A1;

        hence thesis;

      end;

    end

    registration

      let g be homogeneous Function;

      cluster ( (1,2)->(1,?,2) g) -> homogeneous;

      coherence

      proof

        set G = ( (1,2)->(1,?,2) g);

        ( dom <: <*(3 proj 1), (3 proj 3)*>:>) = (( dom (3 proj 1)) /\ ( dom (3 proj 3))) by FINSEQ_3: 142;



        then ( dom <: <*(3 proj 1), (3 proj 3)*>:>) = ((3 -tuples_on NAT ) /\ ( dom (3 proj 3))) by Th35

        .= ((3 -tuples_on NAT ) /\ (3 -tuples_on NAT )) by Th35

        .= (3 -tuples_on NAT );

        then ( dom G) c= (3 -tuples_on NAT ) by RELAT_1: 25;

        hence ( dom G) is with_common_domain;

      end;

    end

    registration

      let g be 2 -ary len-total to-naturals homogeneous( NAT * ) -defined Function;

      cluster ( (1,2)->(1,?,2) g) -> non empty3 -ary len-total;

      coherence

      proof



         A1: g is quasi_total homogeneous non empty PartFunc of ( NAT * ), NAT by Th16;

        ( arity g) = 2 by Def21;

        then

        consider G be homogeneous PartFunc of ( NAT * ), NAT such that

         A2: G = (g * <: <*(3 proj 1), (3 proj 3)*>:>) and G is Element of ( HFuncs NAT ) and

         A3: ( arity G) = 3 and

         A4: G is quasi_total non empty by A1, Lm8;

        reconsider G9 = G as quasi_total non empty homogeneous PartFunc of ( NAT * ), NAT by A4;

        G9 is non empty3 -ary len-total to-naturals homogeneous( NAT * ) -defined Function by A3, Def21;

        hence thesis by A2;

      end;

    end

    theorem :: COMPUT_1:83



     Th82: for f be 2 -ary len-total to-naturals homogeneous( NAT * ) -defined Function holds (( (1,2)->(1,?,2) f) . <*i, j, k*>) = (f . <*i, k*>)

    proof

      let f be 2 -ary len-total to-naturals homogeneous( NAT * ) -defined Function;

      reconsider ff = f as quasi_total homogeneous non empty PartFunc of ( NAT * ), NAT by Th16;

      reconsider ijk = <*i, j, k*> as Element of (3 -tuples_on NAT ) by FINSEQ_2: 104;



       A1: ( arity ff) = 2 by Def21;

      then

       A2: ( dom <: <*(3 proj 1), (3 proj 3)*>:>) = (( dom (3 proj 1)) /\ ( dom (3 proj 3))) by Lm8;



       A3: ( dom <: <*(3 proj 1), (3 proj 3)*>:>) = (3 -tuples_on NAT ) by A1, Lm8;

      ( dom (ff * <: <*(3 proj 1), (3 proj 3)*>:>)) = (3 -tuples_on NAT ) by A1, Lm8;



      hence (( (1,2)->(1,?,2) f) . <*i, j, k*>) = (f . ( <: <*(3 proj 1), (3 proj 3)*>:> . ijk)) by FUNCT_1: 12

      .= (f . <*((3 proj 1) . ijk), ((3 proj 3) . ijk)*>) by A2, A3, FINSEQ_3: 142

      .= (f . <*(ijk . 1), ((3 proj 3) . ijk)*>) by Th37

      .= (f . <*(ijk . 1), (ijk . 3)*>) by Th37

      .= (f . <*i, (ijk . 3)*>) by FINSEQ_1: 45

      .= (f . <*i, k*>) by FINSEQ_1: 45;

    end;

    theorem :: COMPUT_1:84



     Th83: for g be 2 -ary primitive-recursive Function holds ( (1,2)->(1,?,2) g) in PrimRec

    proof



       A1: (3 proj 3) in PrimRec by Def14;



       A2: (2 -tuples_on PrimRec ) c= ( PrimRec * ) by FINSEQ_2: 142;

      (3 proj 1) in PrimRec by Def14;

      then <*(3 proj 1), (3 proj 3)*> in (2 -tuples_on PrimRec ) by A1, FINSEQ_2: 101;

      then

      reconsider F = <*(3 proj 1), (3 proj 3)*> as Element of ( PrimRec * ) by A2;

      F is with_the_same_arity

      proof

        let f,g be Function;

        assume that

         A3: f in ( rng F) and

         A4: g in ( rng F);



         A5: ( rng F) = {(3 proj 1), (3 proj 3)} by FINSEQ_2: 127;

        hence f is empty implies g is empty or ( dom g) = { {} } by A3, TARSKI:def 2;

        assume that f is non empty and g is non empty;

        take 3, NAT ;

        f = (3 proj 1) or f = (3 proj 3) by A3, A5, TARSKI:def 2;

        hence ( dom f) c= (3 -tuples_on NAT ) by Th35;

        g = (3 proj 1) or g = (3 proj 3) by A4, A5, TARSKI:def 2;

        hence thesis by Th35;

      end;

      then

      reconsider F as with_the_same_arity Element of ( PrimRec * );

      let g be 2 -ary primitive-recursive Function;

      ( arity g) = 2 by Def21;

      then

       A6: ( arity g) = ( len F) by FINSEQ_1: 44;

      g is Element of PrimRec by Def16;

      hence thesis by A6, Th71;

    end;

    registration

      let f be 2 -ary primitive-recursive homogeneous Function;

      cluster ( (1,2)->(1,?,2) f) -> primitive-recursive3 -ary;

      coherence by Th83;

    end

    definition

      :: COMPUT_1:def23

      func [+] -> 2 -ary primitive-recursive Function equals ( primrec ((1 proj 1),(3 succ 3),2));

      coherence ;

    end

    theorem :: COMPUT_1:85



     Th84: ( [+] . <*i, j*>) = (i + j)

    proof

      reconsider q = <*i*> as Element of (1 -tuples_on NAT ) by FINSEQ_2: 131;

      defpred p[ Nat] means ( [+] . <*i, $1*>) = (i + $1);

       A1:

      now

        let j be Nat;

        reconsider jj = j as Element of NAT by ORDINAL1:def 12;

        reconsider r = <*i, jj, (i + jj)*> as Element of (3 -tuples_on NAT ) by FINSEQ_2: 104;

        assume p[j];



        then ( [+] . <*i, (jj + 1)*>) = ((3 succ 3) . r) by Th80

        .= ((r /. 3) + 1) by Def7

        .= ((i + jj) + 1) by FINSEQ_4: 18

        .= (i + (j + 1));

        hence p[(j + 1)];

      end;

      ( [+] . <*i, 0 *>) = ((1 proj 1) . q) by Th78

      .= (q . 1) by Th37

      .= (i + 0 ) by FINSEQ_1: 40;

      then

       A2: p[ 0 ];

      for j be Nat holds p[j] from NAT_1:sch 2( A2, A1);

      hence thesis;

    end;

    definition

      :: COMPUT_1:def24

      func [*] -> 2 -ary primitive-recursive Function equals ( primrec ((1 const 0 ),( (1,2)->(1,?,2) [+] ),2));

      coherence ;

    end

    theorem :: COMPUT_1:86



     Th85: for i,j be Nat holds ( [*] . <*i, j*>) = (i * j)

    proof

      let i be Nat;

      reconsider i1 = i as Element of NAT by ORDINAL1:def 12;

      defpred p[ Nat] means ( [*] . <*i, $1*>) = (i * $1);

       A1:

      now

        let j be Nat;

        reconsider jj = j as Element of NAT by ORDINAL1:def 12;

        assume p[j];



        then ( [*] . <*i1, (jj + 1)*>) = (( (1,2)->(1,?,2) [+] ) . <*i, jj, (i * jj)*>) by Th80

        .= ( [+] . <*i1, (i1 * jj)*>) by Th82

        .= ((i * 1) + (i * jj)) by Th84

        .= (i * (j + 1));

        hence p[(j + 1)];

      end;

      reconsider ii = <*i1*> as Element of (1 -tuples_on NAT ) by FINSEQ_2: 98;

      ( [*] . <*i, 0 *>) = ((1 const 0 ) . ii) by Th78

      .= (i * 0 );

      then

       A2: p[ 0 ];

      thus for i be Nat holds p[i] from NAT_1:sch 2( A2, A1);

    end;

    registration

      let g,h be 2 -ary primitive-recursive homogeneous Function;

      cluster <*g, h*> -> with_the_same_arity;

      coherence

      proof

        reconsider g, h as Element of PrimRec by Def16;



         A1: ( rng <*g, h*>) = {g, h} by FINSEQ_2: 127;

         A2:

        now

          let f1,f2 be homogeneous Function;

          assume that

           A3: f1 in ( rng <*g, h*>) and

           A4: f2 in ( rng <*g, h*>);

          f1 = g or f1 = h by A1, A3, TARSKI:def 2;

          then

           A5: ( arity f1) = 2 by Def21;

          f2 = g or f2 = h by A1, A4, TARSKI:def 2;

          hence ( arity f1) = ( arity f2) by A5, Def21;

        end;

        ( rng <*g, h*>) c= PrimRec by FINSEQ_1:def 4;

        hence thesis by A2, Th29, XBOOLE_1: 1;

      end;

    end

    registration

      let f,g,h be 2 -ary primitive-recursive Function;

      cluster (f * <: <*g, h*>:>) -> primitive-recursive;

      coherence

      proof

        reconsider g9 = g, h9 = h as Element of PrimRec by Def16;



         A1: f in PrimRec by Def16;



         A2: ( rng <*g9, h9*>) c= PrimRec by FINSEQ_1:def 4;

        then ( rng <*g, h*>) c= ( HFuncs NAT ) by XBOOLE_1: 1;

        then

        reconsider F = <*g, h*> as with_the_same_arity FinSequence of ( HFuncs NAT ) by FINSEQ_1:def 4;



         A3: PrimRec is composition_closed by Def14;



         A4: ( arity f) = 2 by Def21;

        ( len F) = 2 by FINSEQ_1: 44;

        hence (f * <: <*g, h*>:>) in PrimRec by A2, A1, A3, A4;

      end;

    end

    registration

      let f,g,h be 2 -ary primitive-recursive Function;

      cluster (f * <: <*g, h*>:>) -> 2 -ary;

      coherence

      proof

        set x = the Element of (2 -tuples_on NAT );

        reconsider f9 = f, fgh = (f * <: <*g, h*>:>), g9 = g, h9 = h as Element of PrimRec by Def16;



         A1: f9 = f;

        ( rng <*g9, h9*>) c= PrimRec by FINSEQ_1:def 4;

        then ( rng <*g, h*>) c= ( HFuncs NAT ) by XBOOLE_1: 1;

        then

        reconsider F = <*g, h*> as with_the_same_arity FinSequence of ( HFuncs NAT ) by FINSEQ_1:def 4;



         A2: ( dom <:F:>) = (( dom g) /\ ( dom h)) by FINSEQ_3: 142;



         A3: ( arity g) = 2 by Def21;

        ( rng F) = {g, h} by FINSEQ_2: 127;

        then g in ( rng F) by TARSKI:def 2;

        then

         A4: ( arity F) = 2 by A3, Def4;

        ( arity f) = 2 by Def21;

        then

         A5: ( dom f9) = (2 -tuples_on NAT ) by Lm1;

        ( arity h) = 2 by Def21;

        then

         A6: ( dom h9) = (2 -tuples_on NAT ) by Lm1;



         A7: ( dom g9) = (2 -tuples_on NAT ) by A3, Lm1;

        then ( <:F:> . x) = <*(g9 . x), (h9 . x)*> by A6, A2, FINSEQ_3: 142;

        then ( <:F:> . x) is Element of (2 -tuples_on NAT ) by FINSEQ_2: 101;

        then fgh is non empty by A5, A7, A6, A2, FUNCT_1: 11, RELAT_1: 38;

        hence ( arity (f * <: <*g, h*>:>)) = 2 by A1, A4, Th43;

      end;

    end

    registration

      let f be 1 -ary primitive-recursive Function;

      let g be primitive-recursive Function;

      cluster (f * <: <*g*>:>) -> primitive-recursive;

      coherence

      proof

        reconsider g9 = g as Element of PrimRec by Def16;



         A1: f in PrimRec by Def16;



         A2: ( rng <*g9*>) c= PrimRec by FINSEQ_1:def 4;

        then ( rng <*g*>) c= ( HFuncs NAT ) by XBOOLE_1: 1;

        then

        reconsider F = <*g9*> as with_the_same_arity FinSequence of ( HFuncs NAT ) by FINSEQ_1:def 4;



         A3: PrimRec is composition_closed by Def14;



         A4: ( arity f) = 1 by Def21;

        ( len F) = 1 by FINSEQ_1: 39;

        hence (f * <: <*g*>:>) in PrimRec by A2, A1, A3, A4;

      end;

    end

    registration

      let f be 1 -ary primitive-recursive Function;

      let g be 2 -ary primitive-recursive Function;

      cluster (f * <: <*g*>:>) -> 2 -ary;

      coherence

      proof

        set x = the Element of (2 -tuples_on NAT );

        reconsider f9 = f, fg = (f * <: <*g*>:>), g9 = g as Element of PrimRec by Def16;



         A1: f9 = f;

        ( rng <*g9*>) c= PrimRec by FINSEQ_1:def 4;

        then ( rng <*g*>) c= ( HFuncs NAT ) by XBOOLE_1: 1;

        then

        reconsider F = <*g9*> as with_the_same_arity FinSequence of ( HFuncs NAT ) by FINSEQ_1:def 4;



         A2: ( dom <:F:>) = ( dom g) by FINSEQ_3: 141;

        ( arity f) = 1 by Def21;

        then

         A3: ( dom f9) = (1 -tuples_on NAT ) by Lm1;



         A4: ( arity g) = 2 by Def21;

        ( rng F) = {g} by FINSEQ_1: 39;

        then g in ( rng F) by TARSKI:def 1;

        then

         A5: ( arity F) = 2 by A4, Def4;



         A6: ( dom g9) = (2 -tuples_on NAT ) by A4, Lm1;

        then ( <:F:> . x) = <*(g9 . x)*> by FINSEQ_3: 141;

        then ( <:F:> . x) in (1 -tuples_on NAT ) by FINSEQ_2: 98;

        then fg is non empty by A6, A2, A3, FUNCT_1: 11, RELAT_1: 38;

        hence ( arity (f * <: <*g*>:>)) = 2 by A1, A5, Th43;

      end;

    end

    definition

      :: COMPUT_1:def25

      func [!] -> 1 -ary primitive-recursive Function equals ( primrec (( 0 const 1),( [*] * <: <*((1 succ 1) * <: <*(2 proj 1)*>:>), (2 proj 2)*>:>),1));

      coherence ;

    end

    scheme :: COMPUT_1:sch1

    Primrec1 { F() -> 1 -ary len-total to-naturals homogeneous( NAT * ) -defined Function , G() -> 2 -ary len-total to-naturals homogeneous( NAT * ) -defined Function , f( set) -> Element of NAT , g( set, set) -> Element of NAT } :

for i,j be Element of NAT holds ((F() * <: <*G()*>:>) . <*i, j*>) = f(g)

      provided

       A1: for i be Element of NAT holds (F() . <*i*>) = f(i)

       and

       A2: for i,j be Element of NAT holds (G() . <*i, j*>) = g(i,j);

      let i,j be Element of NAT ;

      ( arity G()) = 2 by Def21;

      then

       A3: ( dom G()) = (2 -tuples_on NAT ) by Th22;

      ( dom <: <*G()*>:>) = ( dom G()) by FINSEQ_3: 141;



      hence ((F() * <: <*G()*>:>) . <*i, j*>) = (F() . ( <: <*G()*>:> . <*i, j*>)) by A3, FINSEQ_2: 101, FUNCT_1: 13

      .= (F() . <*(G() . <*i, j*>)*>) by A3, FINSEQ_2: 101, FINSEQ_3: 141

      .= (F() . <*g(i,j)*>) by A2

      .= f(g) by A1;

    end;

    scheme :: COMPUT_1:sch2

    Primrec2 { F,G,H() -> 2 -ary len-total to-naturals homogeneous( NAT * ) -defined Function , f,g,h( set, set) -> Element of NAT } :

for i,j be Element of NAT holds ((F() * <: <*G(), H()*>:>) . <*i, j*>) = f(g,h)

      provided

       A1: for i,j be Element of NAT holds (F() . <*i, j*>) = f(i,j)

       and

       A2: for i,j be Element of NAT holds (G() . <*i, j*>) = g(i,j)

       and

       A3: for i,j be Element of NAT holds (H() . <*i, j*>) = h(i,j);

      let i,j be Element of NAT ;

      ( arity G()) = 2 by Def21;

      then

       A4: ( dom G()) = (2 -tuples_on NAT ) by Th22;

      ( arity H()) = 2 by Def21;

      then

       A5: ( dom H()) = (2 -tuples_on NAT ) by Th22;



       A6: ( dom <: <*G(), H()*>:>) = (( dom G()) /\ ( dom H())) by FINSEQ_3: 142;



      hence ((F() * <: <*G(), H()*>:>) . <*i, j*>) = (F() . ( <: <*G(), H()*>:> . <*i, j*>)) by A4, A5, FINSEQ_2: 101, FUNCT_1: 13

      .= (F() . <*(G() . <*i, j*>), (H() . <*i, j*>)*>) by A6, A4, A5, FINSEQ_2: 101, FINSEQ_3: 142

      .= (F() . <*g(i,j), (H() . <*i, j*>)*>) by A2

      .= (F() . <*g(i,j), h(i,j)*>) by A3

      .= f(g,h) by A1;

    end;

    theorem :: COMPUT_1:87

    ( [!] . <*i*>) = (i ! )

    proof

      defpred p[ Nat] means ( [!] . <*$1*>) = ($1 ! );

      deffunc c( Element of NAT , Element of NAT ) = $2;

      deffunc a( Element of NAT , Element of NAT ) = ($1 * $2);

      deffunc g( Element of NAT , Element of NAT ) = $1;

      deffunc f( Element of NAT ) = ($1 + 1);

      set g = ( [*] * <: <*((1 succ 1) * <: <*(2 proj 1)*>:>), (2 proj 2)*>:>);

      deffunc b( Element of NAT , Element of NAT ) = f(g);



       A1: for i,j be Element of NAT holds ((2 proj 1) . <*i, j*>) = g(i,j)

      proof

        let i,j be Element of NAT ;

        reconsider ij = <*i, j*> as Element of (2 -tuples_on NAT ) by FINSEQ_2: 101;



        thus ((2 proj 1) . <*i, j*>) = (ij . 1) by Th37

        .= i by FINSEQ_1: 44;

      end;



       A2: for i be Element of NAT holds ((1 succ 1) . <*i*>) = f(i)

      proof

        let i be Element of NAT ;

        reconsider ij = <*i*> as Element of (1 -tuples_on NAT ) by FINSEQ_2: 131;



        thus ((1 succ 1) . <*i*>) = ((ij /. 1) + 1) by Def7

        .= (i + 1) by FINSEQ_4: 16;

      end;

      for i,j be Element of NAT holds (((1 succ 1) * <: <*(2 proj 1)*>:>) . <*i, j*>) = f(g) from Primrec1( A2, A1);

      then

       A3: for i,j be Element of NAT holds (((1 succ 1) * <: <*(2 proj 1)*>:>) . <*i, j*>) = b(i,j);



       A4: for i,j be Element of NAT holds ((2 proj 2) . <*i, j*>) = c(i,j)

      proof

        let i,j be Element of NAT ;

        reconsider ij = <*i, j*> as Element of (2 -tuples_on NAT ) by FINSEQ_2: 101;



        thus ((2 proj 2) . <*i, j*>) = (ij . 2) by Th37

        .= j by FINSEQ_1: 44;

      end;



       A5: for i,j be Element of NAT holds ( [*] . <*i, j*>) = a(i,j) by Th85;



       A6: for i,j be Element of NAT holds (g . <*i, j*>) = a(b,c) from Primrec2( A5, A3, A4);



       A7: ( arity ( 0 const 1)) = 0 by Th31;



       A8: ( arity g) = 2 by Def21;

       A9:

      now

        let i be Nat;

        reconsider i1 = i as Element of NAT by ORDINAL1:def 12;

        reconsider ie = (i ! ) as Element of NAT ;

        assume p[i];



        then ( [!] . <*(i1 + 1)*>) = (g . <*i1, ie*>) by A8, A7, Th81

        .= ((i1 + 1) * ie) by A6

        .= ((i + 1) ! ) by NEWTON: 15;

        hence p[(i + 1)];

      end;

      ( 0 -tuples_on NAT ) = { {} } by Th5;

      then

       A10: {} in ( 0 -tuples_on NAT ) by TARSKI:def 1;

      ( [!] . <* 0 *>) = (( 0 const 1) . {} ) by A7, Th79

      .= ( 0 ! ) by A10, FUNCOP_1: 7, NEWTON: 12;

      then

       A11: p[ 0 ];

      for i be Nat holds p[i] from NAT_1:sch 2( A11, A9);

      hence thesis;

    end;

    definition

      :: COMPUT_1:def26

      func [^] -> 2 -ary primitive-recursive Function equals ( primrec ((1 const 1),( (1,2)->(1,?,2) [*] ),2));

      coherence ;

    end

    theorem :: COMPUT_1:88

    ( [^] . <*i, j*>) = (i |^ j)

    proof

      defpred p[ Nat] means ( [^] . <*i, $1*>) = (i |^ $1);

       A1:

      now

        let j be Nat;

        reconsider jj = j as Element of NAT by ORDINAL1:def 12;

        reconsider ij = (i |^ jj) as Element of NAT ;

        assume p[j];



        then ( [^] . <*i, (jj + 1)*>) = (( (1,2)->(1,?,2) [*] ) . <*i, jj, ij*>) by Th80

        .= ( [*] . <*i, ij*>) by Th82

        .= (i * ij) by Th85

        .= (i |^ (j + 1)) by NEWTON: 6;

        hence p[(j + 1)];

      end;

      reconsider ii = <*i*> as Element of (1 -tuples_on NAT ) by FINSEQ_2: 131;

      ( [^] . <*i, 0 *>) = ((1 const 1) . ii) by Th78

      .= 1

      .= (i |^ 0 ) by NEWTON: 4;

      then

       A2: p[ 0 ];

      for j be Nat holds p[j] from NAT_1:sch 2( A2, A1);

      hence thesis;

    end;

    definition

      :: COMPUT_1:def27

      func [pred] -> 1 -ary primitive-recursive Function equals ( primrec (( 0 const 0 ),(2 proj 1),1));

      coherence ;

    end

    theorem :: COMPUT_1:89



     Th88: ( [pred] . <* 0 *>) = 0 & ( [pred] . <*(i + 1)*>) = i

    proof

      defpred p[ Nat] means ( [pred] . <*($1 + 1)*>) = $1;

      reconsider p0 = <* 0 , 0 *> as Element of (2 -tuples_on NAT ) by FINSEQ_2: 101;



       A2: ( arity ( 0 const 0 )) = 0 by Th31;



       A3: ( arity (2 proj 1)) = 2 by Th36;

       A4:

      now

        let i be Nat;

        reconsider i1 = i as Element of NAT by ORDINAL1:def 12;

        reconsider p0 = <*(i1 + 1), i1*> as Element of (2 -tuples_on NAT ) by FINSEQ_2: 101;

        assume p[i];



        then ( [pred] . <*((i + 1) + 1)*>) = ((2 proj 1) . p0) by A2, A3, Th81

        .= ( <*(i + 1), i*> . 1) by Th37

        .= (i + 1) by FINSEQ_1: 44;

        hence p[(i + 1)];

      end;



      thus ( [pred] . <* 0 *>) = (( 0 const 0 ) . {} ) by A2, Th79

      .= 0 ;



      then ( [pred] . <*( 0 + 1)*>) = ((2 proj 1) . p0) by A2, A3, Th81

      .= ( <* 0 , 0 *> . 1) by Th37

      .= 0 by FINSEQ_1: 44;

      then

       A5: p[ 0 ];

      for i be Nat holds p[i] from NAT_1:sch 2( A5, A4);

      hence thesis;

    end;

    definition

      :: COMPUT_1:def28

      func [-] -> 2 -ary primitive-recursive Function equals ( primrec ((1 proj 1),( (1,2)->(1,?,2) ( [pred] * <: <*(2 proj 2)*>:>)),2));

      coherence ;

    end

    theorem :: COMPUT_1:90

    ( [-] . <*i, j*>) = (i -' j)

    proof

      set F = <*(2 proj 2)*>;

      set g = ( [pred] * <:F:>);

      ( rng F) c= PrimRec

      proof

        let x be object;

        assume x in ( rng F);

        then x in {(2 proj 2)} by FINSEQ_1: 39;

        then x = (2 proj 2) by TARSKI:def 1;

        hence thesis by Def14;

      end;

      then

      reconsider F as with_the_same_arity FinSequence of PrimRec by FINSEQ_1:def 4;

      defpred p[ Nat] means ( [-] . <*i, $1*>) = (i -' $1);



       A1: for i, j holds (g . <*i, 0 *>) = 0 & (g . <*i, (j + 1)*>) = j

      proof

        let i, j;

        reconsider i0 = <*i, 0 *> as Element of (2 -tuples_on NAT ) by FINSEQ_2: 101;

        reconsider ij = <*i, (j + 1)*> as Element of (2 -tuples_on NAT ) by FINSEQ_2: 101;



         A2: ( dom (2 proj 2)) = (2 -tuples_on NAT ) by Th35;



         A3: ( dom <:F:>) = ( dom (2 proj 2)) by FINSEQ_3: 141;



        hence (g . <*i, 0 *>) = ( [pred] . ( <:F:> . i0)) by A2, FUNCT_1: 13

        .= ( [pred] . <*((2 proj 2) . i0)*>) by A2, FINSEQ_3: 141

        .= ( [pred] . <*(i0 . 2)*>) by Th37

        .= 0 by Th88, FINSEQ_1: 44;



        thus (g . <*i, (j + 1)*>) = ( [pred] . ( <:F:> . ij)) by A3, A2, FUNCT_1: 13

        .= ( [pred] . <*((2 proj 2) . ij)*>) by A2, FINSEQ_3: 141

        .= ( [pred] . <*(ij . 2)*>) by Th37

        .= ( [pred] . <*(j + 1)*>) by FINSEQ_1: 44

        .= j by Th88;

      end;

       A4:

      now

        let j be Nat;

        assume

         A5: p[j];

         A6:

        now

          per cases by NAT_1: 6;

            suppose

             A7: (i -' j) = 0 ;

            then i <= j by NAT_D: 36;

            then i < (j + 1) by NAT_1: 13;

            then

             A8: (i - (j + 1)) < 0 by XREAL_1: 49;



            thus (g . <*i, (i -' j)*>) = 0 by A1, A7

            .= (i -' (j + 1)) by A8, XREAL_0:def 2;

          end;

            suppose ex k be Nat st (i -' j) = (k + 1);

            then

            consider k be Nat such that

             A9: (i -' j) = (k + 1);

            reconsider k as Element of NAT by ORDINAL1:def 12;

            (i - j) = (k + 1) by A9, XREAL_0:def 2;

            then

             A10: (i - (j + 1)) = k;



            thus (g . <*i, (i -' j)*>) = k by A1, A9

            .= (i -' (j + 1)) by A10, XREAL_0:def 2;

          end;

        end;

        reconsider jj = j as Element of NAT by ORDINAL1:def 12;

        ( [-] . <*i, (jj + 1)*>) = (( (1,2)->(1,?,2) g) . <*i, jj, ( [-] . <*i, jj*>)*>) by Th80

        .= (i -' (jj + 1)) by A5, A6, Th82;

        hence p[(j + 1)];

      end;

      reconsider ii = <*i*> as Element of (1 -tuples_on NAT ) by FINSEQ_2: 98;

      ( [-] . <*i, 0 *>) = ((1 proj 1) . <*i*>) by Th78

      .= (ii . 1) by Th37

      .= i by FINSEQ_1: 40

      .= ((i + 0 ) -' 0 ) by NAT_D: 34

      .= (i -' 0 );

      then

       A11: p[ 0 ];

      for j be Nat holds p[j] from NAT_1:sch 2( A11, A4);

      hence thesis;

    end;