:: The set of primitive recursive functions
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Copyright (c) 2001-2019 Association of Mizar Users

theorem Th1: :: COMPUT_1:1
for x, y, z being set holds
( <*x,y*> +* (1,z) = <*z,y*> & <*x,y*> +* (2,z) = <*x,z*> )
proof end;

theorem Th2: :: COMPUT_1:2
for a, x, y, z being set
for f, g being Function st f +* (a,x) = g +* (a,y) holds
f +* (a,z) = g +* (a,z)
proof end;

theorem Th3: :: COMPUT_1:3
for x being set
for p being FinSequence
for i being Nat holds Del ((p +* (i,x)),i) = Del (p,i)
proof end;

theorem Th4: :: COMPUT_1:4
for i being Element of NAT
for a being set
for p, q being FinSequence st p +* (i,a) = q +* (i,a) holds
Del (p,i) = Del (q,i)
proof end;

theorem Th5: :: COMPUT_1:5
for X being set holds 0 -tuples_on X =
proof end;

theorem :: COMPUT_1:6
for n being Element of NAT st n <> 0 holds
n -tuples_on {} = {}
proof end;

theorem Th7: :: COMPUT_1:7
for f being Function-yielding Function st {} in rng f holds
<:f:> = {}
proof end;

theorem Th8: :: COMPUT_1:8
for D being non empty set
for f being Function st rng f = D holds
rng = 1 -tuples_on D
proof end;

theorem Th9: :: COMPUT_1:9
for i, n being Element of NAT
for D being non empty set st 1 <= i & i <= n + 1 holds
for p being Element of (n + 1) -tuples_on D holds Del (p,i) in n -tuples_on D
proof end;

definition
let X be set ;
attr X is compatible means :Def1: :: COMPUT_1:def 1
for f, g being Function st f in X & g in X holds
f tolerates g;
end;

:: deftheorem Def1 defines compatible COMPUT_1:def 1 :
for X being set holds
( X is compatible iff for f, g being Function st f in X & g in X holds
f tolerates g );

registration
existence
ex b1 being set st
( not b1 is empty & b1 is functional & b1 is compatible )
proof end;
end;

registration
let X be functional compatible set ;
coherence
( union X is Function-like & union X is Relation-like )
proof end;
end;

theorem :: COMPUT_1:10
canceled;

