:: The set of primitive recursive functions
::  by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received July 27, 2001
:: Copyright (c) 2001-2021 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;