:: The set of primitive recursive functions :: by Grzegorz Bancerek and Piotr Rudnicki :: :: Received July 27, 2001 :: Copyright (c) 2001-2012 Association of Mizar Users begin theorem Th1: :: COMPUT_1:1 for x, y, z being set holds ( <*x,y*> +* (1,z) = <*z,y*> & <*x,y*> +* (2,z) = <*x,z*> ) proofend; 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) proofend; theorem Th3: :: COMPUT_1:3 for i being Element of NAT for x being set for p being FinSequence holds Del ((p +* (i,x)),i) = Del (p,i) proofend; 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) proofend; theorem Th5: :: COMPUT_1:5 for X being set holds 0 -tuples_on X = {{}} proofend; theorem :: COMPUT_1:6 for n being Element of NAT st n <> 0 holds n -tuples_on {} = {} proofend; theorem Th7: :: COMPUT_1:7 for f being Function st {} in rng f holds <:f:> = {} proofend; theorem Th8: :: COMPUT_1:8 for D being non empty set for f being Function st rng f = D holds rng <:<*f*>:> = 1 -tuples_on D proofend; 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 proofend; theorem Th10: :: COMPUT_1:10 for X being set for Y being FinSequenceSet of X holds Y c= X * proofend; begin definition let X be set ; attrX 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 cluster non empty functional compatible for set ; existence ex b1 being set st ( not b1 is empty & b1 is functional & b1 is compatible ) proofend; end; registration let X be functional compatible set ; cluster union X -> Relation-like Function-like ; coherence ( union X is Function-like & union X is Relation-like ) proofend; end; theorem Th11: :: COMPUT_1:11 for X being set holds ( ( X is functional & X is compatible ) iff union X is Function ) proofend; 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 ) proofend; end; theorem Th12: :: COMPUT_1:12 for X being non empty functional compatible set holds dom (union X) = union { (dom f) where f is Element of X : verum } proofend; theorem Th13: :: COMPUT_1:13 for X being functional compatible set for f being Function st f in X holds ( dom f c= dom (union X) & ( for x being set st x in dom f holds (union X) . x = f . x ) ) proofend; theorem Th14: :: COMPUT_1:14 for X being non empty functional compatible set holds rng (union X) = union { (rng f) where f is Element of X : verum } proofend; 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 proofend; end; theorem Th15: :: 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 proofend; begin notation let f be Relation; synonym to-naturals f for natural-valued ; end; registration cluster Relation-like NAT * -defined Function-like to-naturals for set ; existence ex b1 being Function st ( b1 is NAT * -defined & b1 is to-naturals ) proofend; end; definition let f be NAT * -defined Relation; attrf 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 Th16: :: 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 proofend; registration cluster empty Relation-like -> homogeneous for set ; coherence for b1 being Relation st b1 is empty holds b1 is homogeneous proofend; end; registration let p be FinSequence; let x be set ; clusterp .--> x -> non empty homogeneous ; coherence ( not p .--> x is empty & p .--> x is homogeneous ) proofend; end; registration cluster non empty Relation-like Function-like homogeneous for set ; existence ex b1 being Function st ( not b1 is empty & b1 is homogeneous ) proofend; end; registration let f be homogeneous Function; let g be Function; clusterf * g -> homogeneous ; coherence g * f is homogeneous proofend; end; registration let X, Y be set ; cluster 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 b1 is homogeneous proofend; 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 ) proofend; end; registration let X be non empty set ; cluster non empty Relation-like X * -defined X -valued Function-like homogeneous quasi_total for Element of K32(K33((X *),X)); existence ex b1 being PartFunc of (X *),X st ( not b1 is empty & b1 is homogeneous & b1 is quasi_total ) proofend; end; registration cluster non empty Relation-like NAT * -defined Function-like to-naturals homogeneous len-total for set ; existence ex b1 being NAT * -defined Function st ( not b1 is empty & b1 is homogeneous & b1 is to-naturals & b1 is len-total ) proofend; end; registration cluster Function-like -> NAT * -defined to-naturals for Element of K32(K33((NAT *),NAT)); coherence for b1 being PartFunc of (NAT *),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 *),NAT)); coherence for b1 being PartFunc of (NAT *),NAT st b1 is quasi_total holds b1 is len-total proofend; end; theorem Th17: :: COMPUT_1:17 for g being NAT * -defined to-naturals len-total Function holds g is quasi_total PartFunc of (NAT *),NAT proofend; theorem Th18: :: COMPUT_1:18 arity {} = 0 proofend; theorem Th19: :: COMPUT_1:19 for f being homogeneous Relation st dom f = {{}} holds arity f = 0 proofend; theorem Th20: :: COMPUT_1:20 for X, Y being set for f being homogeneous PartFunc of (X *),Y holds dom f c= (arity f) -tuples_on X proofend; theorem Th21: :: COMPUT_1:21 for f being NAT * -defined homogeneous Function holds dom f c= (arity f) -tuples_on NAT proofend; 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 = (arity f) -tuples_on D ) proofend; theorem Th22: :: 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 = (arity f) -tuples_on X ) proofend; theorem Th23: :: COMPUT_1:23 for f being NAT * -defined to-naturals homogeneous Function holds ( ( f is len-total & not f is empty ) iff dom f = (arity f) -tuples_on NAT ) proofend; 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 proofend; theorem Th25: :: 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 proofend; definition let R be Relation; attrR 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 cluster empty Relation-like -> with_the_same_arity for set ; coherence for b1 being Relation st b1 is empty holds b1 is with_the_same_arity proofend; end; registration let X be set ; cluster Relation-like NAT -defined X -valued Function-like finite countable FinSequence-like FinSubsequence-like with_the_same_arity for FinSequence of X; existence ex b1 being FinSequence of X st b1 is with_the_same_arity proofend; cluster Relation-like NAT -defined X -valued Function-like finite countable FinSequence-like FinSubsequence-like with_the_same_arity for Element of X * ; existence ex b1 being Element of X * st b1 is with_the_same_arity proofend; 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 ) ) proofend; 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 ) ) proofend; 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 proofend; 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 proofend; 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 proofend; registration let X be non empty set ; cluster non empty Relation-like X * -defined X -valued Function-like homogeneous quasi_total for Element of HFuncs X; existence ex b1 being Element of HFuncs X st ( not b1 is empty & b1 is homogeneous & b1 is quasi_total ) proofend; 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 proofend; end; registration let X be non empty set ; let S be non empty Subset of (HFuncs X); cluster -> homogeneous for Element of S; coherence for b1 being Element of S holds b1 is homogeneous ; end; theorem Th28: :: COMPUT_1:28 for f being NAT * -defined to-naturals homogeneous Function holds f is Element of HFuncs NAT proofend; theorem Th29: :: COMPUT_1:29 for f being NAT * -defined to-naturals homogeneous len-total Function holds f is quasi_total Element of HFuncs NAT proofend; theorem Th30: :: 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 proofend; definition let n, m be Element of NAT ; funcn const m -> NAT * -defined to-naturals homogeneous Function equals :: COMPUT_1:def 6 (n -tuples_on NAT) --> m; coherence (n -tuples_on NAT) --> m is NAT * -defined to-naturals homogeneous Function proofend; end; :: deftheorem defines const COMPUT_1:def_6_:_ for n, m being Element of NAT holds n const m = (n -tuples_on NAT) --> m; theorem Th31: :: COMPUT_1:31 for n, m being Element of NAT holds n const m in HFuncs NAT proofend; registration let n, m be Element of NAT ; clustern const m -> non empty NAT * -defined to-naturals homogeneous len-total ; coherence ( n const m is len-total & not n const m is empty ) proofend; end; theorem Th32: :: COMPUT_1:32 for n, m being Element of NAT holds arity (n const m) = n proofend; registration cluster -> NAT * -defined to-naturals homogeneous for Element of HFuncs NAT; 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 ; funcn 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 ) ) proofend; 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 proofend; 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 Th33: :: COMPUT_1:33 for n, i being Element of NAT holds n succ i in HFuncs NAT proofend; registration let n, i be Element of NAT ; clustern succ i -> non empty NAT * -defined to-naturals homogeneous len-total ; coherence ( n succ i is len-total & not n succ i is empty ) proofend; end; theorem Th34: :: COMPUT_1:34 for n, i being Element of NAT holds arity (n succ i) = n proofend; definition let n, i be Element of NAT ; funcn proj i -> NAT * -defined to-naturals homogeneous Function equals :: COMPUT_1:def 8 proj ((n |-> NAT),i); correctness coherence proj ((n |-> NAT),i) is NAT * -defined to-naturals homogeneous Function; proofend; end; :: deftheorem defines proj COMPUT_1:def_8_:_ for n, i being Element of NAT holds n proj i = proj ((n |-> NAT),i); theorem Th35: :: COMPUT_1:35 for n, i being Element of NAT holds n proj i in HFuncs NAT proofend; theorem Th36: :: COMPUT_1:36 for n, i being Element of NAT holds ( dom (n proj i) = n -tuples_on NAT & ( 1 <= i & i <= n implies rng (n proj i) = NAT ) ) proofend; registration let n, i be Element of NAT ; clustern proj i -> non empty NAT * -defined to-naturals homogeneous len-total ; coherence ( n proj i is len-total & not n proj i is empty ) proofend; end; theorem Th37: :: COMPUT_1:37 for n, i being Element of NAT holds arity (n proj i) = n proofend; theorem Th38: :: COMPUT_1:38 for n, i being Element of NAT for t being Element of n -tuples_on NAT holds (n proj i) . t = t . i proofend; registration let X be set ; cluster HFuncs X -> functional ; coherence HFuncs X is functional ; end; theorem Th39: :: COMPUT_1:39 for n being Element of NAT for D, E being non empty set for F being Function of D,(HFuncs E) 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 ) proofend; theorem :: COMPUT_1:40 for D being non empty set for F being Function of NAT,(HFuncs D) st ( for i being Element of NAT holds F . i c= F . (i + 1) ) holds Union F in HFuncs D proofend; theorem Th41: :: COMPUT_1:41 for D being non empty set for F being with_the_same_arity FinSequence of HFuncs D holds dom <:F:> c= (arity F) -tuples_on D proofend; registration let X be non empty set ; let F be with_the_same_arity FinSequence of HFuncs X; cluster<:F:> -> homogeneous ; coherence <:F:> is homogeneous proofend; end; theorem Th42: :: 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= (arity F) -tuples_on D & rng (f * <:F:>) c= D & f * <:F:> in HFuncs D ) proofend; 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 proofend; end; registration let f be NAT * -defined homogeneous Function; cluster<*f*> -> with_the_same_arity ; coherence <*f*> is with_the_same_arity proofend; end; theorem :: COMPUT_1:43 for f being NAT * -defined to-naturals homogeneous Function holds arity <*f*> = arity f proofend; theorem Th44: :: 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 proofend; theorem Th45: :: 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:>) = (arity F) -tuples_on D ) proofend; theorem Th46: :: 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 proofend; theorem Th47: :: 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 proofend; theorem Th48: :: 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 proofend; begin definition let g, f1, f2 be NAT * -defined to-naturals homogeneous Function; let i be Element of NAT ; predg is_primitive-recursively_expressed_by f1,f2,i means :Def9: :: 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 Element of 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 Def9 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 Element of 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[ Element of NAT , Element of HFuncs NAT, Element of HFuncs NAT, FinSequence of NAT , Element of 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 Element of 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 Function of NAT,(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 being Element of 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 Function of NAT,(HFuncs NAT) 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 Element of 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 ) ) ) ) proofend; uniqueness for b1, b2 being Element of HFuncs NAT st ex F being Function of NAT,(HFuncs NAT) 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 Element of 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 Function of NAT,(HFuncs NAT) 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 Element of 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 proofend; end; :: deftheorem Def10 defines primrec COMPUT_1:def_10_:_ for f1, f2 being NAT * -defined to-naturals homogeneous Function for i being Element of 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 Function of NAT,(HFuncs NAT) 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 Element of 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 Th49: :: COMPUT_1:49 for i being Element of NAT for e1, e2 being NAT * -defined to-naturals homogeneous Function 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) proofend; theorem Th50: :: COMPUT_1:50 for i being Element of NAT for e1, e2 being NAT * -defined to-naturals homogeneous Function for p being FinSequence of NAT st not i in dom p holds primrec (e1,e2,i,p) = {} proofend; theorem Th51: :: COMPUT_1:51 for i being Element of NAT for e1, e2 being NAT * -defined to-naturals homogeneous Function for p, q being FinSequence of NAT holds primrec (e1,e2,i,p) tolerates primrec (e1,e2,i,q) proofend; theorem Th52: :: COMPUT_1:52 for i being Element of NAT for e1, e2 being NAT * -defined to-naturals homogeneous Function for p being FinSequence of NAT holds dom (primrec (e1,e2,i,p)) c= (1 + (arity e1)) -tuples_on NAT proofend; theorem Th53: :: 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 proofend; theorem Th54: :: 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)) proofend; definition let f1, f2 be NAT * -defined to-naturals homogeneous Function; let i be Element of 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),(HFuncs 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),(HFuncs NAT) st ( b1 = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) ) proofend; uniqueness for b1, b2 being Element of HFuncs NAT st ex G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs 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),(HFuncs 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 proofend; end; :: deftheorem Def11 defines primrec COMPUT_1:def_11_:_ for f1, f2 being NAT * -defined to-naturals homogeneous Function for i being Element of 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),(HFuncs 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 Th55: :: 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 proofend; theorem Th56: :: 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 proofend; theorem Th57: :: 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 ) proofend; 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,_m_being_Element_of_NAT_ for_F1,_F_being_Function_of_NAT,(HFuncs_NAT)_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_Element_of_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_Element_of_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, m being Element of NAT for F1, F being Function of NAT,(HFuncs NAT) 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 Element of 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 Element of 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, m being Element of NAT for F1, F being Function of NAT,(HFuncs NAT) 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 Element of 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 Element of NAT holds S1[M,F . M,F . (M + 1),p +* (i,m),i,f2] ) holds F1 = F let i, m be Element of NAT ; ::_thesis: for F1, F being Function of NAT,(HFuncs NAT) 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 Element of 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 Element of 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 Function of NAT,(HFuncs NAT); ::_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 Element of 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 Element of 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 Element of 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 Element of 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 set st x in NAT holds F . x = F1 . x proof let x be set ; ::_thesis: ( x in NAT implies F . x = F1 . x ) defpred S2[ Element of NAT ] means F . $1 = F1 . $1; A11: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of 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 ; percases ( ( 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 ) ; supposeA15: ( 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; supposeA16: ( 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 Element of NAT holds S2[k] from NAT_1:sch_1(A17, A11); 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_Function_of_NAT,(HFuncs_NAT)_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_Element_of_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 Function of NAT,(HFuncs NAT) 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 Element of 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 Function of NAT,(HFuncs NAT) 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 Element of 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 Function of NAT,(HFuncs NAT) 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 Element of 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 Function of NAT,(HFuncs NAT) 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 Element of 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 Function of NAT,(HFuncs NAT); ::_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 Element of 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 Element of 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 percases ( ( 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 ) ; supposeA5: ( 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 A1, FUNCT_7:31; (p +* (i,m)) . i = m by A1, FUNCT_7:31; 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 A6, TARSKI:def_1; 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 A8, FUNCT_4:11; ::_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 Element of NAT st p +* (i,k) in dom (F . m) holds k <= m proof defpred S2[ Element of NAT ] means for k being Element of NAT st p +* (i,k) in dom (F . $1) holds k <= $1; A10: for m being Element of NAT st S2[m] holds S2[m + 1] proof let m be Element of NAT ; ::_thesis: ( S2[m] implies S2[m + 1] ) assume A11: S2[m] ; ::_thesis: S2[m + 1] let k be Element of 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 percases ( ( 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)))} by FUNCOP_1:13; thus k <= m + 1 ::_thesis: verum proof percases ( p +* (i,k) in dom (F . m) or p +* (i,k) in {((p +* (i,(m + 1))) +* (i,(m + 1)))} ) by A12, A13, XBOOLE_0:def_3; supposeA14: p +* (i,k) in dom (F . m) ; ::_thesis: k <= m + 1 A15: m <= m + 1 by NAT_1:11; k <= m by A11, A14; hence k <= m + 1 by A15, XXREAL_0:2; ::_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 A1, FUNCT_7:31 .= m + 1 by A1, A16, FUNCT_7:31 ; 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 A11, A12; m <= m + 1 by NAT_1:11; hence k <= m + 1 by A17, XXREAL_0:2; ::_thesis: verum end; end; end; A18: S2[ 0 ] proof let k be Element of NAT ; ::_thesis: ( p +* (i,k) in dom (F . 0) implies k <= 0 ) assume A19: p +* (i,k) in dom (F . 0) ; ::_thesis: k <= 0 percases ( ( 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, FUNCOP_1:13; then A20: p +* (i,k) = (p +* (i,(m + 1))) +* (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 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 A3, A19; ::_thesis: verum end; end; end; thus for n being Element of NAT holds S2[n] from NAT_1:sch_1(A18, A10); ::_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 funcp +* (i,k) -> Element of n -tuples_on NAT; coherence p +* (i,k) is Element of n -tuples_on NAT proofend; 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),(HFuncs_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_Element_of_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),(HFuncs 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 Element of 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),(HFuncs 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 Element of 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),(HFuncs 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 Element of 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),(HFuncs 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 Element of 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),(HFuncs 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 Element of 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 Element of NAT holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n)))) thus for k, n being Element of NAT holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n)))) ::_thesis: verum proof let k be Element of NAT ; ::_thesis: for n being Element of NAT holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n)))) set pk = p +* (i,k); defpred S2[ Element of NAT ] means dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + $1)))); A3: now__::_thesis:_for_n_being_Element_of_NAT_st_S2[n]_holds_ S2[n_+_1] let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[b1 + 1] ) assume A4: S2[n] ; ::_thesis: S2[b1 + 1] set m = k + n; set pkn1 = p +* (i,((k + n) + 1)); set pkn = p +* (i,(k + n)); consider F being Function of NAT,(HFuncs NAT) such that A5: primrec (f1,f2,i,(p +* (i,(k + n)))) = F . ((p +* (i,(k + n))) /. i) and A6: ( i in dom (p +* (i,(k + n))) & Del ((p +* (i,(k + n))),i) in dom f1 implies F . 0 = ((p +* (i,(k + n))) +* (i,0)) .--> (f1 . (Del ((p +* (i,(k + n))),i))) ) and A7: ( ( not i in dom (p +* (i,(k + n))) or not Del ((p +* (i,(k + n))),i) in dom f1 ) implies F . 0 = {} ) and A8: for M being Element of NAT holds S1[M,F . M,F . (M + 1),p +* (i,(k + n)),i,f2] by Def10; dom p = dom (p +* (i,((k + n) + 1))) by FUNCT_7:30; then A9: (p +* (i,((k + n) + 1))) /. i = (p +* (i,((k + n) + 1))) . i by A1, PARTFUN1:def_6 .= (k + n) + 1 by A1, FUNCT_7:31 ; consider F1 being Function of NAT,(HFuncs NAT) such that A10: primrec (f1,f2,i,(p +* (i,((k + n) + 1)))) = F1 . ((p +* (i,((k + n) + 1))) /. i) and A11: ( 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 A12: ( ( 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 A13: for M being Element of NAT holds S1[M,F1 . M,F1 . (M + 1),p +* (i,((k + n) + 1)),i,f2] by Def10; F1 = F by A6, A7, A8, A11, A12, A13, Lm2; then A14: G . (p +* (i,(k + (n + 1)))) = F . ((k + n) + 1) by A2, A10, A9; dom p = dom (p +* (i,(k + n))) by FUNCT_7:30; then (p +* (i,(k + n))) /. i = (p +* (i,(k + n))) . i by A1, PARTFUN1:def_6 .= k + n by A1, FUNCT_7:31 ; then A15: G . (p +* (i,(k + n))) = F . (k + n) by A2, A5; percases ( ( i in dom (p +* (i,(k + n))) & (p +* (i,(k + n))) +* (i,(k + n)) in dom (F . (k + n)) & ((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*> in dom f2 ) or not i in dom (p +* (i,(k + n))) or not (p +* (i,(k + n))) +* (i,(k + n)) in dom (F . (k + n)) or not ((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*> in dom f2 ) ; suppose ( i in dom (p +* (i,(k + n))) & (p +* (i,(k + n))) +* (i,(k + n)) in dom (F . (k + n)) & ((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*> in dom f2 ) ; ::_thesis: S2[b1 + 1] then F . ((k + n) + 1) = (F . (k + n)) +* (((p +* (i,(k + n))) +* (i,((k + n) + 1))) .--> (f2 . (((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*>))) by A8; then dom (F . ((k + n) + 1)) = (dom (F . (k + n))) \/ (dom ({((p +* (i,(k + n))) +* (i,((k + n) + 1)))} --> (f2 . (((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*>)))) by FUNCT_4:def_1; then dom (F . (k + n)) c= dom (F . ((k + n) + 1)) by XBOOLE_1:7; hence S2[n + 1] by A4, A14, A15, XBOOLE_1:1; ::_thesis: verum end; suppose ( not i in dom (p +* (i,(k + n))) or not (p +* (i,(k + n))) +* (i,(k + n)) in dom (F . (k + n)) or not ((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*> 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 Element of NAT holds S2[n] from NAT_1:sch_1(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),(HFuncs_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_Element_of_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),(HFuncs 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 Element of 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),(HFuncs 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 Element of 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),(HFuncs 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 Element of 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),(HFuncs 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 Element of 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),(HFuncs 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 Element of 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 Element of 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 Element of 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 Element of NAT ; ::_thesis: for n being Element of 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[ Element of 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 Element of NAT st S2[n] holds S2[n + 1] proof let n be Element of 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))))) set m = k + n; set pkn = p +* (i,(k + n)); consider F being Function of NAT,(HFuncs NAT) such that A6: primrec (f1,f2,i,(p +* (i,(k + n)))) = F . ((p +* (i,(k + n))) /. i) and A7: ( i in dom (p +* (i,(k + n))) & Del ((p +* (i,(k + n))),i) in dom f1 implies F . 0 = ((p +* (i,(k + n))) +* (i,0)) .--> (f1 . (Del ((p +* (i,(k + n))),i))) ) and A8: ( ( not i in dom (p +* (i,(k + n))) or not Del ((p +* (i,(k + n))),i) in dom f1 ) implies F . 0 = {} ) and A9: for M being Element of NAT holds S1[M,F . M,F . (M + 1),p +* (i,(k + n)),i,f2] by Def10; A10: dom p = dom (p +* (i,(k + n))) by FUNCT_7:30; then (p +* (i,(k + n))) /. i = (p +* (i,(k + n))) . i by A1, PARTFUN1:def_6 .= k + n by A1, FUNCT_7:31 ; then A11: not p +* (i,k) in dom (F . (k + n)) by A2, A4, A5, A6; set pkn1 = p +* (i,((k + n) + 1)); consider F1 being Function of NAT,(HFuncs NAT) 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 Element of 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 A1, PARTFUN1:def_6 .= (k + n) + 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 . ((k + n) + 1) by A2, A12, A16; percases ( ( i in dom (p +* (i,(k + n))) & (p +* (i,(k + n))) +* (i,(k + n)) in dom (F . (k + n)) & ((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*> in dom f2 ) or not i in dom (p +* (i,(k + n))) or not (p +* (i,(k + n))) +* (i,(k + n)) in dom (F . (k + n)) or not ((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*> in dom f2 ) ; suppose ( i in dom (p +* (i,(k + n))) & (p +* (i,(k + n))) +* (i,(k + n)) in dom (F . (k + n)) & ((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*> in dom f2 ) ; ::_thesis: not p +* (i,k) in dom (G . (p +* (i,(k + (n + 1))))) then F . ((k + n) + 1) = (F . (k + n)) +* (((p +* (i,(k + n))) +* (i,((k + n) + 1))) .--> (f2 . (((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*>))) by A9; then dom (F . ((k + n) + 1)) = (dom (F . (k + n))) \/ (dom ({((p +* (i,(k + n))) +* (i,((k + n) + 1)))} --> (f2 . (((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*>)))) by FUNCT_4:def_1; then A18: dom (F . ((k + n) + 1)) = (dom (F . (k + n))) \/ {((p +* (i,(k + n))) +* (i,((k + n) + 1)))} by FUNCOP_1:13; k <= k + n by NAT_1:11; then A19: k <> (k + n) + 1 by NAT_1:13; A20: (p +* (i,k)) . i = k by A1, FUNCT_7:31; ((p +* (i,(k + n))) +* (i,((k + n) + 1))) . i = (k + n) + 1 by A1, A10, FUNCT_7:31; then not p +* (i,k) in {((p +* (i,(k + n))) +* (i,((k + n) + 1)))} by A19, A20, TARSKI:def_1; hence not p +* (i,k) in dom (G . (p +* (i,(k + (n + 1))))) by A11, A17, A18, XBOOLE_0:def_3; ::_thesis: verum end; suppose ( not i in dom (p +* (i,(k + n))) or not (p +* (i,(k + n))) +* (i,(k + n)) in dom (F . (k + n)) or not ((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*> 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 Element of NAT holds S2[n] from NAT_1:sch_1(A21, A3); ::_thesis: verum end; end; Lm6: 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,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)))*>) ) ) proofend; 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 Th60: :: 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)) proofend; 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 Th63: :: 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)))*>) proofend; theorem Th64: :: 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 proofend; 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) proofend; begin definition let X be set ; attrX is composition_closed means :Def12: :: 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; attrX is primitive-recursion_closed means :Def13: :: 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 Def12 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 Def13 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 ; attrX 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 Th66: :: COMPUT_1:66 HFuncs NAT is primitive-recursively_closed proofend; registration cluster non empty functional primitive-recursively_closed for Element of K32((HFuncs NAT)); existence ex b1 being Subset of (HFuncs NAT) st ( b1 is primitive-recursively_closed & not b1 is empty ) proofend; 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 Th67: :: 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 = {} proofend; theorem Th68: :: 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 ) ) proofend; theorem Th69: :: COMPUT_1:69 for n, c being Element of NAT for P being non empty primitive-recursively_closed Subset of (HFuncs NAT) holds n const c in P proofend; theorem Th70: :: COMPUT_1:70 for i, n being Element of NAT for P being non empty primitive-recursively_closed Subset of (HFuncs NAT) st 1 <= i & i <= n holds n succ i in P proofend; theorem Th71: :: COMPUT_1:71 for P being non empty primitive-recursively_closed Subset of (HFuncs NAT) holds {} in P proofend; theorem Th72: :: COMPUT_1:72 for P being non empty primitive-recursively_closed Subset of (HFuncs NAT) 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 proofend; theorem Th73: :: COMPUT_1:73 for P being non empty primitive-recursively_closed Subset of (HFuncs NAT) 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 proofend; definition func PrimRec -> Subset of (HFuncs NAT) equals :: COMPUT_1:def 15 meet { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ; coherence meet { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } is Subset of (HFuncs NAT) proofend; end; :: deftheorem defines PrimRec COMPUT_1:def_15_:_ PrimRec = meet { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ; theorem Th74: :: COMPUT_1:74 for X being Subset of (HFuncs NAT) st X is primitive-recursively_closed holds PrimRec c= X proofend; registration cluster PrimRec -> non empty primitive-recursively_closed ; coherence ( not PrimRec is empty & PrimRec is primitive-recursively_closed ) proofend; 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 ; attrx 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 cluster primitive-recursive -> Relation-like Function-like for set ; coherence for b1 being set st b1 is primitive-recursive holds ( b1 is Relation-like & b1 is Function-like ) proofend; end; registration cluster Relation-like primitive-recursive -> NAT * -defined to-naturals homogeneous for set ; coherence for b1 being Relation st b1 is primitive-recursive holds ( b1 is homogeneous & b1 is to-naturals & b1 is NAT * -defined ) proofend; end; registration cluster -> primitive-recursive for Element of PrimRec ; coherence for b1 being Element of PrimRec holds b1 is primitive-recursive by Def16; end; registration cluster Relation-like Function-like primitive-recursive for set ; existence ex b1 being Function st b1 is primitive-recursive proofend; cluster Relation-like NAT * -defined NAT -valued Function-like complex-valued ext-real-valued real-valued to-naturals homogeneous primitive-recursive for Element of HFuncs NAT; existence ex b1 being Element of HFuncs NAT st b1 is primitive-recursive proofend; end; definition func initial-funcs -> Subset of (HFuncs NAT) equals :: COMPUT_1:def 17 {(0 const 0),(1 succ 1)} \/ { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } ; coherence {(0 const 0),(1 succ 1)} \/ { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } is Subset of (HFuncs NAT) proofend; let Q be Subset of (HFuncs NAT); func PR-closure Q -> Subset of (HFuncs NAT) 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 (HFuncs NAT) proofend; func composition-closure Q -> Subset of (HFuncs NAT) equals :: COMPUT_1:def 19 Q \/ { (f * <:F:>) where f is Element of HFuncs NAT, F is with_the_same_arity Element of (HFuncs NAT) * : ( 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 (HFuncs NAT) * : ( f in Q & arity f = len F & rng F c= Q ) } is Subset of (HFuncs NAT) proofend; end; :: deftheorem defines initial-funcs COMPUT_1:def_17_:_ initial-funcs = {(0 const 0),(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 (HFuncs NAT) 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 (HFuncs NAT) holds composition-closure Q = Q \/ { (f * <:F:>) where f is Element of HFuncs NAT, F is with_the_same_arity Element of (HFuncs NAT) * : ( f in Q & arity f = len F & rng F c= Q ) } ; definition func PrimRec-Approximation -> Function of NAT,(bool (HFuncs NAT)) 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 Function of NAT,(bool (HFuncs NAT)) st ( b1 . 0 = initial-funcs & ( for m being Nat holds b1 . (m + 1) = (PR-closure (b1 . m)) \/ (composition-closure (b1 . m)) ) ) proofend; uniqueness for b1, b2 being Function of NAT,(bool (HFuncs NAT)) 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 proofend; end; :: deftheorem Def20 defines PrimRec-Approximation COMPUT_1:def_20_:_ for b1 being Function of NAT,(bool (HFuncs NAT)) 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 Th75: :: COMPUT_1:75 for m, n being Element of NAT st m <= n holds PrimRec-Approximation . m c= PrimRec-Approximation . n proofend; theorem Th76: :: COMPUT_1:76 Union PrimRec-Approximation is primitive-recursively_closed proofend; theorem Th77: :: COMPUT_1:77 PrimRec = Union PrimRec-Approximation proofend; theorem Th78: :: 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 proofend; registration cluster -> homogeneous quasi_total for Element of PrimRec ; coherence for b1 being Element of PrimRec holds ( b1 is quasi_total & b1 is homogeneous ) proofend; end; registration cluster primitive-recursive -> quasi_total for Element of HFuncs NAT; coherence for b1 being Element of HFuncs NAT st b1 is primitive-recursive holds b1 is quasi_total proofend; end; registration cluster Relation-like NAT * -defined Function-like primitive-recursive -> NAT * -defined len-total for set ; coherence for b1 being NAT * -defined Function st b1 is primitive-recursive holds b1 is len-total proofend; cluster non empty Relation-like NAT * -defined NAT -valued Function-like complex-valued ext-real-valued real-valued to-naturals homogeneous quasi_total primitive-recursive for Element of PrimRec ; existence not for b1 being Element of PrimRec holds b1 is empty proofend; end; begin definition let n be set ; let f be homogeneous Relation; attrf 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 cluster Relation-like Function-like homogeneous 1 -ary -> non empty homogeneous for set ; coherence for b1 being homogeneous Function st b1 is 1 -ary holds not b1 is empty proofend; cluster Relation-like Function-like homogeneous 2 -ary -> non empty homogeneous for set ; coherence for b1 being homogeneous Function st b1 is 2 -ary holds not b1 is empty proofend; cluster Relation-like Function-like homogeneous 3 -ary -> non empty homogeneous for set ; coherence for b1 being homogeneous Function st b1 is 3 -ary holds not b1 is empty proofend; end; registration let n be non empty Element of NAT ; clustern proj 1 -> NAT * -defined to-naturals homogeneous primitive-recursive ; coherence n proj 1 is primitive-recursive proofend; end; registration cluster2 proj 2 -> NAT * -defined to-naturals homogeneous primitive-recursive ; coherence 2 proj 2 is primitive-recursive proofend; cluster1 succ 1 -> NAT * -defined to-naturals homogeneous primitive-recursive ; coherence 1 succ 1 is primitive-recursive proofend; cluster3 succ 3 -> NAT * -defined to-naturals homogeneous primitive-recursive ; coherence 3 succ 3 is primitive-recursive proofend; let i be Element of NAT ; cluster0 const i -> NAT * -defined to-naturals homogeneous 0 -ary ; coherence 0 const i is 0 -ary proofend; cluster1 const i -> NAT * -defined to-naturals homogeneous 1 -ary ; coherence 1 const i is 1 -ary proofend; cluster2 const i -> NAT * -defined to-naturals homogeneous 2 -ary ; coherence 2 const i is 2 -ary proofend; cluster3 const i -> NAT * -defined to-naturals homogeneous 3 -ary ; coherence 3 const i is 3 -ary proofend; cluster1 proj i -> NAT * -defined to-naturals homogeneous 1 -ary ; coherence 1 proj i is 1 -ary proofend; cluster2 proj i -> NAT * -defined to-naturals homogeneous 2 -ary ; coherence 2 proj i is 2 -ary proofend; cluster3 proj i -> NAT * -defined to-naturals homogeneous 3 -ary ; coherence 3 proj i is 3 -ary proofend; cluster1 succ i -> NAT * -defined to-naturals homogeneous 1 -ary ; coherence 1 succ i is 1 -ary proofend; cluster2 succ i -> NAT * -defined to-naturals homogeneous 2 -ary ; coherence 2 succ i is 2 -ary proofend; cluster3 succ i -> NAT * -defined to-naturals homogeneous 3 -ary ; coherence 3 succ i is 3 -ary proofend; let j be Element of NAT ; clusteri const j -> NAT * -defined to-naturals homogeneous primitive-recursive ; coherence i const j is primitive-recursive proofend; end; registration cluster non empty Relation-like Function-like homogeneous primitive-recursive 0 -ary for set ; existence ex b1 being homogeneous Function st ( b1 is 0 -ary & b1 is primitive-recursive & not b1 is empty ) by Def14; cluster Relation-like Function-like homogeneous primitive-recursive 1 -ary for set ; existence ex b1 being homogeneous Function st ( b1 is 1 -ary & b1 is primitive-recursive ) by Def14; cluster Relation-like Function-like homogeneous primitive-recursive 2 -ary for set ; existence ex b1 being homogeneous Function st ( b1 is 2 -ary & b1 is primitive-recursive ) proofend; cluster Relation-like Function-like homogeneous primitive-recursive 3 -ary for set ; existence ex b1 being homogeneous Function st ( b1 is 3 -ary & b1 is primitive-recursive ) proofend; end; registration cluster non empty Relation-like NAT * -defined Function-like to-naturals homogeneous len-total 0 -ary for set ; 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 ) proofend; cluster non empty Relation-like NAT * -defined Function-like to-naturals homogeneous len-total 1 -ary for set ; 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 ) proofend; cluster non empty Relation-like NAT * -defined Function-like to-naturals homogeneous len-total 2 -ary for set ; 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 ) proofend; cluster non empty Relation-like NAT * -defined Function-like to-naturals homogeneous len-total 3 -ary for set ; 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 ) proofend; 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 ) proofend; 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 ) proofend; cluster primrec (f,g,2) -> primitive-recursive 2 -ary ; coherence ( primrec (f,g,2) is primitive-recursive & primrec (f,g,2) is 2 -ary ) proofend; end; theorem Th79: :: 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*> proofend; theorem Th80: :: 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)) . <*0*> = f1 . {} proofend; theorem Th81: :: 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*>)*> proofend; theorem Th82: :: 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*>)*> proofend; Lm8: now__::_thesis:_for_g_being_non_empty_homogeneous_quasi_total_PartFunc_of_(NAT_*),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_*),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 *),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 *),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 *),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 Th22; 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 *),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)*>:> = (3 -tuples_on NAT) /\ (dom (3 proj 3)) by Th36 .= (3 -tuples_on NAT) /\ (3 -tuples_on NAT) by Th36 .= 3 -tuples_on NAT ; ::_thesis: ( dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT & ex G being homogeneous PartFunc of (NAT *),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_set_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 set ; ::_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 Th36 .= product <*NAT,NAT*> by Th36 .= 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 A2, Th22; 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 A4, A5, FINSEQ_3:142 .= <*(x9 . 1),((3 proj 3) . x9)*> by Th38 .= <*(x9 . 1),(x9 . 3)*> by Th38 .= <*d1,(x9 . 3)*> by FINSEQ_1:45 .= x by A8, FINSEQ_1:45 ; hence x in rng <:<*(3 proj 1),(3 proj 3)*>:> by A5, FUNCT_1:def_3; ::_thesis: verum end; then rng <:<*(3 proj 1),(3 proj 3)*>:> = dom g by TARSKI:1; hence A9: dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT by A5, RELAT_1:27; ::_thesis: ex G being homogeneous PartFunc of (NAT *),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 *),NAT by A1, FINSEQ_2:142, RELSET_1:4; reconsider G = G as homogeneous PartFunc of (NAT *),NAT by A9, MARGREL1:def_21; 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 *),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 A9, CARD_1:def_7; hence arity G = 3 by A10, A9, MARGREL1:def_25; ::_thesis: ( G is quasi_total & not G is empty ) hence ( G is quasi_total & not G is empty ) by A9, Th22; ::_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; cluster (1,2)->(1,?,2) g -> NAT * -defined to-naturals ; coherence ( (1,2)->(1,?,2) g is to-naturals & (1,2)->(1,?,2) g is NAT * -defined ) proofend; end; registration let g be homogeneous Function; cluster (1,2)->(1,?,2) g -> homogeneous ; coherence (1,2)->(1,?,2) g is homogeneous proofend; end; registration let g be NAT * -defined to-naturals homogeneous len-total 2 -ary Function; cluster (1,2)->(1,?,2) g -> non empty len-total 3 -ary ; 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 ) proofend; end; theorem Th83: :: 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 ((1,2)->(1,?,2) f) . <*i,j,k*> = f . <*i,k*> proofend; theorem Th84: :: COMPUT_1:84 for g being primitive-recursive 2 -ary Function holds (1,2)->(1,?,2) g in PrimRec proofend; registration let f be homogeneous primitive-recursive 2 -ary Function; cluster (1,2)->(1,?,2) f -> primitive-recursive 3 -ary ; coherence ( (1,2)->(1,?,2) f is primitive-recursive & (1,2)->(1,?,2) f is 3 -ary ) proofend; 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 Th85: :: COMPUT_1:85 for i, j being Element of NAT holds [+] . <*i,j*> = i + j proofend; definition func [*] -> primitive-recursive 2 -ary Function equals :: COMPUT_1:def 24 primrec ((1 const 0),((1,2)->(1,?,2) [+]),2); coherence primrec ((1 const 0),((1,2)->(1,?,2) [+]),2) is primitive-recursive 2 -ary Function ; end; :: deftheorem defines [*] COMPUT_1:def_24_:_ [*] = primrec ((1 const 0),((1,2)->(1,?,2) [+]),2); theorem Th86: :: COMPUT_1:86 for i, j being Element of NAT holds [*] . <*i,j*> = i * j proofend; registration let g, h be homogeneous primitive-recursive 2 -ary Function; cluster<*g,h*> -> with_the_same_arity ; coherence <*g,h*> is with_the_same_arity proofend; end; registration let f, g, h be primitive-recursive 2 -ary Function; cluster<:<*g,h*>:> * f -> primitive-recursive ; coherence f * <:<*g,h*>:> is primitive-recursive proofend; 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 proofend; end; registration let f be primitive-recursive 1 -ary Function; let g be primitive-recursive Function; cluster<:<*g*>:> * f -> primitive-recursive ; coherence f * <:<*g*>:> is primitive-recursive proofend; end; registration let f be primitive-recursive 1 -ary Function; let g be primitive-recursive 2 -ary Function; cluster<:<*g*>:> * f -> 2 -ary ; coherence f * <:<*g*>:> is 2 -ary proofend; end; definition func [!] -> primitive-recursive 1 -ary Function equals :: COMPUT_1:def 25 primrec ((0 const 1),([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>),1); coherence primrec ((0 const 1),([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>),1) is primitive-recursive 1 -ary Function ; end; :: deftheorem defines [!] COMPUT_1:def_25_:_ [!] = primrec ((0 const 1),([*] * <:<*((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) proofend; 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) proofend; theorem :: COMPUT_1:87 for i being Element of NAT holds [!] . <*i*> = i ! proofend; definition func [^] -> primitive-recursive 2 -ary Function equals :: COMPUT_1:def 26 primrec ((1 const 1),((1,2)->(1,?,2) [*]),2); coherence primrec ((1 const 1),((1,2)->(1,?,2) [*]),2) is primitive-recursive 2 -ary Function ; end; :: deftheorem defines [^] COMPUT_1:def_26_:_ [^] = primrec ((1 const 1),((1,2)->(1,?,2) [*]),2); theorem :: COMPUT_1:88 for i, j being Element of NAT holds [^] . <*i,j*> = i |^ j proofend; definition func [pred] -> primitive-recursive 1 -ary Function equals :: COMPUT_1:def 27 primrec ((0 const 0),(2 proj 1),1); coherence primrec ((0 const 0),(2 proj 1),1) is primitive-recursive 1 -ary Function ; end; :: deftheorem defines [pred] COMPUT_1:def_27_:_ [pred] = primrec ((0 const 0),(2 proj 1),1); theorem Th89: :: COMPUT_1:89 for i being Element of NAT holds ( [pred] . <*0*> = 0 & [pred] . <*(i + 1)*> = i ) proofend; definition func [-] -> primitive-recursive 2 -ary Function equals :: COMPUT_1:def 28 primrec ((1 proj 1),((1,2)->(1,?,2) ([pred] * <:<*(2 proj 2)*>:>)),2); coherence primrec ((1 proj 1),((1,2)->(1,?,2) ([pred] * <:<*(2 proj 2)*>:>)),2) is primitive-recursive 2 -ary Function ; end; :: deftheorem defines [-] COMPUT_1:def_28_:_ [-] = primrec ((1 proj 1),((1,2)->(1,?,2) ([pred] * <:<*(2 proj 2)*>:>)),2); theorem :: COMPUT_1:90 for i, j being Element of NAT holds [-] . <*i,j*> = i -' j proofend;