::$CT theorem Th10: :: COMPUT_1:11 for X being set holds ( ( X is functional & X is compatible ) iff union X is Function ) proof end; registration let X, Y be set ; cluster non empty compatible for PartFunc-set of X,Y; existence ex b1 being PFUNC_DOMAIN of X,Y st ( not b1 is empty & b1 is compatible ) proof end; end; theorem Th11: :: COMPUT_1:12 for X being non empty functional compatible set holds dom () = union { (dom f) where f is Element of X : verum } proof end; theorem Th12: :: COMPUT_1:13 for X being functional compatible set for f being Function st f in X holds ( dom f c= dom () & ( for x being set st x in dom f holds () . x = f . x ) ) proof end; theorem Th13: :: COMPUT_1:14 for X being non empty functional compatible set holds rng () = union { (rng f) where f is Element of X : verum } proof end; registration let X, Y be set ; cluster non empty -> functional for PartFunc-set of X,Y; coherence for b1 being PFUNC_DOMAIN of X,Y holds b1 is functional by RFUNCT_3:def 3; end; theorem Th14: :: COMPUT_1:15 for X, Y being set for P being compatible PFUNC_DOMAIN of X,Y holds union P is PartFunc of X,Y proof end; notation let f be Relation; synonym to-naturals f for natural-valued ; end; registration existence ex b1 being Function st ( b1 is NAT * -defined & b1 is to-naturals ) proof end; end; definition let f be NAT * -defined Relation; attr f is len-total means :Def2: :: COMPUT_1:def 2 for x, y being FinSequence of NAT st len x = len y & x in dom f holds y in dom f; end; :: deftheorem Def2 defines len-total COMPUT_1:def 2 : for f being NAT * -defined Relation holds ( f is len-total iff for x, y being FinSequence of NAT st len x = len y & x in dom f holds y in dom f ); theorem Th15: :: COMPUT_1:16 for n being Element of NAT for D being non empty set for R being Relation st dom R c= n -tuples_on D holds R is homogeneous ; registration coherence for b1 being Relation st b1 is empty holds b1 is homogeneous ; end; registration let p be FinSequence; let x be set ; cluster p .--> x -> non empty homogeneous ; coherence ( not p .--> x is empty & p .--> x is homogeneous ) proof end; end; registration existence ex b1 being Function st ( not b1 is empty & b1 is homogeneous ) proof end; end; registration let f be homogeneous Function; let g be Function; cluster f * g -> homogeneous ; coherence g * f is homogeneous proof end; end; registration let X, Y be set ; existence ex b1 being PartFunc of (X *),Y st b1 is homogeneous proof end; end; registration let X, Y be non empty set ; cluster non empty Relation-like X * -defined Y -valued Function-like homogeneous for Element of K32(K33((X *),Y)); existence ex b1 being PartFunc of (X *),Y st ( not b1 is empty & b1 is homogeneous ) proof end; end; registration let X be non empty set ; existence ex b1 being PartFunc of (X *),X st ( not b1 is empty & b1 is homogeneous & b1 is quasi_total ) proof end; end; registration existence ex b1 being NAT * -defined Function st ( not b1 is empty & b1 is homogeneous & b1 is to-naturals & b1 is len-total ) proof end; end; registration cluster Function-like -> NAT * -defined to-naturals for Element of K32(K33((),NAT)); coherence for b1 being PartFunc of (),NAT holds ( b1 is to-naturals & b1 is NAT * -defined ) ; end; registration cluster Function-like quasi_total -> len-total for Element of K32(K33((),NAT)); coherence for b1 being PartFunc of (),NAT st b1 is quasi_total holds b1 is len-total ; end; theorem Th16: :: COMPUT_1:17 for g being NAT * -defined to-naturals len-total Function holds g is quasi_total PartFunc of (),NAT proof end; theorem Th17: :: COMPUT_1:18 proof end; theorem Th18: :: COMPUT_1:19 for f being homogeneous Relation st dom f = holds arity f = 0 proof end; theorem Th19: :: COMPUT_1:20 for X, Y being set for f being homogeneous PartFunc of (X *),Y holds dom f c= () -tuples_on X proof end; theorem Th20: :: COMPUT_1:21 for f being NAT * -defined homogeneous Function holds dom f c= () -tuples_on NAT proof end; Lm1: for D being non empty set for f being homogeneous PartFunc of (D *),D holds ( ( f is quasi_total & not f is empty ) iff dom f = () -tuples_on D ) proof end; theorem Th21: :: COMPUT_1:22 for X being set for f being homogeneous PartFunc of (X *),X holds ( ( f is quasi_total & not f is empty ) iff dom f = () -tuples_on X ) proof end; theorem Th22: :: COMPUT_1:23 for f being NAT * -defined to-naturals homogeneous Function holds ( ( f is len-total & not f is empty ) iff dom f = () -tuples_on NAT ) proof end; theorem :: COMPUT_1:24 for D being non empty set for f being non empty homogeneous PartFunc of (D *),D for n being Element of NAT st dom f c= n -tuples_on D holds arity f = n proof end; theorem Th24: :: COMPUT_1:25 for D being non empty set for f being homogeneous PartFunc of (D *),D for n being Element of NAT st dom f = n -tuples_on D holds arity f = n proof end; definition let R be Relation; attr R is with_the_same_arity means :Def3: :: COMPUT_1:def 3 for f, g being Function st f in rng R & g in rng R holds ( ( not f is empty or g is empty or dom g = ) & ( not f is empty & not g is empty implies ex n being Element of NAT ex X being non empty set st ( dom f c= n -tuples_on X & dom g c= n -tuples_on X ) ) ); end; :: deftheorem Def3 defines with_the_same_arity COMPUT_1:def 3 : for R being Relation holds ( R is with_the_same_arity iff for f, g being Function st f in rng R & g in rng R holds ( ( not f is empty or g is empty or dom g = ) & ( not f is empty & not g is empty implies ex n being Element of NAT ex X being non empty set st ( dom f c= n -tuples_on X & dom g c= n -tuples_on X ) ) ) ); registration coherence for b1 being Relation st b1 is empty holds b1 is with_the_same_arity ; end; registration let X be set ; existence ex b1 being FinSequence of X st b1 is with_the_same_arity proof end; existence ex b1 being Element of X * st b1 is with_the_same_arity proof end; end; definition let F be with_the_same_arity Relation; func arity F -> Element of NAT means :Def4: :: COMPUT_1:def 4 for f being homogeneous Function st f in rng F holds it = arity f if ex f being homogeneous Function st f in rng F otherwise it = 0 ; existence ( ( ex f being homogeneous Function st f in rng F implies ex b1 being Element of NAT st for f being homogeneous Function st f in rng F holds b1 = arity f ) & ( ( for f being homogeneous Function holds not f in rng F ) implies ex b1 being Element of NAT st b1 = 0 ) ) proof end; uniqueness for b1, b2 being Element of NAT holds ( ( ex f being homogeneous Function st f in rng F & ( for f being homogeneous Function st f in rng F holds b1 = arity f ) & ( for f being homogeneous Function st f in rng F holds b2 = arity f ) implies b1 = b2 ) & ( ( for f being homogeneous Function holds not f in rng F ) & b1 = 0 & b2 = 0 implies b1 = b2 ) ) proof end; correctness consistency for b1 being Element of NAT holds verum ; ; end; :: deftheorem Def4 defines arity COMPUT_1:def 4 : for F being with_the_same_arity Relation for b2 being Element of NAT holds ( ( ex f being homogeneous Function st f in rng F implies ( b2 = arity F iff for f being homogeneous Function st f in rng F holds b2 = arity f ) ) & ( ( for f being homogeneous Function holds not f in rng F ) implies ( b2 = arity F iff b2 = 0 ) ) ); theorem :: COMPUT_1:26 for F being with_the_same_arity FinSequence st len F = 0 holds arity F = 0 proof end; definition let X be set ; func HFuncs X -> PFUNC_DOMAIN of X * ,X equals :: COMPUT_1:def 5 { f where f is Element of PFuncs ((X *),X) : f is homogeneous } ; coherence { f where f is Element of PFuncs ((X *),X) : f is homogeneous } is PFUNC_DOMAIN of X * ,X proof end; end; :: deftheorem defines HFuncs COMPUT_1:def 5 : for X being set holds HFuncs X = { f where f is Element of PFuncs ((X *),X) : f is homogeneous } ; theorem :: COMPUT_1:27 for X being set holds {} in HFuncs X proof end; registration let X be non empty set ; existence ex b1 being Element of HFuncs X st ( not b1 is empty & b1 is homogeneous & b1 is quasi_total ) proof end; end; registration let X be set ; cluster -> homogeneous for Element of HFuncs X; coherence for b1 being Element of HFuncs X holds b1 is homogeneous proof end; end; registration let X be non empty set ; let S be non empty Subset of (); cluster -> homogeneous for Element of S; coherence for b1 being Element of S holds b1 is homogeneous ; end; theorem Th27: :: COMPUT_1:28 for f being NAT * -defined to-naturals homogeneous Function holds f is Element of HFuncs NAT proof end; theorem Th28: :: COMPUT_1:29 proof end; theorem Th29: :: COMPUT_1:30 for X being non empty set for F being Relation st rng F c= HFuncs X & ( for f, g being homogeneous Function st f in rng F & g in rng F holds arity f = arity g ) holds F is with_the_same_arity proof end; definition let n, m be Nat; coherence proof end; end; :: deftheorem defines const COMPUT_1:def 6 : for n, m being Nat holds n const m = () --> m; theorem Th30: :: COMPUT_1:31 for m, n being Element of NAT holds n const m in HFuncs NAT proof end; registration let n, m be Element of NAT ; coherence ( n const m is len-total & not n const m is empty ) proof end; end; theorem Th31: :: COMPUT_1:32 for m, n being Element of NAT holds arity (n const m) = n proof end; registration coherence for b1 being Element of HFuncs NAT holds ( b1 is homogeneous & b1 is to-naturals & b1 is NAT * -defined ) ; end; definition let n, i be Element of NAT ; func n succ i -> NAT * -defined to-naturals homogeneous Function means :Def7: :: COMPUT_1:def 7 ( dom it = n -tuples_on NAT & ( for p being Element of n -tuples_on NAT holds it . p = (p /. i) + 1 ) ); existence ex b1 being NAT * -defined to-naturals homogeneous Function st ( dom b1 = n -tuples_on NAT & ( for p being Element of n -tuples_on NAT holds b1 . p = (p /. i) + 1 ) ) proof end; uniqueness for b1, b2 being NAT * -defined to-naturals homogeneous Function st dom b1 = n -tuples_on NAT & ( for p being Element of n -tuples_on NAT holds b1 . p = (p /. i) + 1 ) & dom b2 = n -tuples_on NAT & ( for p being Element of n -tuples_on NAT holds b2 . p = (p /. i) + 1 ) holds b1 = b2 proof end; end; :: deftheorem Def7 defines succ COMPUT_1:def 7 : for n, i being Element of NAT for b3 being NAT * -defined to-naturals homogeneous Function holds ( b3 = n succ i iff ( dom b3 = n -tuples_on NAT & ( for p being Element of n -tuples_on NAT holds b3 . p = (p /. i) + 1 ) ) ); theorem Th32: :: COMPUT_1:33 for i, n being Element of NAT holds n succ i in HFuncs NAT proof end; registration let n, i be Element of NAT ; coherence ( n succ i is len-total & not n succ i is empty ) proof end; end; theorem Th33: :: COMPUT_1:34 for i, n being Element of NAT holds arity (n succ i) = n proof end; definition let n, i be Nat; func n proj i -> NAT * -defined to-naturals homogeneous Function equals :: COMPUT_1:def 8 proj ((),i); correctness coherence ; proof end; end; :: deftheorem defines proj COMPUT_1:def 8 : for n, i being Nat holds n proj i = proj ((),i); theorem Th34: :: COMPUT_1:35 for i, n being Element of NAT holds n proj i in HFuncs NAT proof end; theorem Th35: :: COMPUT_1:36 for i, n being Element of NAT holds ( dom (n proj i) = n -tuples_on NAT & ( 1 <= i & i <= n implies rng (n proj i) = NAT ) ) proof end; registration let n, i be Element of NAT ; coherence ( n proj i is len-total & not n proj i is empty ) proof end; end; theorem Th36: :: COMPUT_1:37 for i, n being Element of NAT holds arity (n proj i) = n proof end; theorem Th37: :: COMPUT_1:38 for i, n being Element of NAT for t being Element of n -tuples_on NAT holds (n proj i) . t = t . i proof end; registration let X be set ; coherence ; end; theorem Th38: :: COMPUT_1:39 for n being Element of NAT for D, E being non empty set for F being Function of D,() st rng F is compatible & ( for x being Element of D holds dom (F . x) c= n -tuples_on E ) holds ex f being Element of HFuncs E st ( f = Union F & dom f c= n -tuples_on E ) proof end; theorem :: COMPUT_1:40 for D being non empty set for F being sequence of () st ( for i being Nat holds F . i c= F . (i + 1) ) holds Union F in HFuncs D proof end; theorem Th40: :: COMPUT_1:41 for D being non empty set for F being with_the_same_arity FinSequence of HFuncs D holds dom <:F:> c= () -tuples_on D proof end; registration let X be non empty set ; let F be with_the_same_arity FinSequence of HFuncs X; coherence proof end; end; theorem Th41: :: COMPUT_1:42 for D being non empty set for f being Element of HFuncs D for F being with_the_same_arity FinSequence of HFuncs D holds ( dom (f * <:F:>) c= () -tuples_on D & rng (f * <:F:>) c= D & f * <:F:> in HFuncs D ) proof end; definition let X, Y be non empty set ; let 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 for b1 being Element of S holds b1 is Element of P proof end; end; registration let f be NAT * -defined homogeneous Function; coherence proof end; end; theorem :: COMPUT_1:43 for f being NAT * -defined to-naturals homogeneous Function holds arity <*f*> = arity f proof end; theorem Th43: :: COMPUT_1:44 for f, g being non empty Element of HFuncs NAT for F being with_the_same_arity FinSequence of HFuncs NAT st g = f * <:F:> holds arity g = arity F proof end; theorem Th44: :: COMPUT_1:45 for D being non empty set for f being non empty quasi_total Element of HFuncs D for F being with_the_same_arity FinSequence of HFuncs D st arity f = len F & not F is empty & ( for h being Element of HFuncs D st h in rng F holds ( h is quasi_total & not h is empty ) ) holds ( f * <:F:> is non empty quasi_total Element of HFuncs D & dom (f * <:F:>) = () -tuples_on D ) proof end; theorem Th45: :: COMPUT_1:46 for D being non empty set for f being quasi_total Element of HFuncs D for F being with_the_same_arity FinSequence of HFuncs D st arity f = len F & ( for h being 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 end; theorem Th46: :: COMPUT_1:47 for D being non empty set for f, g being non empty quasi_total Element of HFuncs D st arity f = 0 & arity g = 0 & f . {} = g . {} holds f = g proof end; theorem Th47: :: COMPUT_1:48 for f, g being non empty NAT * -defined to-naturals homogeneous len-total Function st arity f = 0 & arity g = 0 & f . {} = g . {} holds f = g proof end; definition let g, f1, f2 be NAT * -defined to-naturals homogeneous Function; let i be Element of NAT ; pred g is_primitive-recursively_expressed_by f1,f2,i means :: COMPUT_1:def 9 ex n being 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 being FinSequence of NAT st len p = n holds ( ( p +* (i,0) in dom g implies Del (p,i) in dom f1 ) & ( Del (p,i) in dom f1 implies p +* (i,0) in dom g ) & ( p +* (i,0) in dom g implies g . (p +* (i,0)) = f1 . (Del (p,i)) ) & ( for n being Nat holds ( ( p +* (i,(n + 1)) in dom g implies ( p +* (i,n) in dom g & (p +* (i,n)) ^ <*(g . (p +* (i,n)))*> in dom f2 ) ) & ( p +* (i,n) in dom g & (p +* (i,n)) ^ <*(g . (p +* (i,n)))*> in dom f2 implies p +* (i,(n + 1)) in dom g ) & ( p +* (i,(n + 1)) in dom g implies g . (p +* (i,(n + 1))) = f2 . ((p +* (i,n)) ^ <*(g . (p +* (i,n)))*>) ) ) ) ) ) ); end; :: deftheorem defines is_primitive-recursively_expressed_by COMPUT_1:def 9 : for g, f1, f2 being NAT * -defined to-naturals homogeneous Function for i being Element of NAT holds ( g is_primitive-recursively_expressed_by f1,f2,i iff ex n being 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 being FinSequence of NAT st len p = n holds ( ( p +* (i,0) in dom g implies Del (p,i) in dom f1 ) & ( Del (p,i) in dom f1 implies p +* (i,0) in dom g ) & ( p +* (i,0) in dom g implies g . (p +* (i,0)) = f1 . (Del (p,i)) ) & ( for n being Nat holds ( ( p +* (i,(n + 1)) in dom g implies ( p +* (i,n) in dom g & (p +* (i,n)) ^ <*(g . (p +* (i,n)))*> in dom f2 ) ) & ( p +* (i,n) in dom g & (p +* (i,n)) ^ <*(g . (p +* (i,n)))*> in dom f2 implies p +* (i,(n + 1)) in dom g ) & ( p +* (i,(n + 1)) in dom g implies g . (p +* (i,(n + 1))) = f2 . ((p +* (i,n)) ^ <*(g . (p +* (i,n)))*>) ) ) ) ) ) ) ); defpred S1[ 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 NAT * -defined to-naturals homogeneous Function;
let i be Nat;
let p be FinSequence of NAT ;
func primrec (f1,f2,i,p) -> Element of HFuncs NAT means :Def10: :: COMPUT_1:def 10
ex F being sequence of () 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 being 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
ex b1 being Element of HFuncs NAT ex F being sequence of () st
( b1 = 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 being 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 ) ) ) )
proof end;
uniqueness
for b1, b2 being Element of HFuncs NAT st ex F being sequence of () st
( b1 = 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 being 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 ) ) ) ) & ex F being sequence of () st
( b2 = 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 being 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 ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines primrec COMPUT_1:def 10 :
for f1, f2 being NAT * -defined to-naturals homogeneous Function
for i being Nat
for p being FinSequence of NAT
for b5 being Element of HFuncs NAT holds
( b5 = primrec (f1,f2,i,p) iff ex F being sequence of () st
( b5 = 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 being 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 ) ) ) ) );

