:: The set of primitive recursive functions :: by Grzegorz Bancerek and Piotr Rudnicki :: :: Received July 27, 2001 :: Copyright (c) 2001-2016 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1, FINSEQ_1, FUNCT_4, FINSEQ_3, XXREAL_0, NAT_1, ARYTM_3, CARD_1, FINSEQ_2, PARTFUN1, SETFAM_1, FUNCT_6, TARSKI, MSUALG_6, RFUNCT_3, VALUED_0, UNIALG_1, CARD_3, FUNCOP_1, FUNCT_2, PRALG_3, ORDINAL1, ORDINAL4, ZFMISC_1, FINSET_1, VALUED_2, REALSET1, NEWTON, ARYTM_1, COMPUT_1, XCMPLX_0; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, RELAT_1, RELSET_1, FUNCT_1, FINSEQ_1, FINSEQ_2, SETFAM_1, FUNCT_2, MARGREL1, FUNCOP_1, XXREAL_2, VALUED_0, FUNCT_4, CARD_3, PROB_1, FINSEQ_3, FINSEQ_4, PARTFUN1, RFUNCT_3, FUNCT_6, FUNCT_7, MIDSP_3, FINSET_1, NEWTON, NAT_D, NAT_1, RECDEF_1; constructors DOMAIN_1, FUNCT_4, REAL_1, PROB_1, FINSEQ_3, FINSEQ_4, NEWTON, RFUNCT_3, NAT_D, RECDEF_1, XXREAL_2, MIDSP_3, RELSET_1, FUNCT_6, MARGREL1; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCOP_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, FINSEQ_2, FUNCT_7, FUNCT_2, VALUED_0, XXREAL_2, CARD_1, RELSET_1, CARD_3, FINSEQ_3, MARGREL1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Preliminaries reserve i, j, k, c, m, n for Element of NAT, a, x, y, z, X, Y for set, D, E for non empty set, R for Relation, f, g for Function, p, q for FinSequence; theorem :: COMPUT_1:1 <*x,y*>+*(1,z) = <*z,y*> & <*x,y*>+*(2,z) = <*x,z*>; theorem :: COMPUT_1:2 f+*(a,x) = g+*(a,y) implies f+*(a,z) = g+*(a,z); theorem :: COMPUT_1:3 for i being Nat holds Del(p+*(i,x),i) = Del(p,i); theorem :: COMPUT_1:4 p+*(i,a) = q+*(i,a) implies Del(p,i) = Del(q,i); theorem :: COMPUT_1:5 0-tuples_on X = {{}}; theorem :: COMPUT_1:6 n <> 0 implies n-tuples_on {} = {}; theorem :: COMPUT_1:7 for f being Function-yielding Function holds {} in rng f implies <:f:> = {}; theorem :: COMPUT_1:8 rng f = D implies rng <:<*f*>:> = 1-tuples_on D; theorem :: COMPUT_1:9 1 <= i & i <= n+1 implies for p being Element of (n+1)-tuples_on D holds Del(p,i) in n-tuples_on D; begin :: Sets of compatible functions definition let X be set; attr X is compatible means :: COMPUT_1:def 1 for f,g being Function st f in X & g in X holds f tolerates g; end; registration cluster non empty functional compatible for set; end; registration let X be functional compatible set; cluster union X -> Function-like Relation-like; end; ::\$CT theorem :: COMPUT_1:11 X is functional compatible iff union X is Function; registration let X,Y be set; cluster non empty compatible for PFUNC_DOMAIN of X,Y; end; theorem :: COMPUT_1:12 for X being non empty functional compatible set holds dom union X = union the set of all dom f where f is Element of X; theorem :: COMPUT_1:13 for X being functional compatible set, 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; theorem :: COMPUT_1:14 for X being non empty functional compatible set holds rng union X = union the set of all rng f where f is Element of X; registration let X,Y; cluster -> functional for PFUNC_DOMAIN of X,Y; end; theorem :: COMPUT_1:15 for P being compatible PFUNC_DOMAIN of X,Y holds union P is PartFunc of X,Y; begin :: Homogeneous relations notation let f be Relation; synonym f is to-naturals for f is natural-valued; end; registration cluster NAT*-defined to-naturals for Function; end; definition let f be NAT*-defined Relation; attr f is len-total means :: 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; theorem :: COMPUT_1:16 dom R c= n-tuples_on D implies R is homogeneous; registration cluster empty -> homogeneous for Relation; end; registration let p be FinSequence, x be set; cluster p .--> x -> non empty homogeneous; end; registration cluster non empty homogeneous for Function; end; registration let f be homogeneous Function, g be Function; cluster g*f -> homogeneous; end; registration let X,Y be set; cluster homogeneous for PartFunc of X*, Y; end; registration let X,Y be non empty set; cluster non empty homogeneous for PartFunc of X*, Y; end; registration let X be non empty set; cluster non empty homogeneous quasi_total for PartFunc of X*, X; end; registration cluster non empty homogeneous to-naturals len-total for NAT*-defined Function; end; registration cluster -> to-naturals NAT*-defined for PartFunc of NAT*, NAT; end; registration cluster quasi_total -> len-total for PartFunc of NAT*,NAT; end; theorem :: COMPUT_1:17 for g being len-total to-naturals NAT*-defined Function holds g is quasi_total PartFunc of NAT*, NAT; theorem :: COMPUT_1:18 arity {} = 0; theorem :: COMPUT_1:19 for f being homogeneous Relation st dom f = {{}} holds arity f = 0; theorem :: COMPUT_1:20 for f being homogeneous PartFunc of X*, Y holds dom f c= (arity f)-tuples_on X; theorem :: COMPUT_1:21 for f being homogeneous NAT*-defined Function holds dom f c= ( arity f)-tuples_on NAT; theorem :: COMPUT_1:22 for f being homogeneous PartFunc of X*, X holds f is quasi_total non empty iff dom f = (arity f)-tuples_on X; theorem :: COMPUT_1:23 for f being homogeneous to-naturals NAT*-defined Function holds f is len-total non empty iff dom f = (arity f)-tuples_on NAT; theorem :: COMPUT_1:24 for f being non empty homogeneous PartFunc of D*, D, n st dom f c= n -tuples_on D holds arity f = n; theorem :: COMPUT_1:25 for f being homogeneous PartFunc of D*, D, n st dom f = n -tuples_on D holds arity f = n; definition let R be Relation; attr R is with_the_same_arity means :: COMPUT_1:def 3 for f,g being Function st f in rng R & g in rng R holds (f is empty implies g is empty or dom g = {{}}) & (f is non empty & g is non empty implies ex n being Element of NAT, X being non empty set st dom f c= n-tuples_on X & dom g c= n-tuples_on X); end; registration cluster empty -> with_the_same_arity for Relation; end; registration let X be set; cluster with_the_same_arity for FinSequence of X; cluster with_the_same_arity for Element of X*; end; definition let F be with_the_same_arity Relation; func arity F -> Element of NAT means :: 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; end; theorem :: COMPUT_1:26 for F be with_the_same_arity FinSequence st len F = 0 holds arity F = 0; 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}; end; theorem :: COMPUT_1:27 {} in HFuncs X; registration let X be non empty set; cluster non empty homogeneous quasi_total for Element of HFuncs X; end; registration let X be set; cluster -> homogeneous for Element of HFuncs X; end; registration let X be non empty set, S be non empty Subset of HFuncs X; cluster -> homogeneous for Element of S; end; theorem :: COMPUT_1:28 for f being to-naturals homogeneous NAT*-defined Function holds f is Element of HFuncs NAT; theorem :: COMPUT_1:29 for f being len-total to-naturals homogeneous NAT*-defined Function holds f is quasi_total Element of HFuncs NAT; theorem :: COMPUT_1:30 for X being non empty set, 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; definition let n, m be Nat; func n const m -> homogeneous to-naturals NAT*-defined Function equals :: COMPUT_1:def 6 (n-tuples_on NAT) --> m; end; theorem :: COMPUT_1:31 n const m in HFuncs NAT; registration let n,m be Element of NAT; cluster n const m -> len-total non empty; end; theorem :: COMPUT_1:32 arity (n const m) = n; registration cluster -> homogeneous to-naturals NAT*-defined for Element of HFuncs NAT; end; definition let n,i be Element of NAT; func n succ i -> homogeneous to-naturals NAT*-defined Function means :: 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; end; theorem :: COMPUT_1:33 n succ i in HFuncs NAT; registration let n,i be Element of NAT; cluster n succ i -> len-total non empty; end; theorem :: COMPUT_1:34 arity (n succ i) = n; definition let n,i be Nat; func n proj i -> homogeneous to-naturals NAT*-defined Function equals :: COMPUT_1:def 8 proj(n|->NAT, i); end; theorem :: COMPUT_1:35 n proj i in HFuncs NAT; theorem :: COMPUT_1:36 dom (n proj i) = n-tuples_on NAT & (1 <= i & i <= n implies rng (n proj i) = NAT); registration let n,i be Element of NAT; cluster n proj i -> len-total non empty; end; theorem :: COMPUT_1:37 arity (n proj i) = n; theorem :: COMPUT_1:38 for t being Element of n-tuples_on NAT holds (n proj i).t = t.i; registration let X be set; cluster HFuncs X -> functional; end; theorem :: COMPUT_1:39 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 ex f being Element of HFuncs E st f = Union F & dom f c= n-tuples_on E; theorem :: COMPUT_1:40 for F being sequence of HFuncs D st for i being Nat holds F.i c= F.(i+1) holds Union F in HFuncs D; theorem :: COMPUT_1:41 for F being with_the_same_arity FinSequence of HFuncs D holds dom <:F:> c= (arity F)-tuples_on D; registration let X be non empty set; let F be with_the_same_arity FinSequence of HFuncs X; cluster <:F:> -> homogeneous; end; theorem :: COMPUT_1:42 for f being Element of HFuncs D, 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; definition let X,Y be non empty set, P be PFUNC_DOMAIN of X,Y; let S be non empty Subset of P; redefine mode Element of S -> Element of P; end; registration let f be homogeneous NAT*-defined Function; cluster <*f*> -> with_the_same_arity; end; theorem :: COMPUT_1:43 for f being homogeneous to-naturals NAT*-defined Function holds arity <*f*> = arity f; theorem :: COMPUT_1:44 for f,g being non empty Element of HFuncs NAT, F being with_the_same_arity FinSequence of HFuncs NAT st g = f*<:F:> holds arity g = arity F; theorem :: COMPUT_1:45 for f being non empty quasi_total Element of HFuncs D, F being with_the_same_arity FinSequence of HFuncs D st arity f = len F & F is non empty & (for h being Element of HFuncs D st h in rng F holds h is quasi_total non empty) holds f*<:F:> is non empty quasi_total Element of HFuncs D & dom (f*<:F :>) = (arity F)-tuples_on D; theorem :: COMPUT_1:46 for f being quasi_total Element of HFuncs D, 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; theorem :: COMPUT_1:47 for f,g being non empty quasi_total Element of HFuncs D st arity f = 0 & arity g = 0 & f.{} = g.{} holds f = g; theorem :: COMPUT_1:48 for f,g being non empty len-total homogeneous to-naturals NAT* -defined Function st arity f = 0 & arity g = 0 & f.{} = g.{} holds f = g; begin :: Primitive recursiveness reserve f1, f2 for non empty homogeneous to-naturals NAT*-defined Function, e1 , e2 for homogeneous to-naturals NAT*-defined Function, p for Element of (arity f1+1)-tuples_on NAT; definition let g, f1, f2 be homogeneous to-naturals NAT*-defined Function, i be Element of NAT; 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 iff Del(p,i) in dom f1) & (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 iff p+*(i,n) in dom g & (p+*(i,n))^<*g.(p+*(i,n))*> in dom f2) & (p+*(i,n+1) in dom g implies g.(p+*(i,n+1)) = f2.((p+*(i,n))^<*g.(p+*(i,n))*>)); end; definition let f1,f2 be homogeneous to-naturals NAT*-defined Function; let i be Nat; let p be FinSequence of NAT; func primrec(f1,f2,i,p) -> Element of HFuncs NAT means :: COMPUT_1:def 10 ex F being sequence of HFuncs NAT st it = F.(p/.i) & (i in dom p & Del(p,i) in dom f1 implies F.0 = p+*(i,0) .--> (f1.Del(p,i))) & (not i in dom p or not Del(p,i) in dom f1 implies F.0 = {}) & for m 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); end; theorem :: COMPUT_1:49 for i being Nat for p, q being FinSequence of NAT st q in dom primrec(e1,e2,i,p) ex k st q = p+*(i,k); theorem :: COMPUT_1:50 for i being Nat for p being FinSequence of NAT st not i in dom p holds primrec( e1,e2,i,p) = {}; theorem :: COMPUT_1:51 for i being Nat for p, q being FinSequence of NAT holds primrec(e1,e2,i,p) tolerates primrec(e1,e2,i,q); theorem :: COMPUT_1:52 for i being Nat for p being FinSequence of NAT holds dom primrec(e1,e2,i,p) c= ( 1+arity e1)-tuples_on NAT; theorem :: COMPUT_1:53 for p being FinSequence of NAT st e1 is empty holds primrec(e1, e2,i,p) is empty; theorem :: COMPUT_1:54 f1 is len-total & f2 is len-total & arity f1 +2 = arity f2 & 1 <= i & i <= 1+arity f1 implies p in dom primrec(f1,f2,i,p); definition let f1,f2 be homogeneous to-naturals NAT*-defined Function; let i be Nat; func primrec(f1,f2,i) -> Element of HFuncs NAT means :: 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); end; theorem :: COMPUT_1:55 e1 is empty implies primrec(e1,e2,i) is empty; theorem :: COMPUT_1:56 dom primrec(f1,f2,i) c= (arity f1+1)-tuples_on NAT; theorem :: COMPUT_1:57 f1 is len-total & f2 is len-total & arity f1 +2 = arity f2 & 1 <= i & i <= 1+arity f1 implies dom primrec(f1,f2,i) = (arity f1+1)-tuples_on NAT & arity primrec(f1,f2,i) = arity f1+1; definition let n be Nat, p be Element of n-tuples_on NAT; let i,k be Element of NAT; redefine func p+*(i,k) -> Element of n-tuples_on NAT; end; theorem :: COMPUT_1:58 i in dom p implies (p+*(i,0) in dom primrec(f1,f2,i) iff Del(p,i) in dom f1 ); theorem :: COMPUT_1:59 i in dom p & p+*(i,0) in dom primrec(f1,f2,i) implies primrec(f1,f2,i) .(p+*(i,0)) = f1.Del(p,i); theorem :: COMPUT_1:60 i in dom p & f1 is len-total implies primrec(f1,f2,i).(p+*(i,0)) = f1.Del(p,i); theorem :: COMPUT_1:61 i in dom p implies (p+*(i,m+1) in dom primrec(f1,f2,i) iff p+*(i,m) in dom primrec(f1,f2,i) & (p+*(i,m))^<*primrec(f1,f2,i).(p+*(i,m))*> in dom f2); theorem :: COMPUT_1:62 i in dom p & p+*(i,m+1) in dom primrec(f1,f2,i) implies primrec(f1,f2, i).(p+*(i,m+1)) = f2.((p+*(i,m))^<*primrec(f1,f2,i).(p+*(i,m))*>); theorem :: COMPUT_1:63 f1 is len-total & f2 is len-total & arity f1 +2 = arity f2 & 1 <= i & i <= 1+arity f1 implies primrec(f1,f2,i).(p+*(i,m+1)) = f2.((p+*(i,m))^ <*primrec(f1,f2,i).(p+*(i,m))*>); theorem :: COMPUT_1:64 arity f1+2 = arity f2 & 1 <= i & i <= arity f1+1 implies primrec (f1,f2,i) is_primitive-recursively_expressed_by f1,f2,i; theorem :: COMPUT_1:65 1 <= i & i <= arity f1+1 implies for g being Element of HFuncs NAT st g is_primitive-recursively_expressed_by f1,f2,i holds g = primrec(f1,f2,i); begin :: The set of primitive recursive functions definition let X be set; attr X is composition_closed means :: COMPUT_1:def 12 for f being Element of HFuncs NAT , 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, 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; definition let X be set; attr X is primitive-recursively_closed means :: 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; theorem :: COMPUT_1:66 HFuncs NAT is primitive-recursively_closed; registration cluster primitive-recursively_closed non empty for Subset of HFuncs NAT; end; reserve P for primitive-recursively_closed non empty Subset of HFuncs NAT; theorem :: COMPUT_1:67 for g being Element of HFuncs NAT st e1 = {} & g is_primitive-recursively_expressed_by e1, e2, i holds g = {}; theorem :: COMPUT_1:68 for g being Element of HFuncs(NAT), f1, f2 being quasi_total Element of HFuncs(NAT), i being Element of NAT st g is_primitive-recursively_expressed_by f1, f2, i holds g is quasi_total & (f1 is non empty implies g is non empty); theorem :: COMPUT_1:69 n const c in P; theorem :: COMPUT_1:70 1 <= i & i <= n implies n succ i in P; theorem :: COMPUT_1:71 {} in P; theorem :: COMPUT_1:72 for f being Element of P, F being with_the_same_arity FinSequence of P st arity f = len F holds f*<:F:> in P; theorem :: COMPUT_1:73 for f1,f2 being Element of P st arity f1+2 = arity f2 for i being Element of NAT st 1 <= i & i <= arity f1+1 holds primrec(f1,f2,i) in P; 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 }; end; theorem :: COMPUT_1:74 for X being Subset of HFuncs(NAT) st X is primitive-recursively_closed holds PrimRec c= X; registration cluster PrimRec -> non empty primitive-recursively_closed; end; registration cluster -> homogeneous for Element of PrimRec; end; definition let x be set; attr x is primitive-recursive means :: COMPUT_1:def 16 x in PrimRec; end; registration cluster primitive-recursive -> Relation-like Function-like for set; end; registration cluster primitive-recursive -> homogeneous to-naturals NAT*-defined for Relation; end; registration cluster -> primitive-recursive for Element of PrimRec; end; registration cluster primitive-recursive for Function; cluster primitive-recursive for Element of HFuncs NAT; 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}; 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, i being Element of NAT st f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by f1,f2,i}; 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}; end; definition func PrimRec-Approximation -> sequence of bool HFuncs NAT means :: COMPUT_1:def 20 it.0 = initial-funcs & for m being Nat holds it.(m+1) = (PR-closure (it.m)) \/ (composition-closure (it.m)); end; theorem :: COMPUT_1:75 m <= n implies PrimRec-Approximation.m c= PrimRec-Approximation. n; theorem :: COMPUT_1:76 Union PrimRec-Approximation is primitive-recursively_closed; theorem :: COMPUT_1:77 PrimRec = Union PrimRec-Approximation; theorem :: COMPUT_1:78 for f being Element of HFuncs(NAT) st f in PrimRec-Approximation .m holds f is quasi_total; registration cluster -> quasi_total homogeneous for Element of PrimRec; end; registration cluster primitive-recursive -> quasi_total for Element of HFuncs NAT; end; registration cluster primitive-recursive -> len-total for NAT*-defined Function; cluster non empty for Element of PrimRec; end; begin :: Examples definition let n be set; let f be homogeneous Relation; attr f is n-ary means :: COMPUT_1:def 21 arity f = n; end; registration cluster 1-ary -> non empty for homogeneous Function; cluster 2-ary -> non empty for homogeneous Function; cluster 3-ary -> non empty for homogeneous Function; end; registration let n be non zero Element of NAT; cluster n proj 1 -> primitive-recursive; end; registration cluster 2 proj 2 -> primitive-recursive; cluster 1 succ 1 -> primitive-recursive; cluster 3 succ 3 -> primitive-recursive; let i be Element of NAT; cluster 0 const i -> 0-ary; cluster 1 const i -> 1-ary; cluster 2 const i -> 2-ary; cluster 3 const i -> 3-ary; cluster 1 proj i -> 1-ary; cluster 2 proj i -> 2-ary; cluster 3 proj i -> 3-ary; cluster 1 succ i -> 1-ary; cluster 2 succ i -> 2-ary; cluster 3 succ i -> 3-ary; let j be Element of NAT; cluster i const j -> primitive-recursive; end; registration cluster 0-ary primitive-recursive non empty for homogeneous Function; cluster 1-ary primitive-recursive for homogeneous Function; cluster 2-ary primitive-recursive for homogeneous Function; cluster 3-ary primitive-recursive for homogeneous Function; end; registration cluster non empty 0-ary len-total to-naturals for homogeneous NAT*-defined Function; cluster non empty 1-ary len-total to-naturals for homogeneous NAT*-defined Function; cluster non empty 2-ary len-total to-naturals for homogeneous NAT*-defined Function; cluster non empty 3-ary len-total to-naturals for homogeneous NAT*-defined Function; end; registration let f be 0-ary non empty primitive-recursive Function; let g be 2-ary primitive-recursive Function; cluster primrec(f,g,1) -> primitive-recursive 1-ary; end; registration let f be 1-ary primitive-recursive Function; let g be 3-ary primitive-recursive Function; cluster primrec(f,g,1) -> primitive-recursive 2-ary; cluster primrec(f,g,2) -> primitive-recursive 2-ary; end; theorem :: COMPUT_1:79 for f1 be 1-ary len-total to-naturals homogeneous NAT*-defined Function, f2 be non empty to-naturals homogeneous NAT*-defined Function holds primrec(f1,f2,2).<*i,0*> = f1.<*i*>; theorem :: COMPUT_1:80 f1 is len-total & arity f1 = 0 implies primrec(f1,f2,1).<*0*> = f1.{}; theorem :: COMPUT_1:81 for f1 being 1-ary len-total to-naturals homogeneous NAT* -defined Function, f2 being 3-ary len-total to-naturals homogeneous NAT* -defined Function holds primrec(f1,f2,2).<*i,j+1*> = f2.<*i,j,primrec(f1,f2,2) .<*i,j*>*>; theorem :: COMPUT_1:82 f1 is len-total & f2 is len-total & arity f1 = 0 & arity f2 = 2 implies primrec(f1,f2,1).<*i+1*> = f2.<*i,primrec(f1,f2,1).<*i*>*>; definition let g be Function; func (1,2)->(1,?,2) g -> Function equals :: COMPUT_1:def 22 g * <:<*3 proj 1, 3 proj 3*>:>; end; registration let g be to-naturals NAT*-defined Function; cluster (1,2)->(1,?,2) g -> to-naturals NAT*-defined; end; registration let g be homogeneous Function; cluster (1,2)->(1,?,2) g -> homogeneous; end; registration let g be 2-ary len-total to-naturals homogeneous NAT*-defined Function; cluster (1,2)->(1,?,2) g -> non empty 3-ary len-total; end; theorem :: COMPUT_1:83 for f being 2-ary len-total to-naturals homogeneous NAT* -defined Function holds ((1,2)->(1,?,2) f).<*i,j,k*> = f.<*i,k*>; theorem :: COMPUT_1:84 for g being 2-ary primitive-recursive Function holds (1,2)->(1,?,2) g in PrimRec; registration let f be 2-ary primitive-recursive homogeneous Function; cluster (1,2)->(1,?,2) f -> primitive-recursive 3-ary; end; definition func [+] -> 2-ary primitive-recursive Function equals :: COMPUT_1:def 23 primrec(1 proj 1, 3 succ 3, 2); end; theorem :: COMPUT_1:85 [+].<*i,j*> = i+j; definition func [*] -> 2-ary primitive-recursive Function equals :: COMPUT_1:def 24 primrec(1 const 0, (1,2)->(1,?,2) [+], 2); end; theorem :: COMPUT_1:86 for i, j being Nat holds [*].<*i,j*> = i*j; registration let g,h be 2-ary primitive-recursive homogeneous Function; cluster <*g,h*> -> with_the_same_arity; end; registration let f,g,h be 2-ary primitive-recursive Function; cluster f*<:<*g,h*>:> -> primitive-recursive; end; registration let f,g,h be 2-ary primitive-recursive Function; cluster f*<:<*g,h*>:> -> 2-ary; end; registration let f be 1-ary primitive-recursive Function; let g be primitive-recursive Function; cluster f*<:<*g*>:> -> primitive-recursive; end; registration let f be 1-ary primitive-recursive Function; let g be 2-ary primitive-recursive Function; cluster f*<:<*g*>:> -> 2-ary; end; definition func [!] -> 1-ary primitive-recursive Function equals :: COMPUT_1:def 25 primrec(0 const 1, [*]*<:<*(1 succ 1)*<:<*2 proj 1*>:>, 2 proj 2*>:>, 1); end; scheme :: COMPUT_1:sch 1 Primrec1{F() -> 1-ary len-total to-naturals homogeneous NAT*-defined Function, G() -> 2-ary len-total to-naturals homogeneous NAT*-defined Function, f(set) -> Element of NAT, g(set,set) -> Element of NAT}: for i, j being Element of NAT holds (F()*<:<*G()*>:>).<*i,j*> = f(g(i,j)) provided for i being Element of NAT holds F().<*i*> = f(i) and for i,j being Element of NAT holds G().<*i,j*> = g(i,j); scheme :: COMPUT_1:sch 2 Primrec2{F,G,H() -> 2-ary len-total to-naturals homogeneous NAT*-defined Function, f,g,h(set,set) -> Element of NAT}: for i, j being Element of NAT holds (F()*<:<*G(),H()*>:>).<*i,j*> = f(g(i,j),h(i,j)) provided for i,j being Element of NAT holds F().<*i,j*> = f(i,j) and for i,j being Element of NAT holds G().<*i,j*> = g(i,j) and for i,j being Element of NAT holds H().<*i,j*> = h(i,j); theorem :: COMPUT_1:87 [!].<*i*> = i!; definition func [^] -> 2-ary primitive-recursive Function equals :: COMPUT_1:def 26 primrec(1 const 1, (1,2)->(1,?,2) [*], 2); end; theorem :: COMPUT_1:88 [^].<*i,j*> = i |^ j; definition func [pred] -> 1-ary primitive-recursive Function equals :: COMPUT_1:def 27 primrec(0 const 0, 2 proj 1, 1); end; theorem :: COMPUT_1:89 [pred].<*0*> = 0 & [pred].<*i+1*> = i; definition func [-] -> 2-ary primitive-recursive Function equals :: COMPUT_1:def 28 primrec(1 proj 1,(1,2)->(1,?,2) ([pred]*<:<*2 proj 2*>:>), 2); end; theorem :: COMPUT_1:90 [-].<*i,j*> = i -' j;