theorem Th48: :: COMPUT_1:49
for e1, e2 being NAT * -defined to-naturals homogeneous Function
for i being Nat
for p, q being FinSequence of NAT st q in dom (primrec (e1,e2,i,p)) holds
ex k being Element of NAT st q = p +* (i,k)
proof end;

theorem Th49: :: COMPUT_1:50
for e1, e2 being NAT * -defined to-naturals homogeneous Function
for i being Nat
for p being FinSequence of NAT st not i in dom p holds
primrec (e1,e2,i,p) = {}
proof end;

theorem Th50: :: COMPUT_1:51
for e1, e2 being NAT * -defined to-naturals homogeneous Function
for i being Nat
for p, q being FinSequence of NAT holds primrec (e1,e2,i,p) tolerates primrec (e1,e2,i,q)
proof end;

theorem Th51: :: COMPUT_1:52
for e1, e2 being NAT * -defined to-naturals homogeneous Function
for i being Nat
for p being FinSequence of NAT holds dom (primrec (e1,e2,i,p)) c= (1 + (arity e1)) -tuples_on NAT
proof end;

theorem Th52: :: COMPUT_1:53
for i being Element of NAT
for e1, e2 being NAT * -defined to-naturals homogeneous Function
for p being FinSequence of NAT st e1 is empty holds
primrec (e1,e2,i,p) is empty
proof end;

theorem Th53: :: COMPUT_1:54
for i being Element of NAT
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st f1 is len-total & f2 is len-total & (arity f1) + 2 = arity f2 & 1 <= i & i <= 1 + (arity f1) holds
p in dom (primrec (f1,f2,i,p))
proof end;

definition
let f1, f2 be NAT * -defined to-naturals homogeneous Function;
let i be Nat;
func primrec (f1,f2,i) -> Element of HFuncs NAT means :Def11: :: COMPUT_1:def 11
ex G being Function of (((arity f1) + 1) -tuples_on NAT),() st
( it = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) );
existence
ex b1 being Element of HFuncs NAT ex G being Function of (((arity f1) + 1) -tuples_on NAT),() st
( b1 = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) )
proof end;
uniqueness
for b1, b2 being Element of HFuncs NAT st ex G being Function of (((arity f1) + 1) -tuples_on NAT),() st
( b1 = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) ) & ex G being Function of (((arity f1) + 1) -tuples_on NAT),() st
( b2 = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines primrec COMPUT_1:def 11 :
for f1, f2 being NAT * -defined to-naturals homogeneous Function
for i being Nat
for b4 being Element of HFuncs NAT holds
( b4 = primrec (f1,f2,i) iff ex G being Function of (((arity f1) + 1) -tuples_on NAT),() st
( b4 = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) ) );

theorem Th54: :: COMPUT_1:55
for i being Element of NAT
for e1, e2 being NAT * -defined to-naturals homogeneous Function st e1 is empty holds
primrec (e1,e2,i) is empty
proof end;

theorem Th55: :: COMPUT_1:56
for i being Element of NAT
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function holds dom (primrec (f1,f2,i)) c= ((arity f1) + 1) -tuples_on NAT
proof end;

theorem Th56: :: COMPUT_1:57
for i being Element of NAT
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function st f1 is len-total & f2 is len-total & (arity f1) + 2 = arity f2 & 1 <= i & i <= 1 + (arity f1) holds
( dom (primrec (f1,f2,i)) = ((arity f1) + 1) -tuples_on NAT & arity (primrec (f1,f2,i)) = (arity f1) + 1 )
proof end;

Lm2: now :: thesis: for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT
for i being Nat
for m being Element of NAT
for F1, F being sequence of () st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F1 . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F1 . 0 = {} ) & ( for M being Nat holds S1[M,F1 . M,F1 . (M + 1),p +* (i,(m + 1)),i,f2] ) & ( i in dom (p +* (i,m)) & Del ((p +* (i,m)),i) in dom f1 implies F . 0 = {((p +* (i,m)) +* (i,0))} --> (f1 . (Del ((p +* (i,m)),i))) ) & ( ( not i in dom (p +* (i,m)) or not Del ((p +* (i,m)),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* (i,m),i,f2] ) holds
F1 = F
let f1, f2 be non empty NAT * -defined to-naturals homogeneous Function; :: thesis: for p being Element of ((arity f1) + 1) -tuples_on NAT
for i being Nat
for m being Element of NAT
for F1, F being sequence of () st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F1 . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F1 . 0 = {} ) & ( for M being Nat holds S1[M,F1 . M,F1 . (M + 1),p +* (i,(m + 1)),i,f2] ) & ( i in dom (p +* (i,m)) & Del ((p +* (i,m)),i) in dom f1 implies F . 0 = {((p +* (i,m)) +* (i,0))} --> (f1 . (Del ((p +* (i,m)),i))) ) & ( ( not i in dom (p +* (i,m)) or not Del ((p +* (i,m)),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* (i,m),i,f2] ) holds
F1 = F

let p be Element of ((arity f1) + 1) -tuples_on NAT; :: thesis: for i being Nat
for m being Element of NAT
for F1, F being sequence of () st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F1 . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F1 . 0 = {} ) & ( for M being Nat holds S1[M,F1 . M,F1 . (M + 1),p +* (i,(m + 1)),i,f2] ) & ( i in dom (p +* (i,m)) & Del ((p +* (i,m)),i) in dom f1 implies F . 0 = {((p +* (i,m)) +* (i,0))} --> (f1 . (Del ((p +* (i,m)),i))) ) & ( ( not i in dom (p +* (i,m)) or not Del ((p +* (i,m)),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* (i,m),i,f2] ) holds
F1 = F

let i be Nat; :: thesis: for m being Element of NAT
for F1, F being sequence of () st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F1 . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F1 . 0 = {} ) & ( for M being Nat holds S1[M,F1 . M,F1 . (M + 1),p +* (i,(m + 1)),i,f2] ) & ( i in dom (p +* (i,m)) & Del ((p +* (i,m)),i) in dom f1 implies F . 0 = {((p +* (i,m)) +* (i,0))} --> (f1 . (Del ((p +* (i,m)),i))) ) & ( ( not i in dom (p +* (i,m)) or not Del ((p +* (i,m)),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* (i,m),i,f2] ) holds
F1 = F

let m be Element of NAT ; :: thesis: for F1, F being sequence of () st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F1 . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F1 . 0 = {} ) & ( for M being Nat holds S1[M,F1 . M,F1 . (M + 1),p +* (i,(m + 1)),i,f2] ) & ( i in dom (p +* (i,m)) & Del ((p +* (i,m)),i) in dom f1 implies F . 0 = {((p +* (i,m)) +* (i,0))} --> (f1 . (Del ((p +* (i,m)),i))) ) & ( ( not i in dom (p +* (i,m)) or not Del ((p +* (i,m)),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* (i,m),i,f2] ) holds
F1 = F

set pm1 = p +* (i,(m + 1));
set pm = p +* (i,m);
let F1, F be sequence of (); :: thesis: ( ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F1 . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F1 . 0 = {} ) & ( for M being Nat holds S1[M,F1 . M,F1 . (M + 1),p +* (i,(m + 1)),i,f2] ) & ( i in dom (p +* (i,m)) & Del ((p +* (i,m)),i) in dom f1 implies F . 0 = {((p +* (i,m)) +* (i,0))} --> (f1 . (Del ((p +* (i,m)),i))) ) & ( ( not i in dom (p +* (i,m)) or not Del ((p +* (i,m)),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* (i,m),i,f2] ) implies F1 = F )
assume that
A1: ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F1 . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) and
A2: ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F1 . 0 = {} ) and
A3: for M being Nat holds S1[M,F1 . M,F1 . (M + 1),p +* (i,(m + 1)),i,f2] and
A4: ( i in dom (p +* (i,m)) & Del ((p +* (i,m)),i) in dom f1 implies F . 0 = {((p +* (i,m)) +* (i,0))} --> (f1 . (Del ((p +* (i,m)),i))) ) and
A5: ( ( not i in dom (p +* (i,m)) or not Del ((p +* (i,m)),i) in dom f1 ) implies F . 0 = {} ) and
A6: for M being Nat holds S1[M,F . M,F . (M + 1),p +* (i,m),i,f2] ; :: thesis: F1 = F
A7: dom p = dom (p +* (i,m)) by FUNCT_7:30;
A8: (p +* (i,m)) +* (i,0) = p +* (i,0) by FUNCT_7:34
.= (p +* (i,(m + 1))) +* (i,0) by FUNCT_7:34 ;
A9: dom p = dom (p +* (i,(m + 1))) by FUNCT_7:30;
A10: Del ((p +* (i,m)),i) = Del (p,i) by Th3
.= Del ((p +* (i,(m + 1))),i) by Th3 ;
for x being object st x in NAT holds
F . x = F1 . x
proof
let x be object ; :: thesis: ( x in NAT implies F . x = F1 . x )
defpred S2[ Nat] means F . $1 = F1 .$1;
A11: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A12: S2[k] ; :: thesis: S2[k + 1]
A13: (p +* (i,m)) +* (i,(k + 1)) = p +* (i,(k + 1)) by FUNCT_7:34
.= (p +* (i,(m + 1))) +* (i,(k + 1)) by FUNCT_7:34 ;
A14: (p +* (i,m)) +* (i,k) = p +* (i,k) by FUNCT_7:34
.= (p +* (i,(m + 1))) +* (i,k) by FUNCT_7:34 ;
per cases ( ( i in dom (p +* (i,m)) & (p +* (i,m)) +* (i,k) in dom (F . k) & ((p +* (i,m)) +* (i,k)) ^ <*((F . k) . ((p +* (i,m)) +* (i,k)))*> in dom f2 ) or not i in dom (p +* (i,m)) or not (p +* (i,m)) +* (i,k) in dom (F . k) or not ((p +* (i,m)) +* (i,k)) ^ <*((F . k) . ((p +* (i,m)) +* (i,k)))*> in dom f2 ) ;
suppose A15: ( i in dom (p +* (i,m)) & (p +* (i,m)) +* (i,k) in dom (F . k) & ((p +* (i,m)) +* (i,k)) ^ <*((F . k) . ((p +* (i,m)) +* (i,k)))*> in dom f2 ) ; :: thesis: S2[k + 1]
hence F . (k + 1) = (F . k) +* (((p +* (i,m)) +* (i,(k + 1))) .--> (f2 . (((p +* (i,m)) +* (i,k)) ^ <*((F . k) . ((p +* (i,m)) +* (i,k)))*>))) by A6
.= F1 . (k + 1) by A3, A7, A9, A12, A14, A13, A15 ;
:: thesis: verum
end;
suppose A16: ( not i in dom (p +* (i,m)) or not (p +* (i,m)) +* (i,k) in dom (F . k) or not ((p +* (i,m)) +* (i,k)) ^ <*((F . k) . ((p +* (i,m)) +* (i,k)))*> in dom f2 ) ; :: thesis: S2[k + 1]
hence F . (k + 1) = F . k by A6
.= F1 . (k + 1) by A3, A7, A9, A12, A14, A16 ;
:: thesis: verum
end;
end;
end;
A17: S2[ 0 ] by A1, A2, A4, A5, A7, A8, A10, FUNCT_7:30;
A18: for k being Nat holds S2[k] from assume x in NAT ; :: thesis: F . x = F1 . x
hence F . x = F1 . x by A18; :: thesis: verum
end;
hence F1 = F by FUNCT_2:12; :: thesis: verum
end;

Lm3: now :: thesis: for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT
for i, m being Element of NAT st i in dom p holds
for F being sequence of () st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* (i,(m + 1)),i,f2] ) holds
( (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m)) & not p +* (i,(m + 1)) in dom (F . m) )
let f1, f2 be non empty NAT * -defined to-naturals homogeneous Function; :: thesis: for p being Element of ((arity f1) + 1) -tuples_on NAT
for i, m being Element of NAT st i in dom p holds
for F being sequence of () st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* (i,(m + 1)),i,f2] ) holds
( (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m)) & not p +* (i,(m + 1)) in dom (F . m) )

let p be Element of ((arity f1) + 1) -tuples_on NAT; :: thesis: for i, m being Element of NAT st i in dom p holds
for F being sequence of () st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* (i,(m + 1)),i,f2] ) holds
( (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m)) & not p +* (i,(m + 1)) in dom (F . m) )

let i, m be Element of NAT ; :: thesis: ( i in dom p implies for F being sequence of () st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* (i,(m + 1)),i,f2] ) holds
( (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m)) & not p +* (i,(m + 1)) in dom (F . m) ) )

assume A1: i in dom p ; :: thesis: for F being sequence of () st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* (i,(m + 1)),i,f2] ) holds
( (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m)) & not p +* (i,(m + 1)) in dom (F . m) )

set pm = p +* (i,m);
set pm1 = p +* (i,(m + 1));
let F be sequence of (); :: thesis: ( ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* (i,(m + 1)),i,f2] ) implies ( (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m)) & not p +* (i,(m + 1)) in dom (F . m) ) )
assume that
A2: ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) and
A3: ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F . 0 = {} ) and
A4: for M being Nat holds S1[M,F . M,F . (M + 1),p +* (i,(m + 1)),i,f2] ; :: thesis: ( (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m)) & not p +* (i,(m + 1)) in dom (F . m) )
thus (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m)) :: thesis: not p +* (i,(m + 1)) in dom (F . m)
proof
per cases ( ( i in dom (p +* (i,(m + 1))) & (p +* (i,(m + 1))) +* (i,m) in dom (F . m) & ((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 ) or not i in dom (p +* (i,(m + 1))) or not (p +* (i,(m + 1))) +* (i,m) in dom (F . m) or not ((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 ) ;
suppose A5: ( i in dom (p +* (i,(m + 1))) & (p +* (i,(m + 1))) +* (i,m) in dom (F . m) & ((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 ) ; :: thesis: (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m))
A6: p +* (i,(m + 1)) = (p +* (i,(m + 1))) +* (i,(m + 1)) by FUNCT_7:34;
A7: (p +* (i,(m + 1))) . i = m + 1 by ;
(p +* (i,m)) . i = m by ;
then p +* (i,m) <> p +* (i,(m + 1)) by A7;
then A8: not p +* (i,m) in dom ({((p +* (i,(m + 1))) +* (i,(m + 1)))} --> (f2 . (((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*>))) by ;
F . (m + 1) = (F . m) +* (((p +* (i,(m + 1))) +* (i,(m + 1))) .--> (f2 . (((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*>))) by A4, A5;
hence (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m)) by ; :: thesis: verum
end;
suppose ( not i in dom (p +* (i,(m + 1))) or not (p +* (i,(m + 1))) +* (i,m) in dom (F . m) or not ((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 ) ; :: thesis: (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m))
hence (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m)) by A4; :: thesis: verum
end;
end;
end;
A9: for m, k being Nat st p +* (i,k) in dom (F . m) holds
k <= m
proof
defpred S2[ Nat] means for k being Nat st p +* (i,k) in dom (F . $1) holds k <=$1;
A10: for m being Nat st S2[m] holds
S2[m + 1]
proof
let m be Nat; :: thesis: ( S2[m] implies S2[m + 1] )
assume A11: S2[m] ; :: thesis: S2[m + 1]
let k be Nat; :: thesis: ( p +* (i,k) in dom (F . (m + 1)) implies k <= m + 1 )
assume A12: p +* (i,k) in dom (F . (m + 1)) ; :: thesis: k <= m + 1
per cases ( ( i in dom (p +* (i,(m + 1))) & (p +* (i,(m + 1))) +* (i,m) in dom (F . m) & ((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 ) or not i in dom (p +* (i,(m + 1))) or not (p +* (i,(m + 1))) +* (i,m) in dom (F . m) or not ((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 ) ;
suppose ( i in dom (p +* (i,(m + 1))) & (p +* (i,(m + 1))) +* (i,m) in dom (F . m) & ((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 ) ; :: thesis: k <= m + 1
then F . (m + 1) = (F . m) +* (((p +* (i,(m + 1))) +* (i,(m + 1))) .--> (f2 . (((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*>))) by A4;
then dom (F . (m + 1)) = (dom (F . m)) \/ (dom ({((p +* (i,(m + 1))) +* (i,(m + 1)))} --> (f2 . (((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*>)))) by FUNCT_4:def 1;
then A13: dom (F . (m + 1)) = (dom (F . m)) \/ {((p +* (i,(m + 1))) +* (i,(m + 1)))} ;
thus k <= m + 1 :: thesis: verum
proof
per cases ( p +* (i,k) in dom (F . m) or p +* (i,k) in {((p +* (i,(m + 1))) +* (i,(m + 1)))} ) by ;
suppose A14: p +* (i,k) in dom (F . m) ; :: thesis: k <= m + 1
A15: m <= m + 1 by NAT_1:11;
k <= m by ;
hence k <= m + 1 by ; :: thesis: verum
end;
suppose p +* (i,k) in {((p +* (i,(m + 1))) +* (i,(m + 1)))} ; :: thesis: k <= m + 1
then A16: p +* (i,k) = (p +* (i,(m + 1))) +* (i,(m + 1)) by TARSKI:def 1
.= p +* (i,(m + 1)) by FUNCT_7:34 ;
k = (p +* (i,k)) . i by
.= m + 1 by ;
hence k <= m + 1 ; :: thesis: verum
end;
end;
end;
end;
suppose ( not i in dom (p +* (i,(m + 1))) or not (p +* (i,(m + 1))) +* (i,m) in dom (F . m) or not ((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 ) ; :: thesis: k <= m + 1
then F . (m + 1) = F . m by A4;
then A17: k <= m by ;
m <= m + 1 by NAT_1:11;
hence k <= m + 1 by ; :: thesis: verum
end;
end;
end;
A18: S2[ 0 ]
proof
let k be Nat; :: thesis: ( p +* (i,k) in dom (F . 0) implies k <= 0 )
assume A19: p +* (i,k) in dom (F . 0) ; :: thesis: k <= 0
per cases ( ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 ) or not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) ;
suppose ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 ) ; :: thesis: k <= 0
then dom (F . 0) = {((p +* (i,(m + 1))) +* (i,0))} by A2;
then A20: p +* (i,k) = (p +* (i,(m + 1))) +* (i,0) by
.= p +* (i,0) by FUNCT_7:34 ;
k = (p +* (i,k)) . i by
.= 0 by ;
hence k <= 0 ; :: thesis: verum
end;
suppose ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) ; :: thesis: k <= 0
hence k <= 0 by ; :: thesis: verum
end;
end;
end;
thus for n being Nat holds S2[n] from :: thesis: verum
end;
thus not p +* (i,(m + 1)) in dom (F . m) :: thesis: verum
proof
assume p +* (i,(m + 1)) in dom (F . m) ; :: thesis: contradiction
then m + 1 <= m by A9;
hence contradiction by NAT_1:13; :: thesis: verum
end;
end;

definition
let n be Nat;
let 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
p +* (i,k) is Element of n -tuples_on NAT
proof end;
end;

Lm4: now :: thesis: for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT
for i, m being Element of NAT st i in dom p holds
for G being Function of (((arity f1) + 1) -tuples_on NAT),() st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds
for k, n being Nat holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n))))
let f1, f2 be non empty NAT * -defined to-naturals homogeneous Function; :: thesis: for p being Element of ((arity f1) + 1) -tuples_on NAT
for i, m being Element of NAT st i in dom p holds
for G being Function of (((arity f1) + 1) -tuples_on NAT),() st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds
for k, n being Nat holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n))))

let p be Element of ((arity f1) + 1) -tuples_on NAT; :: thesis: for i, m being Element of NAT st i in dom p holds
for G being Function of (((arity f1) + 1) -tuples_on NAT),() st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds
for k, n being Nat holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n))))

let i, m be Element of NAT ; :: thesis: ( i in dom p implies for G being Function of (((arity f1) + 1) -tuples_on NAT),() st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds
for k, n being Nat holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n)))) )

assume A1: i in dom p ; :: thesis: for G being Function of (((arity f1) + 1) -tuples_on NAT),() st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds
for k, n being Nat holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n))))

let G be Function of (((arity f1) + 1) -tuples_on NAT),(); :: thesis: ( ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) implies for k, n being Nat holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n)))) )
assume A2: for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ; :: thesis: for k, n being Nat holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n))))
thus for k, n being Nat holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n)))) :: thesis: verum
proof
let k be Nat; :: thesis: for n being Nat holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n))))
set pk = p +* (i,k);
defpred S2[ Nat] means dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + $1)))); A3: now :: thesis: for n being Nat st S2[n] holds S2[n + 1] let n be Nat; :: thesis: ( S2[n] implies S2[b1 + 1] ) assume A4: S2[n] ; :: thesis: S2[b1 + 1] 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 being sequence of () such that A5: primrec (f1,f2,i,(p +* (i,m))) = F . ((p +* (i,m)) /. i) and A6: ( i in dom (p +* (i,m)) & Del ((p +* (i,m)),i) in dom f1 implies F . 0 = ((p +* (i,m)) +* (i,0)) .--> (f1 . (Del ((p +* (i,m)),i))) ) and A7: ( ( not i in dom (p +* (i,m)) or not Del ((p +* (i,m)),i) in dom f1 ) implies F . 0 = {} ) and A8: for M being Nat holds S1[M,F . M,F . (M + 1),p +* (i,m),i,f2] by Def10; dom p = dom (p +* (i,(m + 1))) by FUNCT_7:30; then A9: (p +* (i,(m + 1))) /. i = (p +* (i,(m + 1))) . i by .= m + 1 by ; consider F1 being sequence of () such that A10: primrec (f1,f2,i,(p +* (i,(m + 1)))) = F1 . ((p +* (i,(m + 1))) /. i) and A11: ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F1 . 0 = ((p +* (i,(m + 1))) +* (i,0)) .--> (f1 . (Del ((p +* (i,(m + 1))),i))) ) and A12: ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F1 . 0 = {} ) and A13: for M being Nat holds S1[M,F1 . M,F1 . (M + 1),p +* (i,(m + 1)),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 (p +* (i,m)) by FUNCT_7:30; then (p +* (i,m)) /. i = (p +* (i,m)) . i by .= m by ; then A15: G . (p +* (i,(k + n))) = F . m by A2, A5; per cases ( ( i in dom (p +* (i,m)) & (p +* (i,m)) +* (i,m) in dom (F . m) & ((p +* (i,m)) +* (i,m)) ^ <*((F . m) . ((p +* (i,m)) +* (i,m)))*> in dom f2 ) or not i in dom (p +* (i,m)) or not (p +* (i,m)) +* (i,m) in dom (F . m) or not ((p +* (i,m)) +* (i,m)) ^ <*((F . m) . ((p +* (i,m)) +* (i,m)))*> in dom f2 ) ; suppose ( i in dom (p +* (i,m)) & (p +* (i,m)) +* (i,m) in dom (F . m) & ((p +* (i,m)) +* (i,m)) ^ <*((F . m) . ((p +* (i,m)) +* (i,m)))*> in dom f2 ) ; :: thesis: S2[b1 + 1] then F . (m + 1) = (F . m) +* (((p +* (i,m)) +* (i,(m + 1))) .--> (f2 . (((p +* (i,m)) +* (i,m)) ^ <*((F . m) . ((p +* (i,m)) +* (i,m)))*>))) by A8; then dom (F . (m + 1)) = (dom (F . m)) \/ (dom ({((p +* (i,m)) +* (i,(m + 1)))} --> (f2 . (((p +* (i,m)) +* (i,m)) ^ <*((F . m) . ((p +* (i,m)) +* (i,m)))*>)))) by FUNCT_4:def 1; then dom (F . m) c= dom (F . (m + 1)) by XBOOLE_1:7; hence S2[n + 1] by ; :: thesis: verum end; suppose ( not i in dom (p +* (i,m)) or not (p +* (i,m)) +* (i,m) in dom (F . m) or not ((p +* (i,m)) +* (i,m)) ^ <*((F . m) . ((p +* (i,m)) +* (i,m)))*> in dom f2 ) ; :: thesis: S2[b1 + 1] hence S2[n + 1] by A4, A8, A14, A15; :: thesis: verum end; end; end; A16: S2[ 0 ] ; thus for n being Nat holds S2[n] from NAT_1:sch 2(A16, A3); :: thesis: verum end; end; Lm5: now :: thesis: for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function for p being Element of ((arity f1) + 1) -tuples_on NAT for i, m being Element of NAT st i in dom p holds for G being Function of (((arity f1) + 1) -tuples_on NAT),() st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds for k, n being Nat st not p +* (i,k) in dom (G . (p +* (i,k))) holds not p +* (i,k) in dom (G . (p +* (i,(k + n)))) let f1, f2 be non empty NAT * -defined to-naturals homogeneous Function; :: thesis: for p being Element of ((arity f1) + 1) -tuples_on NAT for i, m being Element of NAT st i in dom p holds for G being Function of (((arity f1) + 1) -tuples_on NAT),() st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds for k, n being Nat st not p +* (i,k) in dom (G . (p +* (i,k))) holds not p +* (i,k) in dom (G . (p +* (i,(k + n)))) let p be Element of ((arity f1) + 1) -tuples_on NAT; :: thesis: for i, m being Element of NAT st i in dom p holds for G being Function of (((arity f1) + 1) -tuples_on NAT),() st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds for k, n being Nat st not p +* (i,k) in dom (G . (p +* (i,k))) holds not p +* (i,k) in dom (G . (p +* (i,(k + n)))) let i, m be Element of NAT ; :: thesis: ( i in dom p implies for G being Function of (((arity f1) + 1) -tuples_on NAT),() st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds for k, n being Nat st not p +* (i,k) in dom (G . (p +* (i,k))) holds not p +* (i,k) in dom (G . (p +* (i,(k + n)))) ) assume A1: i in dom p ; :: thesis: for G being Function of (((arity f1) + 1) -tuples_on NAT),() st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds for k, n being Nat st not p +* (i,k) in dom (G . (p +* (i,k))) holds not p +* (i,k) in dom (G . (p +* (i,(k + n)))) let G be Function of (((arity f1) + 1) -tuples_on NAT),(); :: thesis: ( ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) implies for k, n being Nat st not p +* (i,k) in dom (G . (p +* (i,k))) holds not p +* (i,k) in dom (G . (p +* (i,(k + n)))) ) assume A2: for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ; :: thesis: for k, n being Nat st not p +* (i,k) in dom (G . (p +* (i,k))) holds not p +* (i,k) in dom (G . (p +* (i,(k + n)))) thus for k, n being Nat st not p +* (i,k) in dom (G . (p +* (i,k))) holds not p +* (i,k) in dom (G . (p +* (i,(k + n)))) :: thesis: verum proof let k be Nat; :: thesis: for n being Nat st not p +* (i,k) in dom (G . (p +* (i,k))) holds not p +* (i,k) in dom (G . (p +* (i,(k + n)))) set pk = p +* (i,k); defpred S2[ Nat] means ( not p +* (i,k) in dom (G . (p +* (i,k))) implies not p +* (i,k) in dom (G . (p +* (i,(k +$1)))) );
A3: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume that
A4: S2[n] and
A5: not p +* (i,k) in dom (G . (p +* (i,k))) ; :: thesis: not p +* (i,k) in dom (G . (p +* (i,(k + (n + 1)))))
reconsider m = k + n as Element of NAT by ORDINAL1:def 12;
set pkn = p +* (i,m);
consider F being sequence of () such that
A6: primrec (f1,f2,i,(p +* (i,m))) = F . ((p +* (i,m)) /. i) and
A7: ( i in dom (p +* (i,m)) & Del ((p +* (i,m)),i) in dom f1 implies F . 0 = ((p +* (i,m)) +* (i,0)) .--> (f1 . (Del ((p +* (i,m)),i))) ) and
A8: ( ( not i in dom (p +* (i,m)) or not Del ((p +* (i,m)),i) in dom f1 ) implies F . 0 = {} ) and
A9: for M being Nat holds S1[M,F . M,F . (M + 1),p +* (i,m),i,f2] by Def10;
A10: dom p = dom (p +* (i,m)) by FUNCT_7:30;
then (p +* (i,m)) /. i = (p +* (i,m)) . i by
.= m by ;
then A11: not p +* (i,k) in dom (F . m) by A2, A4, A5, A6;
set pkn1 = p +* (i,((k + n) + 1));
consider F1 being sequence of () such that
A12: primrec (f1,f2,i,(p +* (i,((k + n) + 1)))) = F1 . ((p +* (i,((k + n) + 1))) /. i) and
A13: ( i in dom (p +* (i,((k + n) + 1))) & Del ((p +* (i,((k + n) + 1))),i) in dom f1 implies F1 . 0 = ((p +* (i,((k + n) + 1))) +* (i,0)) .--> (f1 . (Del ((p +* (i,((k + n) + 1))),i))) ) and
A14: ( ( not i in dom (p +* (i,((k + n) + 1))) or not Del ((p +* (i,((k + n) + 1))),i) in dom f1 ) implies F1 . 0 = {} ) and
A15: for M being Nat holds S1[M,F1 . M,F1 . (M + 1),p +* (i,((k + n) + 1)),i,f2] by Def10;
dom p = dom (p +* (i,((k + n) + 1))) by FUNCT_7:30;
then A16: (p +* (i,((k + n) + 1))) /. i = (p +* (i,((k + n) + 1))) . i by
.= m + 1 by ;
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 ( ( i in dom (p +* (i,m)) & (p +* (i,m)) +* (i,m) in dom (F . m) & ((p +* (i,m)) +* (i,m)) ^ <*((F . m) . ((p +* (i,m)) +* (i,m)))*> in dom f2 ) or not i in dom (p +* (i,m)) or not (p +* (i,m)) +* (i,m) in dom (F . m) or not ((p +* (i,m)) +* (i,m)) ^ <*((F . m) . ((p +* (i,m)) +* (i,m)))*> in dom f2 ) ;
suppose ( i in dom (p +* (i,m)) & (p +* (i,m)) +* (i,m) in dom (F . m) & ((p +* (i,m)) +* (i,m)) ^ <*((F . m) . ((p +* (i,m)) +* (i,m)))*> in dom f2 ) ; :: thesis: not p +* (i,k) in dom (G . (p +* (i,(k + (n + 1)))))
then F . (m + 1) = (F . m) +* (((p +* (i,m)) +* (i,(m + 1))) .--> (f2 . (((p +* (i,m)) +* (i,m)) ^ <*((F . m) . ((p +* (i,m)) +* (i,m)))*>))) by A9;
then dom (F . (m + 1)) = (dom (F . m)) \/ (dom ({((p +* (i,m)) +* (i,(m + 1)))} --> (f2 . (((p +* (i,m)) +* (i,m)) ^ <*((F . m) . ((p +* (i,m)) +* (i,m)))*>)))) by FUNCT_4:def 1;
then A18: dom (F . (m + 1)) = (dom (F . m)) \/ {((p +* (i,m)) +* (i,(m + 1)))} ;
k <= k + n by NAT_1:11;
then A19: k <> m + 1 by NAT_1:13;
A20: (p +* (i,k)) . i = k by ;
((p +* (i,m)) +* (i,(m + 1))) . i = m + 1 by ;
then not p +* (i,k) in {((p +* (i,m)) +* (i,(m + 1)))} by ;
hence not p +* (i,k) in dom (G . (p +* (i,(k + (n + 1))))) by ; :: thesis: verum
end;
suppose ( not i in dom (p +* (i,m)) or not (p +* (i,m)) +* (i,m) in dom (F . m) or not ((p +* (i,m)) +* (i,m)) ^ <*((F . m) . ((p +* (i,m)) +* (i,m)))*> in dom f2 ) ; :: thesis: not p +* (i,k) in dom (G . (p +* (i,(k + (n + 1)))))
hence not p +* (i,k) in dom (G . (p +* (i,(k + (n + 1))))) by A9, A11, A17; :: thesis: verum
end;
end;
end;
A21: S2[ 0 ] ;
thus for n being Nat holds S2[n] from NAT_1:sch 2(A21, A3); :: thesis: verum
end;
end;

Lm6: for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT
for i, m being Nat st i in dom p holds
( ( p +* (i,0) in dom (primrec (f1,f2,i)) implies Del (p,i) in dom f1 ) & ( Del (p,i) in dom f1 implies p +* (i,0) in dom (primrec (f1,f2,i)) ) & ( 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)) implies ( 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) in dom (primrec (f1,f2,i)) & (p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*> in dom f2 implies p +* (i,(m + 1)) in dom (primrec (f1,f2,i)) ) & ( 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 end;

theorem :: COMPUT_1:58
for i being Element of NAT
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p holds
( p +* (i,0) in dom (primrec (f1,f2,i)) iff Del (p,i) in dom f1 ) by Lm6;

theorem :: COMPUT_1:59
for i being Element of NAT
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p & p +* (i,0) in dom (primrec (f1,f2,i)) holds
(primrec (f1,f2,i)) . (p +* (i,0)) = f1 . (Del (p,i)) by Lm6;

theorem Th59: :: COMPUT_1:60
for i being Element of NAT
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p & f1 is len-total holds
(primrec (f1,f2,i)) . (p +* (i,0)) = f1 . (Del (p,i))
proof end;

theorem :: COMPUT_1:61
for i, m being Element of NAT
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p holds
( 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
for i, m being Element of NAT
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p & p +* (i,(m + 1)) in dom (primrec (f1,f2,i)) holds
(primrec (f1,f2,i)) . (p +* (i,(m + 1))) = f2 . ((p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*>) by Lm6;

theorem Th62: :: COMPUT_1:63
for i, m being Element of NAT
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st f1 is len-total & f2 is len-total & (arity f1) + 2 = arity f2 & 1 <= i & i <= 1 + (arity f1) holds
(primrec (f1,f2,i)) . (p +* (i,(m + 1))) = f2 . ((p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*>)
proof end;

theorem Th63: :: COMPUT_1:64
for i being Element of NAT
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function st (arity f1) + 2 = arity f2 & 1 <= i & i <= (arity f1) + 1 holds
primrec (f1,f2,i) is_primitive-recursively_expressed_by f1,f2,i
proof end;

theorem :: COMPUT_1:65
for i being Element of NAT
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function st 1 <= i & i <= (arity f1) + 1 holds
for g being Element of HFuncs NAT st g is_primitive-recursively_expressed_by f1,f2,i holds
g = primrec (f1,f2,i)
proof end;

definition
let X be set ;
attr X is composition_closed means :: COMPUT_1:def 12
for f being Element of HFuncs NAT
for F being 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;
attr X is primitive-recursion_closed means :: COMPUT_1:def 13
for g, f1, f2 being Element of HFuncs NAT
for i being Element of NAT st g is_primitive-recursively_expressed_by f1,f2,i & f1 in X & f2 in X holds
g in X;
end;

:: deftheorem defines composition_closed COMPUT_1:def 12 :
for X being set holds
( X is composition_closed iff for f being Element of HFuncs NAT
for F being 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 );

:: deftheorem defines primitive-recursion_closed COMPUT_1:def 13 :
for X being set holds
( X is primitive-recursion_closed iff for g, f1, f2 being Element of HFuncs NAT
for i being Element of NAT st g is_primitive-recursively_expressed_by f1,f2,i & f1 in X & f2 in X holds
g in X );

definition
let X be set ;
attr X is primitive-recursively_closed means :Def14: :: COMPUT_1:def 14
( 0 const 0 in X & 1 succ 1 in X & ( for n, i being Element of NAT st 1 <= i & i <= n holds
n proj i in X ) & X is composition_closed & X is primitive-recursion_closed );
end;

:: deftheorem Def14 defines primitive-recursively_closed COMPUT_1:def 14 :
for X being set holds
( X is primitive-recursively_closed iff ( 0 const 0 in X & 1 succ 1 in X & ( for n, i being Element of NAT st 1 <= i & i <= n holds
n proj i in X ) & X is composition_closed & X is primitive-recursion_closed ) );

theorem Th65: :: COMPUT_1:66
proof end;

registration
existence
ex b1 being Subset of () st
( b1 is primitive-recursively_closed & not b1 is empty )
proof end;
end;

Lm7: for X being non empty set
for n, i being Element of NAT st 1 <= i & i <= n holds
for x being Element of X
for p being Element of n -tuples_on X holds p +* (i,x) in n -tuples_on X

;

theorem Th66: :: COMPUT_1:67
for i being Element of NAT
for e1, e2 being NAT * -defined to-naturals homogeneous Function
for g being Element of HFuncs NAT st e1 = {} & g is_primitive-recursively_expressed_by e1,e2,i holds
g = {}
proof end;

theorem Th67: :: COMPUT_1:68
for g being Element of HFuncs NAT
for f1, f2 being quasi_total Element of HFuncs NAT
for i being Element of NAT st g is_primitive-recursively_expressed_by f1,f2,i holds
( g is quasi_total & ( not f1 is empty implies not g is empty ) )
proof end;

theorem Th68: :: COMPUT_1:69
for c, n being Element of NAT
for P being non empty primitive-recursively_closed Subset of () holds n const c in P
proof end;

theorem Th69: :: COMPUT_1:70
for i, n being Element of NAT
for P being non empty primitive-recursively_closed Subset of () st 1 <= i & i <= n holds
n succ i in P
proof end;

theorem Th70: :: COMPUT_1:71
for P being non empty primitive-recursively_closed Subset of () holds {} in P
proof end;

theorem Th71: :: COMPUT_1:72
for P being non empty primitive-recursively_closed Subset of ()
for f being Element of P
for F being with_the_same_arity FinSequence of P st arity f = len F holds
f * <:F:> in P
proof end;

theorem Th72: :: COMPUT_1:73
for P being non empty primitive-recursively_closed Subset of ()
for f1, f2 being Element of P st (arity f1) + 2 = arity f2 holds
for i being Element of NAT st 1 <= i & i <= (arity f1) + 1 holds
primrec (f1,f2,i) in P
proof end;

definition
func PrimRec -> Subset of () equals :: COMPUT_1:def 15
meet { R where R is Subset of () : R is primitive-recursively_closed } ;
coherence
meet { R where R is Subset of () : R is primitive-recursively_closed } is Subset of ()
proof end;
end;

:: deftheorem defines PrimRec COMPUT_1:def 15 :
PrimRec = meet { R where R is Subset of () : R is primitive-recursively_closed } ;

theorem Th73: :: COMPUT_1:74
for X being Subset of () st X is primitive-recursively_closed holds
PrimRec c= X
proof end;

registration
coherence
( not PrimRec is empty & PrimRec is primitive-recursively_closed )
proof end;
end;

registration
cluster -> homogeneous for Element of PrimRec ;
coherence
for b1 being Element of PrimRec holds b1 is homogeneous
;
end;

definition
let x be set ;
attr x is primitive-recursive means :Def16: :: COMPUT_1:def 16
x in PrimRec ;
end;

:: deftheorem Def16 defines primitive-recursive COMPUT_1:def 16 :
for x being set holds
( x is primitive-recursive iff x in PrimRec );

registration
coherence
for b1 being set st b1 is primitive-recursive holds
( b1 is Relation-like & b1 is Function-like )
;
end;

registration
coherence
for b1 being Relation st b1 is primitive-recursive holds
( b1 is homogeneous & b1 is to-naturals & b1 is NAT * -defined )
;
end;

registration
coherence
for b1 being Element of PrimRec holds b1 is primitive-recursive
;
end;

registration
existence
ex b1 being Function st b1 is primitive-recursive
proof end;
existence
ex b1 being Element of HFuncs NAT st b1 is primitive-recursive
proof end;
end;

definition
func initial-funcs -> Subset of () equals :: COMPUT_1:def 17
{(),(1 succ 1)} \/ { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } ;
coherence
{(),(1 succ 1)} \/ { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } is Subset of ()
proof end;
let Q be Subset of ();
func PR-closure Q -> Subset of () equals :: COMPUT_1:def 18
Q \/ { g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Element of NAT st
( f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by f1,f2,i )
}
;
coherence
Q \/ { g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Element of NAT st
( f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by f1,f2,i )
}
is Subset of ()
proof end;
func composition-closure Q -> Subset of () equals :: COMPUT_1:def 19
Q \/ { (f * <:F:>) where f is Element of HFuncs NAT, F is with_the_same_arity Element of () * : ( f in Q & arity f = len F & rng F c= Q ) } ;
coherence
Q \/ { (f * <:F:>) where f is Element of HFuncs NAT, F is with_the_same_arity Element of () * : ( f in Q & arity f = len F & rng F c= Q ) } is Subset of ()
proof end;
end;

:: deftheorem defines initial-funcs COMPUT_1:def 17 :
initial-funcs = {(),(1 succ 1)} \/ { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } ;

:: deftheorem defines PR-closure COMPUT_1:def 18 :
for Q being Subset of () holds PR-closure Q = Q \/ { g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Element of NAT st
( f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by f1,f2,i )
}
;

:: deftheorem defines composition-closure COMPUT_1:def 19 :
for Q being Subset of () holds composition-closure Q = Q \/ { (f * <:F:>) where f is Element of HFuncs NAT, F is with_the_same_arity Element of () * : ( f in Q & arity f = len F & rng F c= Q ) } ;

definition
func PrimRec-Approximation -> sequence of () means :Def20: :: COMPUT_1:def 20
( it . 0 = initial-funcs & ( for m being Nat holds it . (m + 1) = (PR-closure (it . m)) \/ (composition-closure (it . m)) ) );
existence
ex b1 being sequence of () st
( b1 . 0 = initial-funcs & ( for m being Nat holds b1 . (m + 1) = (PR-closure (b1 . m)) \/ (composition-closure (b1 . m)) ) )
proof end;
uniqueness
for b1, b2 being sequence of () st b1 . 0 = initial-funcs & ( for m being Nat holds b1 . (m + 1) = (PR-closure (b1 . m)) \/ (composition-closure (b1 . m)) ) & b2 . 0 = initial-funcs & ( for m being Nat holds b2 . (m + 1) = (PR-closure (b2 . m)) \/ (composition-closure (b2 . m)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines PrimRec-Approximation COMPUT_1:def 20 :
for b1 being sequence of () holds
( b1 = PrimRec-Approximation iff ( b1 . 0 = initial-funcs & ( for m being Nat holds b1 . (m + 1) = (PR-closure (b1 . m)) \/ (composition-closure (b1 . m)) ) ) );

theorem Th74: :: COMPUT_1:75
for m, n being Element of NAT st m <= n holds
PrimRec-Approximation . m c= PrimRec-Approximation . n
proof end;

theorem Th75: :: COMPUT_1:76
proof end;

theorem Th76: :: COMPUT_1:77
proof end;

theorem Th77: :: COMPUT_1:78
for m being Element of NAT
for f being Element of HFuncs NAT st f in PrimRec-Approximation . m holds
f is quasi_total
proof end;

registration
coherence
for b1 being Element of PrimRec holds
( b1 is quasi_total & b1 is homogeneous )
proof end;
end;

registration
coherence
for b1 being Element of HFuncs NAT st b1 is primitive-recursive holds
b1 is quasi_total
;
end;

registration
coherence
for b1 being NAT * -defined Function st b1 is primitive-recursive holds
b1 is len-total
proof end;
existence
not for b1 being Element of PrimRec holds b1 is empty
proof end;
end;

definition
let n be set ;
let f be homogeneous Relation;
attr f is n -ary means :Def21: :: COMPUT_1:def 21
arity f = n;
end;

:: deftheorem Def21 defines -ary COMPUT_1:def 21 :
for n being set
for f being homogeneous Relation holds
( f is n -ary iff arity f = n );

registration
coherence
for b1 being homogeneous Function st b1 is 1 -ary holds
not b1 is empty
proof end;
coherence
for b1 being homogeneous Function st b1 is 2 -ary holds
not b1 is empty
proof end;
coherence
for b1 being homogeneous Function st b1 is 3 -ary holds
not b1 is empty
proof end;
end;

registration
let n be non zero Element of NAT ;
coherence
proof end;
end;

registration
coherence by Def14;
coherence by Th69;
coherence by Th69;
let i be Element of NAT ;
coherence
0 const i is 0 -ary
by Th31;
coherence
1 const i is 1 -ary
by Th31;
coherence
2 const i is 2 -ary
by Th31;
coherence
3 const i is 3 -ary
by Th31;
coherence
1 proj i is 1 -ary
by Th36;
coherence
2 proj i is 2 -ary
by Th36;
coherence
3 proj i is 3 -ary
by Th36;
coherence
1 succ i is 1 -ary
by Th33;
coherence
2 succ i is 2 -ary
by Th33;
coherence
3 succ i is 3 -ary
by Th33;
let j be Element of NAT ;
coherence by Th68;
end;

registration
existence
ex b1 being homogeneous Function st
( b1 is 0 -ary & b1 is primitive-recursive & not b1 is empty )
by Def14;
existence
ex b1 being homogeneous Function st
( b1 is 1 -ary & b1 is primitive-recursive )
by Def14;
existence
ex b1 being homogeneous Function st
( b1 is 2 -ary & b1 is primitive-recursive )
proof end;
existence
ex b1 being homogeneous Function st
( b1 is 3 -ary & b1 is primitive-recursive )
proof end;
end;

registration
existence
ex b1 being NAT * -defined homogeneous Function st
( not b1 is empty & b1 is 0 -ary & b1 is len-total & b1 is to-naturals )
proof end;
existence
ex b1 being NAT * -defined homogeneous Function st
( not b1 is empty & b1 is 1 -ary & b1 is len-total & b1 is to-naturals )
proof end;
existence
ex b1 being NAT * -defined homogeneous Function st
( not b1 is empty & b1 is 2 -ary & b1 is len-total & b1 is to-naturals )
proof end;
existence
ex b1 being NAT * -defined homogeneous Function st
( not b1 is empty & b1 is 3 -ary & b1 is len-total & b1 is to-naturals )
proof end;
end;

registration
let f be non empty primitive-recursive 0 -ary Function;
let g be primitive-recursive 2 -ary Function;
cluster primrec (f,g,1) -> primitive-recursive 1 -ary ;
coherence
( primrec (f,g,1) is primitive-recursive & primrec (f,g,1) is 1 -ary )
proof end;
end;

registration
let f be primitive-recursive 1 -ary Function;
let g be primitive-recursive 3 -ary Function;
cluster primrec (f,g,1) -> primitive-recursive 2 -ary ;
coherence
( primrec (f,g,1) is primitive-recursive & primrec (f,g,1) is 2 -ary )
proof end;
cluster primrec (f,g,2) -> primitive-recursive 2 -ary ;
coherence
( primrec (f,g,2) is primitive-recursive & primrec (f,g,2) is 2 -ary )
proof end;
end;

theorem Th78: :: COMPUT_1:79
for i being Element of NAT
for f1 being NAT * -defined to-naturals homogeneous len-total 1 -ary Function
for f2 being non empty NAT * -defined to-naturals homogeneous Function holds (primrec (f1,f2,2)) . <*i,0*> = f1 . <*i*>
proof end;

theorem Th79: :: COMPUT_1:80
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function st f1 is len-total & arity f1 = 0 holds
(primrec (f1,f2,1)) . = f1 . {}
proof end;

theorem Th80: :: COMPUT_1:81
for i, j being Element of NAT
for f1 being NAT * -defined to-naturals homogeneous len-total 1 -ary Function
for f2 being NAT * -defined to-naturals homogeneous len-total 3 -ary Function holds (primrec (f1,f2,2)) . <*i,(j + 1)*> = f2 . <*i,j,((primrec (f1,f2,2)) . <*i,j*>)*>
proof end;

theorem Th81: :: COMPUT_1:82
for i being Element of NAT
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function st f1 is len-total & f2 is len-total & arity f1 = 0 & arity f2 = 2 holds
(primrec (f1,f2,1)) . <*(i + 1)*> = f2 . <*i,((primrec (f1,f2,1)) . <*i*>)*>
proof end;

Lm8: now :: thesis: for g being non empty homogeneous quasi_total PartFunc of (),NAT st arity g = 2 holds
( dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3)) & dom <:<*(3 proj 1),(3 proj 3)*>:> = 3 -tuples_on NAT & dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT & ex G being homogeneous PartFunc of (),NAT st
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty ) )
reconsider z3 = <*0,0,0*> as FinSequence of NAT ;
let g be non empty homogeneous quasi_total PartFunc of (),NAT; :: thesis: ( arity g = 2 implies ( dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3)) & dom <:<*(3 proj 1),(3 proj 3)*>:> = 3 -tuples_on NAT & dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT & ex G being homogeneous PartFunc of (),NAT st
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty ) ) )

set G = g * <:<*(3 proj 1),(3 proj 3)*>:>;
A1: rng (g * <:<*(3 proj 1),(3 proj 3)*>:>) c= NAT by RELAT_1:def 19;
assume A2: arity g = 2 ; :: thesis: ( dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3)) & dom <:<*(3 proj 1),(3 proj 3)*>:> = 3 -tuples_on NAT & dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT & ex G being homogeneous PartFunc of (),NAT st
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty ) )

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; :: thesis: ( dom <:<*(3 proj 1),(3 proj 3)*>:> = 3 -tuples_on NAT & dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT & ex G being homogeneous PartFunc of (),NAT st
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty ) )

hence A5: dom <:<*(3 proj 1),(3 proj 3)*>:> = () /\ (dom (3 proj 3)) by Th35
.= () /\ () by Th35
.= 3 -tuples_on NAT ;
:: thesis: ( dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT & ex G being homogeneous PartFunc of (),NAT st
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty ) )

now :: thesis: for x being object holds
( ( x in rng <:<*(3 proj 1),(3 proj 3)*>:> implies x in dom g ) & ( x in dom g implies x in rng <:<*(3 proj 1),(3 proj 3)*>:> ) )
set f = <*(3 proj 1),(3 proj 3)*>;
let x be object ; :: thesis: ( ( x in rng <:<*(3 proj 1),(3 proj 3)*>:> implies x in dom g ) & ( x in dom g implies x in rng <:<*(3 proj 1),(3 proj 3)*>:> ) )
set F = <:<*(3 proj 1),(3 proj 3)*>:>;
A6: product (rngs <*(3 proj 1),(3 proj 3)*>) = product <*(rng (3 proj 1)),(rng (3 proj 3))*> by FINSEQ_3:133
.= product <*NAT,(rng (3 proj 3))*> by Th35
.= product by Th35
.= 2 -tuples_on NAT by FINSEQ_3:128 ;
hereby :: thesis: ( x in dom g implies x in rng <:<*(3 proj 1),(3 proj 3)*>:> )
A7: rng <:<*(3 proj 1),(3 proj 3)*>:> c= product (rngs <*(3 proj 1),(3 proj 3)*>) by FUNCT_6:29;
assume x in rng <:<*(3 proj 1),(3 proj 3)*>:> ; :: thesis: x in dom g
hence x in dom g by A3, A6, A7; :: thesis: verum
end;
assume x in dom g ; :: thesis: x in rng <:<*(3 proj 1),(3 proj 3)*>:>
then x is Element of 2 -tuples_on NAT by ;
then consider d1, d2 being 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;
<:<*(3 proj 1),(3 proj 3)*>:> . x9 = <*((3 proj 1) . x9),((3 proj 3) . x9)*> by
.= <*(x9 . 1),((3 proj 3) . x9)*> by Th37
.= <*(x9 . 1),(x9 . 3)*> by Th37
.= <*d1,(x9 . 3)*> by FINSEQ_1:45
.= x by ;
hence x in rng <:<*(3 proj 1),(3 proj 3)*>:> by ; :: thesis: verum
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 ; :: thesis: ex G being homogeneous PartFunc of (),NAT st
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty )

then reconsider G = g * <:<*(3 proj 1),(3 proj 3)*>:> as PartFunc of (),NAT by ;
reconsider G = G as homogeneous PartFunc of (),NAT by ;
take G = G; :: thesis: ( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty )
thus G = g * <:<*(3 proj 1),(3 proj 3)*>:> ; :: thesis: ( G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty )
G is Element of PFuncs ((),NAT) by PARTFUN1:45;
then G in HFuncs NAT ;
hence G is Element of HFuncs NAT ; :: thesis: ( arity G = 3 & G is quasi_total & not G is empty )
len z3 = 3 by FINSEQ_1:45;
then A10: z3 is Element of 3 -tuples_on NAT by FINSEQ_2:92;
for x being FinSequence st x in dom G holds
3 = len x by ;
hence arity G = 3 by ; :: thesis: ( G is quasi_total & not G is empty )
hence ( G is quasi_total & not G is empty ) by ; :: thesis: verum
end;

definition
let g be Function;
func (1,2)->(1,?,2) g -> Function equals :: COMPUT_1:def 22
g * <:<*(3 proj 1),(3 proj 3)*>:>;
coherence
g * <:<*(3 proj 1),(3 proj 3)*>:> is Function
;
end;

:: deftheorem defines (1,2)->(1,?,2) COMPUT_1:def 22 :
for g being Function holds (1,2)->(1,?,2) g = g * <:<*(3 proj 1),(3 proj 3)*>:>;

registration
let g be NAT * -defined to-naturals Function;
coherence
proof end;
end;

registration
let g be homogeneous Function;
coherence
proof end;
end;

registration
let g be NAT * -defined to-naturals homogeneous len-total 2 -ary Function;
coherence
( not (1,2)->(1,?,2) g is empty & (1,2)->(1,?,2) g is 3 -ary & (1,2)->(1,?,2) g is len-total )
proof end;
end;

theorem Th82: :: COMPUT_1:83
for i, j, k being Element of NAT
for f being NAT * -defined to-naturals homogeneous len-total 2 -ary Function holds () . <*i,j,k*> = f . <*i,k*>
proof end;

theorem Th83: :: COMPUT_1:84
for g being primitive-recursive 2 -ary Function holds (1,2)->(1,?,2) g in PrimRec
proof end;

registration
let f be homogeneous primitive-recursive 2 -ary Function;
coherence by Th83;
end;

definition
func [+] -> primitive-recursive 2 -ary Function equals :: COMPUT_1:def 23
primrec ((1 proj 1),(3 succ 3),2);
coherence
primrec ((1 proj 1),(3 succ 3),2) is primitive-recursive 2 -ary Function
;
end;

:: deftheorem defines [+] COMPUT_1:def 23 :
[+] = primrec ((1 proj 1),(3 succ 3),2);

theorem Th84: :: COMPUT_1:85
for i, j being Element of NAT holds [+] . <*i,j*> = i + j
proof end;

definition
func [*] -> primitive-recursive 2 -ary Function equals :: COMPUT_1:def 24
primrec ((),,2);
coherence
primrec ((),,2) is primitive-recursive 2 -ary Function
;
end;

:: deftheorem defines [*] COMPUT_1:def 24 :
[*] = primrec ((),,2);

theorem Th85: :: COMPUT_1:86
for i, j being Nat holds [*] . <*i,j*> = i * j
proof end;

registration
let g, h be homogeneous primitive-recursive 2 -ary Function;
coherence
proof end;
end;

registration
let f, g, h be primitive-recursive 2 -ary Function;
coherence
proof end;
end;

registration
let f, g, h be primitive-recursive 2 -ary Function;
cluster <:<*g,h*>:> * f -> 2 -ary ;
coherence
f * <:<*g,h*>:> is 2 -ary
proof end;
end;

registration
let f be primitive-recursive 1 -ary Function;
let g be primitive-recursive Function;
coherence
proof end;
end;

registration
let f be primitive-recursive 1 -ary Function;
let g be primitive-recursive 2 -ary Function;
cluster * f -> 2 -ary ;
coherence
f * is 2 -ary
proof end;
end;

definition
func [!] -> primitive-recursive 1 -ary Function equals :: COMPUT_1:def 25
primrec ((),([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>),1);
coherence
primrec ((),([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>),1) is primitive-recursive 1 -ary Function
;
end;

:: deftheorem defines [!] COMPUT_1:def 25 :
[!] = primrec ((),([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>),1);

scheme :: COMPUT_1:sch 1
Primrec1{ F1() -> NAT * -defined to-naturals homogeneous len-total 1 -ary Function, F2() -> NAT * -defined to-naturals homogeneous len-total 2 -ary Function, F3( set ) -> Element of NAT , F4( set , set ) -> Element of NAT } :
for i, j being Element of NAT holds (F1() * <:<*F2()*>:>) . <*i,j*> = F3(F4(i,j))
provided
A1: for i being Element of NAT holds F1() . <*i*> = F3(i) and
A2: for i, j being Element of NAT holds F2() . <*i,j*> = F4(i,j)
proof end;

scheme :: COMPUT_1:sch 2
Primrec2{ F1() -> NAT * -defined to-naturals homogeneous len-total 2 -ary Function, F2() -> NAT * -defined to-naturals homogeneous len-total 2 -ary Function, F3() -> NAT * -defined to-naturals homogeneous len-total 2 -ary Function, F4( set , set ) -> Element of NAT , F5( set , set ) -> Element of NAT , F6( set , set ) -> Element of NAT } :
for i, j being Element of NAT holds (F1() * <:<*F2(),F3()*>:>) . <*i,j*> = F4(F5(i,j),F6(i,j))
provided
A1: for i, j being Element of NAT holds F1() . <*i,j*> = F4(i,j) and
A2: for i, j being Element of NAT holds F2() . <*i,j*> = F5(i,j) and
A3: for i, j being Element of NAT holds F3() . <*i,j*> = F6(i,j)
proof end;

theorem :: COMPUT_1:87
for i being Element of NAT holds [!] . <*i*> = i !
proof end;

definition
func [^] -> primitive-recursive 2 -ary Function equals :: COMPUT_1:def 26
primrec ((1 const 1),,2);
coherence
primrec ((1 const 1),,2) is primitive-recursive 2 -ary Function
;
end;

:: deftheorem defines [^] COMPUT_1:def 26 :
[^] = primrec ((1 const 1),,2);

theorem :: COMPUT_1:88
for i, j being Element of NAT holds [^] . <*i,j*> = i |^ j
proof end;

definition
func [pred] -> primitive-recursive 1 -ary Function equals :: COMPUT_1:def 27
primrec ((),(2 proj 1),1);
coherence
primrec ((),(2 proj 1),1) is primitive-recursive 1 -ary Function
;
end;

:: deftheorem defines [pred] COMPUT_1:def 27 :
[pred] = primrec ((),(2 proj 1),1);

theorem Th88: :: COMPUT_1:89
for i being Element of NAT holds
( [pred] . = 0 & [pred] . <*(i + 1)*> = i )