:: The set of primitive recursive functions
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received July 27, 2001
:: Copyright (c) 2001-2026 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;
definitions PARTFUN1, RFUNCT_3, FUNCT_1, RELAT_1, TARSKI, MARGREL1;
equalities FINSEQ_2, FUNCOP_1, CARD_3;
expansions PARTFUN1, FUNCT_1, RELAT_1, TARSKI, MARGREL1;
theorems TARSKI, NAT_1, ZFMISC_1, RELAT_1, RELSET_1, FINSEQ_1, FUNCOP_1,
PARTFUN1, FINSEQ_2, FUNCT_6, FUNCT_1, RFUNCT_3, FUNCT_2,
GRFUNC_1, FUNCT_7, FUNCT_4, FINSEQ_3, SETFAM_1, CARD_5, CARD_1, CARD_3,
NEWTON, WSIERP_1, XBOOLE_0, XBOOLE_1, ORDINAL1, XXREAL_0, VALUED_0,
XXREAL_2, XREAL_0, NAT_D, XREAL_1, MARGREL1, XTUPLE_0;
schemes NAT_1, FUNCT_2, RECDEF_1, MONOID_1, PARTFUN2;
begin :: Preliminaries
reserve i, j, k, c, m, n for 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 Th1:
<*x,y*>+*(1,z) = <*z,y*> & <*x,y*>+*(2,z) = <*x,z*>
proof
set a = <*x,y*>+*(1,z), b = <*x,y*>+*(2,z);
<*x,y*>.1 = x;
then
A1: b.1 = x by FUNCT_7:32;
<*x,y*>.2 = y;
then
A2: a.2 = y by FUNCT_7:32;
A3: len <*x,y*> = 2 by FINSEQ_1:44;
then 1 in dom <*x,y*> by FINSEQ_3:25;
then
A4: a.1 = z by FUNCT_7:31;
len a = 2 by A3,FUNCT_7:97;
hence <*x,y*>+*(1,z) = <*z,y*> by A4,A2,FINSEQ_1:44;
2 in dom <*x,y*> by A3,FINSEQ_3:25;
then
A5: b.2 = z by FUNCT_7:31;
len b = 2 by A3,FUNCT_7:97;
hence thesis by A1,A5,FINSEQ_1:44;
end;
theorem Th2:
f+*(a,x) = g+*(a,y) implies f+*(a,z) = g+*(a,z)
proof
set i = a;
assume
A1: f+*(i,x) = g+*(i,y);
A2: dom (g+*(i,z)) = dom g by FUNCT_7:30;
A3: dom (g+*(i,y)) = dom g by FUNCT_7:30;
A4: dom (f+*(i,x)) = dom f by FUNCT_7:30;
now
thus dom (f+*(i,z)) = dom f by FUNCT_7:30;
thus dom (g+*(i,z)) = dom f by A1,A3,A2,FUNCT_7:30;
let a be object;
assume
A5: a in dom f;
per cases;
suppose
A6: a = i;
hence (f+*(i,z)).a = z by A5,FUNCT_7:31
.= (g+*(i,z)).a by A1,A4,A3,A5,A6,FUNCT_7:31;
end;
suppose
A7: a <> i;
hence (f+*(i,z)).a = f.a by FUNCT_7:32
.= (g+*(i,y)).a by A1,A7,FUNCT_7:32
.= g.a by A7,FUNCT_7:32
.= (g+*(i,z)).a by A7,FUNCT_7:32;
end;
end;
hence thesis;
end;
theorem Th3:
for i being Nat holds Del(p+*(i,x),i) = Del(p,i)
proof let i be Nat;
set f = p;
per cases;
suppose
A1: i in dom f;
then
A2: i <= len f by FINSEQ_3:25;
1 <= i by A1,FINSEQ_3:25;
then consider j being Nat such that
A3: len f = j+1 by A2,NAT_1:6;
reconsider j as Element of NAT by ORDINAL1:def 12;
A4: dom (f+*(i,x)) = dom f by FUNCT_7:30;
then
A5: len (f+*(i,x)) = len f by FINSEQ_3:29;
then len Del(f+*(i,x),i) = j by A1,A3,A4,FINSEQ_3:109;
then
A6: dom Del(f+*(i,x),i) = Seg j by FINSEQ_1:def 3;
now
thus len Del(f+*(i,x),i) = j by A1,A3,A4,A5,FINSEQ_3:109;
thus len Del(f,i) = j by A1,A3,FINSEQ_3:109;
let a be Nat;
assume a in dom Del(f+*(i,x),i);
then
A7: a <= j by A6,FINSEQ_1:1;
per cases;
suppose
A8: a < i;
hence Del(f+*(i,x),i).a = (f+*(i,x)).a by FINSEQ_3:110
.= f.a by A8,FUNCT_7:32
.= Del(f,i).a by A8,FINSEQ_3:110;
end;
suppose
A9: i <= a;
then
A10: i < a+1 by NAT_1:13;
thus Del(f+*(i,x),i).a = (f+*(i,x)).(a+1) by A1,A3,A4,A5,A7,A9,
FINSEQ_3:111
.= f.(a+1) by A10,FUNCT_7:32
.= Del(f,i).a by A1,A3,A7,A9,FINSEQ_3:111;
end;
end;
hence thesis by FINSEQ_2:9;
end;
suppose
not i in dom f;
hence thesis by FUNCT_7:def 3;
end;
end;
theorem Th4:
p+*(i,a) = q+*(i,a) implies Del(p,i) = Del(q,i)
proof
set x = p, y = q;
assume
A1: x+*(i,a) = y+*(i,a);
set xi = x+*(i,a), yi = y+*(i,a);
set dx = Del(x,i), dy = Del(y,i);
A2: dom xi = dom x by FUNCT_7:30;
A3: dom yi = dom y by FUNCT_7:30;
A4: Seg len y = dom y by FINSEQ_1:def 3;
A5: Seg len x = dom x by FINSEQ_1:def 3;
per cases;
suppose
A6: i in dom x;
A7: dom Del(x,i) = Seg len dx by FINSEQ_1:def 3;
now
thus len dx = len dx;
x <> {} by A6;
then consider m being Nat such that
A8: len x = m+1 by NAT_1:6;
reconsider m as Element of NAT by ORDINAL1:def 12;
A9: len dx = m by A6,A8,FINSEQ_3:109;
hence len dy = len dx by A1,A2,A3,A5,A4,A6,A8,FINSEQ_1:6,FINSEQ_3:109;
let j be Nat;
assume j in dom Del(x,i);
then
A10: j <= m by A7,A9,FINSEQ_1:1;
per cases;
suppose
A11: j < i;
hence dx.j = x.j by FINSEQ_3:110
.= yi.j by A1,A11,FUNCT_7:32
.= y.j by A11,FUNCT_7:32
.= dy.j by A11,FINSEQ_3:110;
end;
suppose
A12: i <= j;
then
A13: j+1 > i by NAT_1:13;
thus dx.j = x.(j+1) by A6,A8,A10,A12,FINSEQ_3:111
.= yi.(j+1) by A1,A13,FUNCT_7:32
.= y.(j+1) by A13,FUNCT_7:32
.= dy.j by A1,A2,A3,A5,A4,A6,A8,A10,A12,FINSEQ_1:6,FINSEQ_3:111;
end;
end;
hence thesis by FINSEQ_2:9;
end;
suppose
A14: not i in dom x;
then xi = x by FUNCT_7:def 3;
hence thesis by A1,A3,A14,FUNCT_7:def 3;
end;
end;
theorem Th5:
0-tuples_on X = {{}}
proof
set S = {s where s is Element of X*: len s = 0};
now
let x be object;
hereby
assume x in S;
then consider s being Element of X* such that
A1: x = s and
A2: len s = 0;
s = {} by A2;
hence x in {{}} by A1,TARSKI:def 1;
end;
assume x in {{}};
then
A3: x = {} by TARSKI:def 1;
<*>(X*) is Element of X* by FINSEQ_1:49;
hence x in S by A3,CARD_1:27;
end;
hence thesis;
end;
theorem
n <> 0 implies n-tuples_on {} = {}
proof
assume that
A1: n <> 0 and
A2: n-tuples_on {} <> {};
consider x being object such that
A3: x in n-tuples_on {} by A2;
ex s being Element of {}* st s = x & len s = n by A3;
hence contradiction by A1;
end;
theorem Th7:
for f being Function-yielding Function holds
{} in rng f implies <:f:> = {}
proof let f be Function-yielding Function;
A1: dom <:f:> = meet doms f by FUNCT_6:29
.= meet rng doms f by FUNCT_6:def 4;
assume {} in rng f;
then consider x being object such that
A2: x in dom f and
A3: f.x = {} by FUNCT_1:def 3;
A4: dom doms f = dom f by FUNCT_6:def 2;
then
A5: x in dom doms f by A2;
then (doms f).x = {} by A3,A4,FUNCT_6:def 2;
hence thesis by A1,A5,FUNCT_1:3,SETFAM_1:4;
end;
theorem Th8:
rng f = D implies rng <:<*f*>:> = 1-tuples_on D
proof
set X = D;
A1: dom <:<*f*>:> = dom f by FINSEQ_3:141;
assume
A2: rng f = X;
now
let x be object;
hereby
assume x in rng <:<*f*>:>;
then consider y being object such that
A3: y in dom <:<*f*>:> and
A4: <:<*f*>:>.y = x by FUNCT_1:def 3;
reconsider fy = f.y as Element of X by A2,A1,A3,FUNCT_1:3;
A5: <*fy*> is Element of 1-tuples_on X by FINSEQ_2:131;
<:<*f*>:>.y = <*f.y*> by A1,A3,FINSEQ_3:141;
hence x in 1-tuples_on X by A4,A5;
end;
assume x in 1-tuples_on X;
then x is Tuple of 1,X by FINSEQ_2:131;
then consider d being Element of X such that
A6: x = <*d*> by FINSEQ_2:97;
consider y being object such that
A7: y in dom f and
A8: f.y = d by A2,FUNCT_1:def 3;
<:<*f*>:>.y = <*d*> by A7,A8,FINSEQ_3:141;
hence x in rng <:<*f*>:> by A1,A6,A7,FUNCT_1:3;
end;
hence thesis by TARSKI:2;
end;
theorem Th9:
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
proof
set X = D;
assume that
A1: 1 <= i and
A2: i <= n+1;
let p be Element of (n+1)-tuples_on X;
A3: len p = n+1 by CARD_1:def 7;
then i in dom p by A1,A2,FINSEQ_3:25;
then
A4: len Del(p,i) = n by A3,FINSEQ_3:109;
Del(p,i) is FinSequence of X by FINSEQ_3:105;
then Del(p,i) is Element of n-tuples_on X by A4,FINSEQ_2:92;
hence thesis;
end;
begin :: Sets of compatible functions
definition
let X be set;
attr X is compatible means
:Def1:
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;
existence
proof
set A = {{}};
take A;
A is compatible
proof
let f, g be Function;
assume that
A1: f in A and
g in A;
f={} by A1,TARSKI:def 1;
hence thesis;
end;
hence thesis;
end;
end;
registration
let X be functional compatible set;
cluster union X -> Function-like Relation-like;
coherence
proof
thus union X is Function-like
proof
let x,y1,y2 be object;
assume that
A1: [x,y1] in union X and
A2: [x,y2] in union X;
consider f being set such that
A3: [x,y1] in f and
A4: f in X by A1,TARSKI:def 4;
consider g being set such that
A5: [x,y2] in g and
A6: g in X by A2,TARSKI:def 4;
reconsider f, g as Function by A4,A6;
A7: y1 is set & y2 is set by TARSKI:1;
A8: x in dom f by A3,XTUPLE_0:def 12;
then
A9: f.x = y1 by A3,FUNCT_1:def 2,A7;
A10: x in dom g by A5,XTUPLE_0:def 12;
then
A11: g.x = y2 by A5,FUNCT_1:def 2,A7;
A12: x in dom f /\ dom g by A8,A10,XBOOLE_0:def 4;
f tolerates g by A4,A6,Def1;
hence thesis by A9,A11,A12;
end;
thus union X is Relation-like
proof
let x be object;
assume x in union X;
then ex f being set st x in f & f in X by TARSKI:def 4;
hence thesis by RELAT_1:def 1;
end;
end;
end;
::$CT
theorem Th10:
X is functional compatible iff union X is Function
proof
now
assume
A1: union X is Function;
thus X is functional
proof
let f be object;
assume
A2: f in X;
reconsider f as set by TARSKI:1;
A3: f is Function-like
proof
let x, y1, y2 be object;
assume that
A4: [x,y1] in f and
A5: [x, y2] in f;
A6: [x,y2] in union X by A2,A5,TARSKI:def 4;
[x,y1] in union X by A2,A4,TARSKI:def 4;
hence thesis by A1,A6,FUNCT_1:def 1;
end;
f is Relation-like
proof
let x be object;
assume x in f;
then x in union X by A2,TARSKI:def 4;
hence thesis by A1,RELAT_1:def 1;
end;
hence thesis by A3;
end;
thus X is compatible
proof
let f,g be Function such that
A7: f in X and
A8: g in X;
let x be object;
assume
A9: x in dom f /\ dom g;
then
A10: x in dom g by XBOOLE_0:def 4;
then consider y2 being object such that
A11: [x,y2] in g by XTUPLE_0:def 12;
A12: [x,y2] in union X by A8,A11,TARSKI:def 4;
A13: x in dom f by A9,XBOOLE_0:def 4;
then consider y1 being object such that
A14: [x,y1] in f by XTUPLE_0:def 12;
A15: y1 is set by TARSKI:1;
[x,y1] in union X by A7,A14,TARSKI:def 4;
then
A16: y1 = y2 by A1,A12,FUNCT_1:def 1;
thus f.x = y1 by A13,A14,FUNCT_1:def 2,A15
.= g.x by A10,A11,A16,FUNCT_1:def 2,A15;
end;
end;
hence thesis;
end;
registration
let X,Y be set;
cluster non empty compatible for PFUNC_DOMAIN of X,Y;
existence
proof
set A = {{}};
A1: A is compatible
proof
let f, g be Function;
assume that
A2: f in A and
g in A;
f = {} by A2,TARSKI:def 1;
hence thesis;
end;
now
let x be Element of A;
x = {} by TARSKI:def 1;
hence x is PartFunc of X, Y by XBOOLE_1:2;
end;
then A is PFUNC_DOMAIN of X,Y by RFUNCT_3:def 3;
hence thesis by A1;
end;
end;
theorem Th11:
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
proof
let X be non empty functional compatible set;
set F = the set of all dom f where f is Element of X;
now
let x be object;
hereby
assume x in dom union X;
then consider y being object such that
A1: [x,y] in union X by XTUPLE_0:def 12;
consider Z being set such that
A2: [x,y] in Z and
A3: Z in X by A1,TARSKI:def 4;
reconsider Z as Element of X by A3;
A4: dom Z in F;
x in dom Z by A2,XTUPLE_0:def 12;
hence x in union F by A4,TARSKI:def 4;
end;
assume x in union F;
then consider Z being set such that
A5: x in Z and
A6: Z in F by TARSKI:def 4;
consider f being Element of X such that
A7: Z = dom f by A6;
consider y being object such that
A8: [x, y] in f by A5,A7,XTUPLE_0:def 12;
[x, y] in union X by A8,TARSKI:def 4;
hence x in dom union X by XTUPLE_0:def 12;
end;
hence thesis by TARSKI:2;
end;
theorem Th12:
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
proof
let X be functional compatible set, f be Function such that
A1: f in X;
thus dom f c= dom union X
proof
let x be object;
assume x in dom f;
then consider y being object such that
A2: [x,y] in f by XTUPLE_0:def 12;
[x, y] in union X by A1,A2,TARSKI:def 4;
hence thesis by XTUPLE_0:def 12;
end;
let x being set;
assume x in dom f;
then consider y being object such that
A3: [x,y] in f by XTUPLE_0:def 12;
[x, y] in union X by A1,A3,TARSKI:def 4;
hence (union X).x = y by FUNCT_1:1
.= f.x by A3,FUNCT_1:1;
end;
theorem Th13:
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
proof
let X be non empty functional compatible set;
set F = the set of all rng f where f is Element of X;
now
let y be object;
hereby
assume y in rng union X;
then consider x being object such that
A1: [x,y] in union X by XTUPLE_0:def 13;
consider Z being set such that
A2: [x,y] in Z and
A3: Z in X by A1,TARSKI:def 4;
reconsider Z as Element of X by A3;
A4: rng Z in F;
y in rng Z by A2,XTUPLE_0:def 13;
hence y in union F by A4,TARSKI:def 4;
end;
assume y in union F;
then consider Z being set such that
A5: y in Z and
A6: Z in F by TARSKI:def 4;
consider f being Element of X such that
A7: Z = rng f by A6;
consider x being object such that
A8: [x, y] in f by A5,A7,XTUPLE_0:def 13;
[x, y] in union X by A8,TARSKI:def 4;
hence y in rng union X by XTUPLE_0:def 13;
end;
hence thesis by TARSKI:2;
end;
registration
let X,Y;
cluster -> functional for PFUNC_DOMAIN of X,Y;
coherence
by RFUNCT_3:def 3;
end;
theorem Th14:
for P being compatible PFUNC_DOMAIN of X,Y holds union P is PartFunc of X,Y
proof
let D be compatible PFUNC_DOMAIN of X,Y;
set E = the set of all dom f where f is Element of D;
set F = the set of all rng f where f is Element of D;
reconsider u = union D as Function;
A1: rng u c= Y
proof
let y be object;
assume y in rng u;
then y in union F by Th13;
then consider Z being set such that
A2: y in Z and
A3: Z in F by TARSKI:def 4;
consider f being Element of D such that
A4: Z = rng f by A3;
rng f c= Y by RELAT_1:def 19;
hence thesis by A2,A4;
end;
dom u c= X
proof
let x be object;
assume x in dom u;
then x in union E by Th11;
then consider Z being set such that
A5: x in Z and
A6: Z in E by TARSKI:def 4;
ex f being Element of D st Z = dom f by A6;
hence thesis by A5;
end;
hence thesis by A1,RELSET_1:4;
end;
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;
existence
proof
take f={};
thus dom f c= NAT*;
thus thesis;
end;
end;
definition
let f be NAT*-defined Relation;
attr f is len-total means
:Def2:
for x,y being FinSequence of NAT st len x = len y & x in dom f
holds y in dom f;
end;
theorem Th15:
dom R c= n-tuples_on D implies R is homogeneous;
registration
cluster empty -> homogeneous for Relation;
coherence;
end;
registration
let p be FinSequence, x be set;
cluster p .--> x -> non empty homogeneous;
coherence;
end;
registration
cluster non empty homogeneous for Function;
existence
proof
set p = the FinSequence;
take p.-->0;
thus thesis;
end;
end;
registration
let f be homogeneous Function, g be Function;
cluster g*f -> homogeneous;
coherence
proof
dom(g*f) c= dom f by RELAT_1:25;
hence dom(g*f) is with_common_domain;
end;
end;
registration
let X,Y be set;
cluster homogeneous for PartFunc of X*, Y;
existence
proof
set f = {};
reconsider f as PartFunc of X*, Y by XBOOLE_1:2;
take f;
thus dom f is with_common_domain;
end;
end;
registration
let X,Y be non empty set;
cluster non empty homogeneous for PartFunc of X*, Y;
existence
proof
set y = the Element of Y;
reconsider Z = 0-tuples_on X as non empty Subset of X* by FINSEQ_2:90;
reconsider f = Z --> y as PartFunc of X*, Y;
take f;
thus f is non empty;
thus dom f is with_common_domain;
end;
end;
registration
let X be non empty set;
cluster non empty homogeneous quasi_total for PartFunc of X*, X;
existence
proof
set n = the Element of NAT,y = the Element of X;
reconsider Z = n-tuples_on X as non empty Subset of X* by FINSEQ_2:90;
reconsider f = Z --> y as PartFunc of X*, X;
take f;
thus f is non empty;
thus f is homogeneous;
let p,q be FinSequence of X;
assume that
A2: len p = len q and
A3: p in dom f;
len q = n by A2,A3,CARD_1:def 7;
then q is Element of Z by FINSEQ_2:92;
hence thesis;
end;
end;
registration
cluster non empty homogeneous to-naturals len-total for
NAT*-defined Function;
existence
proof
reconsider Z = 0-tuples_on NAT as non empty Subset of NAT* by FINSEQ_2:90;
set f = Z --> 0;
reconsider f as NAT*-defined Function;
A2: f is len-total
proof
let x,y be FinSequence of NAT such that
A3: len x = len y and
A4: x in dom f;
A5: y is Element of (len y)-tuples_on NAT by FINSEQ_2:92;
len x = 0 by A4;
hence thesis by A3,A5;
end;
take f;
thus thesis by A2;
end;
end;
registration
cluster -> to-naturals NAT*-defined for PartFunc of NAT*, NAT;
coherence;
end;
registration
cluster quasi_total -> len-total for PartFunc of NAT*,NAT;
coherence;
end;
theorem Th16:
for g being len-total to-naturals NAT*-defined Function holds
g is quasi_total PartFunc of NAT*, NAT
proof
let g be len-total to-naturals NAT*-defined Function;
A1: rng g c= NAT by VALUED_0:def 6;
dom g c= NAT*;
then reconsider g9 = g as PartFunc of NAT*, NAT by A1,RELSET_1:4;
for x,y being FinSequence of NAT st len x = len y & x in dom g holds y
in dom g by Def2;
then g9 is quasi_total;
hence thesis;
end;
theorem Th17:
arity {} = 0
proof
not ex x being FinSequence st x in dom {};
hence thesis by MARGREL1:def 25;
end;
theorem Th18:
for f being homogeneous Relation st dom f = {{}} holds arity f = 0
proof
let f be homogeneous Relation;
assume dom f = {{}};
then {} in dom f by TARSKI:def 1;
hence thesis by CARD_1:27,MARGREL1:def 25;
end;
theorem Th19:
for f being homogeneous PartFunc of X*,Y holds dom f c= (arity f)-tuples_on X
proof
let f be homogeneous PartFunc of X*, Y;
let x be object;
assume
A1: x in dom f;
per cases;
suppose
A2: X is empty;
then x = <*>(X*) by A1,FUNCT_7:17,TARSKI:def 1;
then
A3: arity f = len <*>(X*) by A1,MARGREL1:def 25;
0-tuples_on X = {{}} by Th5;
hence thesis by A1,A2,A3,FUNCT_7:17;
end;
suppose
X is non empty;
then reconsider X9 = X as non empty set;
reconsider x9 = x as FinSequence of X9 by A1,FINSEQ_1:def 11;
len x9 = arity f by A1,MARGREL1:def 25;
then x9 is Element of (arity f)-tuples_on X9 by FINSEQ_2:92;
hence thesis;
end;
end;
theorem Th20:
for f being homogeneous NAT*-defined Function holds
dom f c= (arity f)-tuples_on NAT
proof
let f be homogeneous NAT*-defined Function;
let x be object;
assume
A1: x in dom f;
reconsider x9 = x as FinSequence of NAT by A1,FINSEQ_1:def 11;
len x9 = arity f by A1,MARGREL1:def 25;
then x9 is Element of (arity f)-tuples_on NAT by FINSEQ_2:92;
hence thesis;
end;
Lm1: for f being homogeneous PartFunc of D*, D holds f is quasi_total non
empty iff dom f = (arity f)-tuples_on D
proof
set X = D;
let f being homogeneous PartFunc of X*, X;
A1: dom f c= (arity f)-tuples_on X by Th19;
hereby
assume f is quasi_total non empty;
then reconsider
f9 = f as quasi_total non empty homogeneous PartFunc of X*, X;
consider x being object such that
A2: x in dom f9 by XBOOLE_0:def 1;
reconsider x9 = x as FinSequence of X by A2,FINSEQ_1:def 11;
A3: len x9 = arity f by A2,MARGREL1:def 25;
now
let z be object;
thus z in dom f implies z in (arity f)-tuples_on X by A1;
assume z in (arity f)-tuples_on X;
then reconsider z9 = z as Element of (arity f)-tuples_on X;
len z9=arity f by CARD_1:def 7;
hence z in dom f by A2,A3,MARGREL1:def 22;
end;
hence dom f = (arity f)-tuples_on X;
end;
assume
A4: dom f = (arity f)-tuples_on X;
thus f is quasi_total
proof
let x, y be FinSequence of X;
assume that
A5: len x = len y and
A6: x in dom f;
len x = arity f by A4,A6,CARD_1:def 7;
then y is Element of (arity f)-tuples_on X by A5,FINSEQ_2:92;
hence y in dom f by A4;
end;
thus thesis by A4;
end;
theorem Th21:
for f being homogeneous PartFunc of X*, X holds
f is quasi_total non empty iff dom f = (arity f)-tuples_on X
proof
let f be homogeneous PartFunc of X*, X;
per cases;
suppose
X is empty;
then f = {};
hence thesis by Th5,Th17;
end;
suppose
X is non empty;
hence thesis by Lm1;
end;
end;
theorem Th22:
for f being homogeneous to-naturals NAT*-defined Function holds
f is len-total non empty iff dom f = (arity f)-tuples_on NAT
proof
let f being homogeneous to-naturals NAT*-defined Function;
A1: dom f c= (arity f)-tuples_on NAT by Th20;
hereby
assume f is len-total non empty;
then reconsider
f9 = f as quasi_total non empty homogeneous PartFunc of NAT*,
NAT by Th16;
consider x being object such that
A2: x in dom f9 by XBOOLE_0:def 1;
reconsider x9 = x as FinSequence of NAT by A2,FINSEQ_1:def 11;
A3: len x9 = arity f by A2,MARGREL1:def 25;
now
let z be object;
thus z in dom f implies z in (arity f)-tuples_on NAT by A1;
assume z in (arity f)-tuples_on NAT;
then reconsider z9 = z as Element of (arity f)-tuples_on NAT;
len z9 = arity f by CARD_1:def 7;
hence z in dom f by A2,A3,MARGREL1:def 22;
end;
hence dom f = (arity f)-tuples_on NAT;
end;
assume
A4: dom f = (arity f)-tuples_on NAT;
thus f is len-total
proof
let x, y be FinSequence of NAT;
assume that
A5: len x = len y and
A6: x in dom f;
len x = arity f by A4,A6,CARD_1:def 7;
then y is Element of (arity f)-tuples_on NAT by A5,FINSEQ_2:92;
hence thesis by A4;
end;
thus thesis by A4;
end;
theorem
for f being non empty homogeneous PartFunc of D*, D, n
st dom f c= n-tuples_on D holds arity f = n
proof
let f be non empty homogeneous PartFunc of D*, D, n;
consider x being object such that
A1: x in dom f by XBOOLE_0:def 1;
assume
A2: dom f c= n-tuples_on D;
then
A3: for x being FinSequence st x in dom f holds n = len x by CARD_1:def 7;
reconsider x as Element of n-tuples_on D by A2,A1;
x in dom f by A1;
hence thesis by A3,MARGREL1:def 25;
end;
theorem Th24:
for f being homogeneous PartFunc of D*, D, n
st dom f = n-tuples_on D holds arity f = n
proof
let f be homogeneous PartFunc of D*, D, n;
consider x being object such that
A1: x in n-tuples_on D by XBOOLE_0:def 1;
reconsider x as Element of n-tuples_on D by A1;
assume
A2: dom f = n-tuples_on D;
then
A3: for x be FinSequence st x in dom f holds len x = n by CARD_1:def 7;
x in dom f by A2;
hence thesis by A3,MARGREL1:def 25;
end;
definition
let R be Relation;
attr R is with_the_same_arity means
:Def3:
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;
coherence;
end;
registration
let X be set;
cluster with_the_same_arity for FinSequence of X;
existence
proof
take <*>X;
thus thesis;
end;
cluster with_the_same_arity for Element of X*;
existence
proof
reconsider p = <*>X as Element of X* by FINSEQ_1:def 11;
take p;
thus thesis;
end;
end;
definition
let F be with_the_same_arity Relation;
func arity F -> Element of NAT means
:Def4:
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
proof
hereby
given f being homogeneous Function such that
A1: f in rng F;
take i = arity f;
let g be homogeneous Function;
assume
A2: g in rng F;
per cases;
suppose
A3: f is empty;
thus i = arity g
proof
per cases by A1,A2,A3,Def3;
suppose
g is empty;
hence thesis by A3;
end;
suppose
dom g = {{}};
hence thesis by A3,Th17,Th18;
end;
end;
end;
suppose
A4: g is empty;
thus i = arity g
proof
per cases by A1,A2,A4,Def3;
suppose
f is empty;
hence thesis by A4;
end;
suppose
dom f = {{}};
hence thesis by A4,Th17,Th18;
end;
end;
end;
suppose
A5: f is non empty & g is non empty;
set a = the Element of dom f;
dom f <> {} by A5;
then
A6: a in dom f;
consider n being Element of NAT, X being non empty set such that
A7: dom f c= n-tuples_on X and
A8: dom g c= n-tuples_on X by A1,A2,A5,Def3;
reconsider a as Element of n-tuples_on X by A7,A6;
A9: arity f = len a by A5,MARGREL1:def 25
.= n by CARD_1:def 7;
set a = the Element of dom g;
dom g <> {} by A5;
then a in dom g;
then reconsider a as Element of n-tuples_on X by A8;
arity g = len a by A5,MARGREL1:def 25;
hence i = arity g by A9,CARD_1:def 7;
end;
end;
thus thesis;
end;
uniqueness
proof
let i1, i2 be Element of NAT;
hereby
given f being homogeneous Function such that
A10: f in rng F;
assume for f being homogeneous Function st f in rng F holds i1 = arity f;
then i1 = arity f by A10;
hence
(for f being homogeneous Function st f in rng F holds i2 = arity f)
implies i1 = i2 by A10;
end;
thus thesis;
end;
correctness;
end;
theorem
for F be with_the_same_arity FinSequence st len F = 0 holds arity F = 0
proof
let F be with_the_same_arity FinSequence;
assume len F = 0;
then F = {};
then for f being homogeneous Function holds not f in rng F;
hence thesis by Def4;
end;
definition
let X be set;
func HFuncs X -> PFUNC_DOMAIN of X*, X equals
{f where f is Element of PFuncs(X*, X): f is homogeneous};
coherence
proof
set H = {f where f is Element of PFuncs(X*, X): f is homogeneous};
H is non empty functional
proof
{} is PartFunc of X* ,X by RELSET_1:12;
then {} in PFuncs(X*, X) by PARTFUN1:45;
then {} in H;
hence H is non empty;
let x be object;
assume x in H;
then ex g being Element of PFuncs(X*, X) st x = g & g is homogeneous;
hence thesis;
end;
then reconsider H as non empty functional set;
now
let f be Element of H;
f in H;
then ex g being Element of PFuncs(X*, X) st f = g & g is homogeneous;
hence f is PartFunc of X*, X;
end;
hence thesis by RFUNCT_3:def 3;
end;
end;
theorem
{} in HFuncs X
proof
set f = {};
reconsider f as PartFunc of X*, X by XBOOLE_1:2;
reconsider f as Element of PFuncs(X*, X) by PARTFUN1:45;
f in {g where g is Element of PFuncs(X*, X): g is homogeneous};
hence thesis;
end;
registration
let X be non empty set;
cluster non empty homogeneous quasi_total for Element of HFuncs X;
existence
proof
set p = <*>X;
set x = the Element of X;
p in X* by FINSEQ_1:def 11;
then reconsider Y = {p} as Subset of X* by ZFMISC_1:31;
A1: Y --> x in PFuncs(X*, X);
p .--> x is homogeneous;
then
{p} --> x in {f where f is Element of PFuncs(X* , X): f is homogeneous
} by A1;
then reconsider f = p .--> x as Element of HFuncs X;
take f;
thus f is non empty homogeneous;
let a,b be FinSequence of X such that
A3: len a = len b;
assume a in dom f;
then a = p by TARSKI:def 1;
then b = {} by A3;
hence thesis by TARSKI:def 1;
end;
end;
registration
let X be set;
cluster -> homogeneous for Element of HFuncs X;
coherence
proof
let f be Element of HFuncs X;
f in HFuncs X;
then ex g being Element of PFuncs(X*, X) st f = g & g is homogeneous;
hence thesis;
end;
end;
registration
let X be non empty set, S be non empty Subset of HFuncs X;
cluster -> homogeneous for Element of S;
coherence;
end;
theorem Th27:
for f being to-naturals homogeneous NAT*-defined Function holds
f is Element of HFuncs NAT
proof
let f be to-naturals homogeneous NAT*-defined Function;
A1: rng f c= NAT by VALUED_0:def 6;
dom f c= NAT*;
then f is PartFunc of NAT*,NAT by A1,RELSET_1:4;
then reconsider f9=f as Element of PFuncs(NAT*,NAT) by PARTFUN1:45;
f9 in {f1 where f1 is Element of PFuncs(NAT*,NAT): f1 is homogeneous};
hence thesis;
end;
theorem Th28:
for f being len-total to-naturals homogeneous NAT*-defined Function holds
f is quasi_total Element of HFuncs NAT
proof
let f be len-total to-naturals homogeneous NAT*-defined Function;
reconsider f9=f as Element of HFuncs NAT by Th27;
f9 is quasi_total
by Def2;
hence thesis;
end;
theorem Th29:
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
proof
let X be non empty set, R be Relation such that
A1: rng R c= HFuncs X and
A2: for f,g being homogeneous Function st f in rng R & g in rng R holds
arity f = arity g;
let f,g be Function;
assume that
A3: f in rng R and
A4: g in rng R;
reconsider f9 = f, g9 = g as Element of HFuncs X by A1,A3,A4;
A5: arity f9 = arity g9 by A2,A3,A4;
hereby
assume f is empty;
then dom g9 c= 0-tuples_on X by A5,Th17,Th19;
then dom g9 c= {<*>X} by FINSEQ_2:94;
hence g is empty or dom g = {{}} by ZFMISC_1:33;
end;
assume that
A6: f is non empty and
g is non empty;
reconsider f9 as non empty Element of HFuncs X by A6;
take arity f9, X;
thus thesis by A5,Th19;
end;
definition
let n, m be Nat;
func n const m -> homogeneous to-naturals NAT*-defined Function equals
(n-tuples_on NAT) --> m;
coherence
proof
set X=NAT;
set f = (n-tuples_on X)-->m;
A1: n-tuples_on X c= X* by FINSEQ_2:142;
f is homogeneous;
hence thesis by A1,RELAT_1:def 18;
end;
end;
theorem Th30:
n const m in HFuncs NAT
proof
set X=NAT;
set f=n const m;
A1: rng f c= NAT by VALUED_0:def 6;
dom f c= NAT*;
then f is PartFunc of X*, X by A1,RELSET_1:4;
then f is Element of PFuncs(X*, X) by PARTFUN1:45;
hence thesis;
end;
registration
let n,m be Nat;
cluster n const m -> len-total non empty;
coherence
proof
set X = NAT;
n const m is len-total
proof
let x, y be FinSequence of X;
assume that
A2: len x = len y and
A3: x in dom (n const m);
len x = n by A3,CARD_1:def 7;
then y is Element of n-tuples_on X by A2,FINSEQ_2:92;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th31:
arity (n const m) = n
proof
set d = the Element of n-tuples_on NAT;
A2: for x be FinSequence st x in dom (n const m) holds n=len x by CARD_1:def 7;
d in dom (n const m);
hence thesis by A2,MARGREL1:def 25;
end;
registration
let n,m;
reduce arity (n const m) to n;
reducibility by Th31;
end;
registration
cluster -> homogeneous to-naturals NAT*-defined for Element of HFuncs NAT;
coherence;
end;
definition
let n, i be Nat;
func n succ i -> homogeneous to-naturals NAT*-defined Function means
:Def7:
dom it = n-tuples_on NAT &
for p being Element of n-tuples_on NAT holds it.p = (p.i)+1;
existence
proof
deffunc f(Element of NAT*) = ($1.i)+1;
defpred p[set] means $1 in n-tuples_on NAT;
consider f being PartFunc of NAT*, NAT such that
A1: for d being Element of NAT* holds d in dom f iff p[d] and
A2: for d being Element of NAT* st d in dom f holds f/.d = f(d)
from PARTFUN2:sch 2;
A3: n-tuples_on NAT c= NAT* by FINSEQ_2:142;
then
A4: for x be object holds x in dom f iff x in n-tuples_on NAT by A1;
then
A5: dom f = n-tuples_on NAT by TARSKI:2;
reconsider f as Element of PFuncs(NAT*, NAT) by PARTFUN1:45;
f is homogeneous by A5;
then f in {g where g is Element of PFuncs(NAT*,NAT):g is homogeneous};
then reconsider f as Element of HFuncs NAT;
take f;
thus dom f = n-tuples_on NAT by A4;
let p be Element of n-tuples_on NAT;
reconsider p9 = p as Element of NAT* by A3;
thus f.p = f/.p9 by A5,PARTFUN1:def 6
.= (p.i)+1 by A2,A5;
end;
uniqueness
proof
let it1, it2 be homogeneous to-naturals NAT*-defined Function such that
A6: dom it1 = n-tuples_on NAT and
A7: for p being Element of n-tuples_on NAT holds it1.p = (p.i)+1 and
A8: dom it2 = n-tuples_on NAT and
A9: for p being Element of n-tuples_on NAT holds it2.p = (p.i)+1;
now
let x be object;
assume x in n-tuples_on NAT;
then reconsider x9 = x as Element of n-tuples_on NAT;
thus it1.x = (x9.i)+1 by A7
.= it2.x by A9;
end;
hence thesis by A6,A8;
end;
end;
theorem Th32:
n succ i in HFuncs NAT
proof
set X=NAT;
set f=n succ i;
A1: rng f c= NAT by VALUED_0:def 6;
dom f c= NAT*;
then f is PartFunc of X*, X by A1,RELSET_1:4;
then f is Element of PFuncs(X*, X) by PARTFUN1:45;
hence thesis;
end;
registration
let n,i be Nat;
cluster n succ i -> len-total non empty;
coherence
proof
A1: dom (n succ i) = n-tuples_on NAT by Def7;
(n succ i) is len-total
proof
let x, y be FinSequence of NAT;
assume that
A2: len x = len y and
A3: x in dom (n succ i);
len x = n by A1,A3,CARD_1:def 7;
then y is Element of n-tuples_on NAT by A2,FINSEQ_2:92;
hence thesis by A1;
end;
hence thesis by A1;
end;
end;
theorem Th33:
arity (n succ i) = n
proof
consider d being object such that
A1: d in dom (n succ i) by XBOOLE_0:def 1;
reconsider d as Element of n-tuples_on NAT by A1,Def7;
dom (n succ i) = n-tuples_on NAT by Def7;
then
A2: for y be FinSequence st y in dom (n succ i) holds n= len y by CARD_1:def 7;
d in dom (n succ i) by A1;
hence thesis by A2,MARGREL1:def 25;
end;
registration
let n,i;
reduce arity (n succ i) to n;
reducibility by Th33;
end;
definition
let n, i be Nat;
func n proj i -> homogeneous to-naturals NAT*-defined Function equals
proj(n|->NAT, i);
correctness
proof
A1: dom proj(n|->NAT, i) = product(n|->NAT) by CARD_3:def 16
.= n-tuples_on NAT by FINSEQ_3:131;
now
set P = proj(n|->NAT, i);
A2: rng P c= NAT
proof
let x be object;
assume x in rng P;
then consider d being object such that
A3: d in dom P and
A4: x = P.d by FUNCT_1:def 3;
reconsider d as Element of n-tuples_on NAT by A1,A3;
reconsider d as FinSequence of NAT;
P.d = d.i by A3,CARD_3:def 16;
hence thesis by A4;
end;
A5: P is homogeneous
proof
thus dom P is with_common_domain;
end;
reconsider P as PartFunc of NAT*, NAT by A1,A2,FINSEQ_2:142,RELSET_1:4;
P is Element of PFuncs(NAT*, NAT) by PARTFUN1:45;
then P in HFuncs NAT by A5;
hence proj(n|->NAT, i) is Element of HFuncs NAT;
end;
hence thesis;
end;
end;
theorem Th34:
n proj i in HFuncs NAT
proof
set X=NAT;
set f=n proj i;
A1: rng f c= NAT by VALUED_0:def 6;
dom f c= NAT*;
then f is PartFunc of X*, X by A1,RELSET_1:4;
then f is Element of PFuncs(X*, X) by PARTFUN1:45;
hence thesis;
end;
theorem Th35:
dom (n proj i) = n-tuples_on NAT &
(1 <= i & i <= n implies rng (n proj i) = NAT)
proof
thus
A1: dom (n proj i)= product(n|->NAT) by CARD_3:def 16
.= n-tuples_on NAT by FINSEQ_3:131;
assume that
A2: 1 <= i and
A3: i <= n;
now
let x be object;
thus x in rng (n proj i) implies x in NAT
by ORDINAL1:def 12;
assume x in NAT;
then reconsider x9 = x as Element of NAT;
reconsider d = n |-> x9 as FinSequence of NAT;
i in Seg n by A2,A3,FINSEQ_1:1;
then
A4: d.i = x9 by FUNCOP_1:7;
(n proj i).d = d.i by A1,CARD_3:def 16;
hence x in rng (n proj i) by A1,A4,FUNCT_1:def 3;
end;
hence thesis by TARSKI:2;
end;
registration
let n,i be Nat;
cluster n proj i -> len-total non empty;
coherence
proof
A1: dom (n proj i) = n-tuples_on NAT by Th35;
n proj i is len-total
proof
let x, y be FinSequence of NAT;
assume that
A2: len x=len y and
A3: x in dom (n proj i);
len x=n by A1,A3,CARD_1:def 7;
then y is Element of n-tuples_on NAT by A2,FINSEQ_2:92;
hence thesis by A1;
end;
hence thesis by A1;
end;
end;
theorem Th36:
arity (n proj i) = n
proof
consider d being object such that
A1: d in n-tuples_on NAT by XBOOLE_0:def 1;
reconsider d as Element of n-tuples_on NAT by A1;
A2: dom (n proj i) = n-tuples_on NAT by Th35;
then
A3: for x be FinSequence st x in dom (n proj i) holds n= len x by CARD_1:def 7;
d in dom (n proj i) by A2;
hence thesis by A3,MARGREL1:def 25;
end;
registration
let n,i;
reduce arity (n proj i) to n;
reducibility by Th36;
end;
theorem Th37:
for t being Element of n-tuples_on NAT holds (n proj i).t = t.i
proof
let t be Element of n-tuples_on NAT;
dom (n proj i) = n-tuples_on NAT by Th35;
hence thesis by CARD_3:def 16;
end;
registration
let X be set;
cluster HFuncs X -> functional;
coherence;
end;
theorem Th38:
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
proof
set X = D, Y = E;
let F be Function of X, HFuncs Y;
assume
A1: rng F is compatible;
assume
A2: for x being Element of X holds dom (F.x) c= n-tuples_on Y;
A3: rng F is functional
proof
let x be object;
A4: rng F c= HFuncs Y by RELAT_1:def 19;
assume x in rng F;
hence thesis by A4;
end;
then reconsider rngF = rng F as non empty functional compatible set by A1;
set D = the set of all dom g where g is Element of rngF;
reconsider f = Union F as Function by A1,A3;
A5: rng f c= Y
proof
let y be object;
assume y in rng f;
then consider x being object such that
A6: x in dom f and
A7: f.x = y by FUNCT_1:def 3;
x in union D by A6,Th11;
then consider d being set such that
A8: x in d and
A9: d in D by TARSKI:def 4;
consider g being Element of rngF such that
A10: d = dom g by A9;
rng F c= HFuncs Y by RELAT_1:def 19;
then reconsider g as Element of HFuncs Y;
A11: g.x in rng g by A8,A10,FUNCT_1:3;
A12: rng g c= Y by RELAT_1:def 19;
f.x = g.x by A8,A10,Th12;
hence thesis by A7,A12,A11;
end;
A13: dom f c= n-tuples_on Y
proof
let x be object;
assume x in dom f;
then x in union D by Th11;
then consider d being set such that
A14: x in d and
A15: d in D by TARSKI:def 4;
consider g being Element of rngF such that
A16: d = dom g by A15;
consider e being object such that
A17: e in dom F and
A18: F.e = g by FUNCT_1:def 3;
reconsider e as Element of X by A17;
dom (F.e) c= n-tuples_on Y by A2;
hence thesis by A14,A16,A18;
end;
n-tuples_on Y c= Y* by FINSEQ_2:142;
then dom f c= Y* by A13;
then reconsider f as PartFunc of Y*, Y by A5,RELSET_1:4;
reconsider f as Element of PFuncs(Y*, Y) by PARTFUN1:45;
f is homogeneous
by A13;
then f in {g where g is Element of PFuncs(Y*, Y): g is homogeneous};
then reconsider f = Union F as Element of HFuncs Y;
take f;
thus f = Union F;
thus thesis by A13;
end;
theorem
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
proof
set X = D;
let F be sequence of HFuncs X such that
A1: for i being Nat holds F.i c= F.(i+1);
A2: now
let n be Element of NAT;
defpred p[Nat] means F.n c= F.(n+$1);
let m be Element of NAT;
A3: now
let i be Nat such that
A4: p[i];
F.(n+i) c= F.(n+i+1) by A1;
hence p[i+1] by A4,XBOOLE_1:1;
end;
A5: p[0];
A6: for i being Nat holds p[i] from NAT_1:sch 2(A5,A3);
assume n <= m;
then consider i being Nat such that
A7: m = n+i by NAT_1:10;
thus F.n c= F.m by A6,A7;
end;
reconsider Y = rng F as non empty Subset of HFuncs X by RELAT_1:def 19;
A8: Y is compatible
proof
let f,g be Function;
assume f in Y;
then consider i being object such that
A9: i in dom F and
A10: f = F.i by FUNCT_1:def 3;
assume g in Y;
then consider j being object such that
A11: j in dom F and
A12: g = F.j by FUNCT_1:def 3;
reconsider i,j as Element of NAT by A9,A11;
i <= j or j <= i;
hence thesis by A2,A10,A12,PARTFUN1:54;
end;
Y is PartFunc-set of X*, X
proof
let f be Element of Y;
f is Element of HFuncs X;
hence thesis;
end;
then Union F is PartFunc of X*, X by A8,Th14;
then reconsider f = Union F as Element of PFuncs(X*, X) by PARTFUN1:45;
A13: dom f=union the set of all dom g where g is Element of Y by A8,Th11;
f is homogeneous
proof
thus dom f is with_common_domain
proof
let x,y be FinSequence;
assume x in dom f;
then consider A1 being set such that
A14: x in A1 and
A15: A1 in the set of all dom g where g is Element of Y by A13,
TARSKI:def 4;
consider g1 being Element of Y such that
A16: A1 = dom g1 by A15;
assume y in dom f;
then consider A2 being set such that
A17: y in A2 and
A18: A2 in the set of all dom g where g is Element of Y by A13,
TARSKI:def 4;
consider g2 being Element of Y such that
A19: A2 = dom g2 by A18;
consider i1 being object such that
A20: i1 in dom F and
A21: g1 = F.i1 by FUNCT_1:def 3;
consider i2 being object such that
A22: i2 in dom F and
A23: g2 = F.i2 by FUNCT_1:def 3;
reconsider i1, i2 as Element of NAT by A20,A22;
i1 <= i2 or i2 <= i1;
then g1 c= g2 or g2 c= g1 by A2,A21,A23;
then dom g1 c= dom g2 or dom g2 c= dom g1 by GRFUNC_1:2;
then dom x = dom y by A14,A16,A17,A19,CARD_3:def 10;
hence len x = len y by FINSEQ_3:29;
end;
end;
hence thesis;
end;
theorem Th40:
for F being with_the_same_arity FinSequence of HFuncs D holds
dom <:F:> c= (arity F)-tuples_on D
proof
set X = D;
let F be with_the_same_arity FinSequence of HFuncs X;
thus dom <:F:> c= (arity F)-tuples_on X
proof
A1: dom <:F:> = meet doms F by FUNCT_6:29
.= meet rng doms F by FUNCT_6:def 4;
let x be object such that
A2: x in dom <:F:>;
consider y being object such that
A3: y in rng doms F by A2,A1,SETFAM_1:1,XBOOLE_0:def 1;
reconsider y as set by TARSKI:1;
A4: x in y by A2,A1,A3,SETFAM_1:def 1;
consider z being object such that
A5: z in dom doms F and
A6: (doms F).z = y by A3,FUNCT_1:def 3;
A7: dom doms F=dom F by FUNCT_6:def 2;
then z in dom F by A5;
then
A8: F.z in rng F by FUNCT_1:3;
rng F c= HFuncs X by RELAT_1:def 19;
then reconsider Fz = F.z as Element of HFuncs X by A8;
A9: dom Fz c= (arity Fz)-tuples_on X by Th19;
(doms F).z = dom Fz by A7,A5,FUNCT_6:def 2;
then x in (arity Fz)-tuples_on X by A6,A4,A9;
hence thesis by A8,Def4;
end;
end;
registration
let X be non empty set;
let F be with_the_same_arity FinSequence of HFuncs X;
cluster <:F:> -> homogeneous;
coherence
proof
dom <:F:> c= (arity F)-tuples_on X by Th40;
hence dom<:F:> is with_common_domain;
end;
end;
theorem Th41:
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
proof
set X = D;
let f be Element of HFuncs X;
let F be with_the_same_arity FinSequence of HFuncs X;
A1: dom (f*<:F:>) c=dom <:F:> by RELAT_1:25;
A2: (arity F)-tuples_on X c= X* by FINSEQ_2:142;
dom <:F:> c=(arity F)-tuples_on X by Th40;
hence dom (f*<:F:>) c= (arity F)-tuples_on X by A1;
then
A3: dom (f*<:F:>) c= X* by A2;
thus rng (f*<:F:>) c= X by RELAT_1:def 19;
then f*<:F:> is PartFunc of X*, X by A3,RELSET_1:4;
then f*<:F:> in PFuncs(X*, X) by PARTFUN1:45;
hence thesis;
end;
definition
let X,Y be non empty set, P be PFUNC_DOMAIN of X,Y;
let S be non empty Subset of P;
redefine mode Element of S -> Element of P; :: redefines Element (SUBSET_1, definition)
coherence
proof
let f be Element of S;
thus thesis;
end;
end;
registration
let f be homogeneous NAT*-defined Function;
cluster <*f*> -> with_the_same_arity;
coherence
proof
let h,g be Function such that
A1: h in rng <*f*> and
A2: g in rng <*f*>;
A3: rng <*f*> = {f} by FINSEQ_1:39;
then
A4: h = f by A1,TARSKI:def 1;
hence h is empty implies g is empty or dom g = {{}} by A2,A3,TARSKI:def 1;
assume that
h is non empty and
g is non empty;
take arity f,NAT;
g = f by A2,A3,TARSKI:def 1;
hence thesis by A4,Th20;
end;
end;
theorem
for f being homogeneous to-naturals NAT*-defined Function holds
arity <*f*> = arity f
proof
let f be homogeneous to-naturals NAT*-defined Function;
rng <*f*> = {f} by FINSEQ_1:38;
then f in rng <*f*> by TARSKI:def 1;
hence thesis by Def4;
end;
theorem Th43:
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
proof
let f, g be non empty Element of HFuncs NAT, F be with_the_same_arity
FinSequence of HFuncs NAT;
assume g = f*<:F:>;
then
A1: dom g c= (arity F)-tuples_on NAT by Th41;
consider x being object such that
A2: x in dom g by XBOOLE_0:def 1;
reconsider x as Element of (arity F)-tuples_on NAT by A1,A2;
len x = arity F by CARD_1:def 7;
hence thesis by A2,MARGREL1:def 25;
end;
theorem Th44:
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
proof
set X = D;
let f being non empty quasi_total Element of HFuncs X, F being
with_the_same_arity FinSequence of HFuncs X such that
A1: arity f = len F and
A2: F is non empty and
A3: for h being Element of HFuncs X st h in rng F holds h is quasi_total
non empty;
set n = arity F;
set fF = f*<:F:>;
A4: dom fF c= n-tuples_on X by Th41;
A5: n-tuples_on X c= dom fF
proof
let x be object;
A6: product rngs F c= (len F)-tuples_on X
proof
let p be object;
A7: dom rngs F = dom F by FUNCT_6:def 3;
assume p in product rngs F;
then consider g being Function such that
A8: p = g and
A9: dom g = dom rngs F and
A10: for x being object st x in dom rngs F holds g.x in (rngs F).x by
CARD_3:def 5;
A11: dom F = Seg len F by FINSEQ_1:def 3;
then reconsider g as FinSequence by A9,A7,FINSEQ_1:def 2;
rng g c= X
proof
let x be object;
assume x in rng g;
then consider d being object such that
A12: d in dom g and
A13: g.d = x by FUNCT_1:def 3;
A14: g.d in (rngs F).d by A9,A10,A12;
reconsider d as Element of NAT by A12;
reconsider Fd = F.d as Element of HFuncs X by A9,A7,A12,
FINSEQ_2:11;
A15: rng Fd c= X by RELAT_1:def 19;
(rngs F).d = rng Fd by A9,A7,A12,FUNCT_6:def 3;
hence thesis by A13,A14,A15;
end;
then reconsider g as FinSequence of X by FINSEQ_1:def 4;
len g = len F by A9,A7,A11,FINSEQ_1:def 3;
then p is Element of (len F)-tuples_on X by A8,FINSEQ_2:92;
hence thesis;
end;
rng <:F:> c= product rngs F by FUNCT_6:29;
then
A16: rng <:F:> c= (len F)-tuples_on X by A6;
A17: dom f = (arity f)-tuples_on X by Th21;
A18: n-tuples_on X c= dom <:F:>
proof
let x be object;
A19: dom doms F = dom F by FUNCT_6:def 2;
assume
A20: x in n-tuples_on X;
A21: now
let y be set;
assume y in rng doms F;
then consider w being object such that
A22: w in dom doms F and
A23: (doms F).w = y by FUNCT_1:def 3;
A24: w in dom F by A19,A22;
then reconsider w as Element of NAT;
reconsider Fw = F.w as Element of HFuncs X by A24,FINSEQ_2:11;
A25: (doms F).w = dom (Fw) by A19,A22,FUNCT_6:def 2;
A26: Fw in rng F by A24,FUNCT_1:3;
then Fw is non empty quasi_total by A3;
then dom (Fw) = (arity Fw)-tuples_on X by Th21;
hence x in y by A20,A23,A25,A26,Def4;
end;
consider z being object such that
A27: z in dom F by A2,XBOOLE_0:def 1;
z in dom doms F by A27,A19;
then
A28: rng doms F <> {} by RELAT_1:42;
dom <:F:> = meet doms F by FUNCT_6:29
.= meet rng doms F by FUNCT_6:def 4;
hence thesis by A28,A21,SETFAM_1:def 1;
end;
assume
A29: x in n-tuples_on X;
then <:F:>.x in rng <:F:> by A18,FUNCT_1:3;
hence thesis by A1,A29,A18,A17,A16,FUNCT_1:11;
end;
then
A30: dom fF = n-tuples_on X by A4,XBOOLE_0:def 10;
A31: rng fF c= X by Th41;
(arity F)-tuples_on X c= X* by FINSEQ_2:142;
then dom fF c= X* by A4;
then fF is Relation of X*, X by A31,RELSET_1:4;
then fF is Element of PFuncs(X*, X) by PARTFUN1:45;
then fF in HFuncs X;
then reconsider fF as Element of HFuncs X;
fF is quasi_total
proof
let x, y be FinSequence of X such that
A32: len x = len y and
A33: x in dom fF;
len x = n by A4,A33,CARD_1:def 7;
then y is Element of n-tuples_on X by A32,FINSEQ_2:92;
hence y in dom fF by A30;
end;
hence f*<:F:> is non empty quasi_total Element of HFuncs X by A5;
thus thesis by A4,A5,XBOOLE_0:def 10;
end;
theorem Th45:
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
proof
set X = D;
let f being quasi_total Element of HFuncs X, F being with_the_same_arity
FinSequence of HFuncs X such that
A1: arity f = len F and
A2: for h being Element of HFuncs X st h in rng F holds h is quasi_total;
reconsider g = {} as PartFunc of X*, X by RELSET_1:12;
A3: g is quasi_total;
g in PFuncs(X*, X) by PARTFUN1:45;
then
A4: g in {h where h is Element of PFuncs(X*, X): h is homogeneous};
per cases;
suppose
f = {};
hence thesis;
end;
suppose
F = {};
hence thesis by A4,A3,FUNCT_6:40;
end;
suppose
ex h being set st h in rng F & h = {};
then <:F:> = {} by Th7;
hence thesis by A4,A3;
end;
suppose
A5: F <> {} & f <> {} & for h being set st h in rng F holds h <> {};
then
for h be Element of HFuncs X st h in rng F holds h is quasi_total non
empty by A2;
hence thesis by A1,A5,Th44;
end;
end;
theorem Th46:
for f,g being non empty quasi_total Element of HFuncs D
st arity f = 0 & arity g = 0 & f.{} = g.{} holds f = g
proof
set X = D;
let f,g be non empty quasi_total Element of HFuncs X;
assume that
A1: arity f = 0 and
A2: arity g = 0 and
A3: f.{} = g.{};
now
thus dom f = 0-tuples_on X by A1,Th21
.= {<*>X} by FINSEQ_2:94;
thus dom g = 0-tuples_on X by A2,Th21
.= {<*>X} by FINSEQ_2:94;
let x be object;
assume x in {<*>X};
then x = {} by TARSKI:def 1;
hence f.x = g.x by A3;
end;
hence thesis;
end;
theorem Th47:
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
proof
let f,g be non empty len-total homogeneous to-naturals NAT*-defined
Function;
A1: g is non empty quasi_total Element of HFuncs NAT by Th28;
f is non empty quasi_total Element of HFuncs NAT by Th28;
hence thesis by A1,Th46;
end;
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 Nat;
pred g is_primitive-recursively_expressed_by f1,f2,i means
ex n being Element of NAT st dom g c= n-tuples_on NAT &
1 <= i & 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 m being Nat holds
(p+*(i,m+1) in dom g iff
p+*(i,m) in dom g & (p+*(i,m))^<*g.(p+*(i,m))*> in dom f2) &
(p+*(i,m+1) in dom g implies
g.(p+*(i,m+1)) = f2.((p+*(i,m))^<*g.(p+*(i,m))*>));
end;
defpred Q[Nat,Element of HFuncs NAT, Element of HFuncs NAT,
FinSequence of NAT, Nat, homogeneous Function] means ($5 in dom $4 &
$4+*($5,$1) in dom $2 & ($4+*($5,$1))^<*$2.($4+*($5,$1))*> in dom $6 implies $3
= $2+*($4+*($5,$1+1) .--> $6.(($4+*($5,$1))^<*$2.($4+*($5,$1))*>))) & (not $5
in dom $4 or not $4+*($5,$1) in dom $2 or not ($4+*($5,$1))^<*$2.($4+*($5,$1))
*> in dom $6 implies $3 = $2);
definition
let f1,f2 be homogeneous to-naturals NAT*-defined Function;
let i be Nat;
let p be FinSequence of NAT;
func primrec(f1,f2,i,p) -> Element of HFuncs NAT means
:Def10:
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);
existence
proof
reconsider ff1 = f1, ff2 = f2 as Element of HFuncs NAT by Th27;
set n = len p;
reconsider z = ff1.Del(p,i) as Element of NAT;
defpred A[Nat,Element of HFuncs NAT, Element of HFuncs NAT]
means Q[$1, $2, $3, p, i, ff2];
p+*(i,0) in NAT* by FINSEQ_1:def 11;
then reconsider Ap = {p+*(i,0)} as non empty Subset of NAT* by ZFMISC_1:31;
{} is PartFunc of NAT*, NAT by RELSET_1:12;
then {} in PFuncs(NAT*, NAT) by PARTFUN1:45;
then
A1: {} in HFuncs NAT;
Ap --> z = p+*(i,0) .--> z;
then Ap --> z in HFuncs NAT;
then reconsider t = Ap --> z, e = {} as Element of HFuncs NAT by A1;
i in dom p & Del(p,i) in dom f1 or not i in dom p or not Del(p,i) in
dom f1;
then consider A being Element of HFuncs NAT such that
A2: i in dom p & Del(p,i) in dom f1 implies A = t and
A3: not i in dom p or not Del(p,i) in dom f1 implies A = e;
A4: for m being Nat for x being Element of HFuncs NAT ex y
being Element of HFuncs NAT st A[m,x,y]
proof
let m be Nat, x be Element of HFuncs NAT;
set f= x+*({p+*(i,m+1)} --> f2.((p+*(i,m))^<*x.(p+*(i,m))*>));
reconsider z = ff2.((p+*(i,m))^<*x.(p+*(i,m))*>) as Element of NAT;
i in dom p & p+*(i,m) in dom x & (p+*(i,m))^<*x.(p+*(i,m))*> in dom
f2 or not i in dom p or not p+*(i,m) in dom x or not (p+*(i,m))^<*x.(p+*(i,m))
*> in dom f2;
then consider y being Function such that
A5: i in dom p & p+*(i,m) in dom x & (p+*(i,m))^<*x.(p+*(i,m))*> in
dom f2 & y = x+*({p+*(i,m+1)}--> f2.((p+*(i,m))^<*x.(p+*(i,m))*>)) or (not i in
dom p or not p+*(i,m) in dom x or not (p+*(i,m))^<*x.(p+*(i,m))*> in dom f2) &
y = x;
p+*(i,m+1) in NAT* by FINSEQ_1:def 11;
then reconsider B = {p+*(i,m+1)} as Subset of NAT* by ZFMISC_1:31;
dom (B --> z) = B;
then
A6: dom f = dom x \/ B by FUNCT_4:def 1;
dom p = dom (p+*(i,m+1)) by FUNCT_7:30;
then len (p+*(i,m+1)) = n by FINSEQ_3:29;
then p+*(i,m+1) is Element of n-tuples_on NAT by FINSEQ_2:92;
then
A7: B c= n-tuples_on NAT by ZFMISC_1:31;
A8: f = x+*(B --> z);
now
assume
A9: p+*(i,m) in dom x;
dom x c= n-tuples_on NAT
proof
let a be object;
A10: dom p = dom (p+*(i,m)) by FUNCT_7:30;
assume
A11: a in dom x;
then reconsider q = a as Element of NAT*;
len q = len (p+*(i,m)) by A9,A11,MARGREL1:def 1;
then len q = n by A10,FINSEQ_3:29;
hence thesis;
end;
then
A12: f is homogeneous by A7,A6,Th15,XBOOLE_1:8;
f in PFuncs(NAT*, NAT) by A8,PARTFUN1:45;
hence f in HFuncs NAT by A12;
end;
then reconsider y as Element of HFuncs NAT by A5;
take y;
thus i in dom p & p+*(i,m) in dom x & (p+*(i,m))^<*x.(p+*(i,m))*> in dom
ff2 implies y = x+*( p+*(i,m+1).-->ff2.((p+*(i,m))^<*x.(p+*(i,m))*>)) by A5;
thus not i in dom p or not p+*(i,m) in dom x or not (p+*(i,m))^<*x.(p+*(
i,m))*> in dom ff2 implies y = x by A5;
end;
consider FF being sequence of HFuncs NAT such that
A13: FF.0 = A and
A14: for m being Nat holds A[m,FF.m qua Element of HFuncs
NAT,FF.(m+1)qua Element of HFuncs NAT] from RECDEF_1:sch 2(A4);
take FF.(p/.i), FF;
thus thesis by A2,A3,A13,A14;
end;
uniqueness
proof
reconsider ff2 = f2 as Element of HFuncs NAT by Th27;
let g1,g2 be Element of HFuncs NAT;
given F1 being sequence of HFuncs NAT such that
A15: g1 = F1.(p/.i) and
A16: i in dom p & Del(p,i) in dom f1 implies F1.0 = p+*(i,0) .--> (f1.
Del(p,i)) and
A17: not i in dom p or not Del(p,i) in dom f1 implies F1.0 = {} and
A18: for m being Nat holds Q[m, F1.m qua Element of HFuncs
NAT, F1.(m+1) qua Element of HFuncs NAT, p, i, f2];
given F2 being sequence of HFuncs NAT such that
A19: g2 = F2.(p/.i) and
A20: i in dom p & Del(p,i) in dom f1 implies F2.0 = p+*(i,0) .--> (f1.
Del(p,i)) and
A21: not i in dom p or not Del(p,i) in dom f1 implies F2.0 = {} and
A22: for m being Nat holds Q[m, F2.m qua Element of HFuncs
NAT, F2.(m+1) qua Element of HFuncs NAT, p, i, f2];
defpred p[Nat] means F1.$1 = F2.$1;
A23: now
let m be Nat;
assume p[m];
then
A24: Q[m, F1.m qua Element of HFuncs NAT, F2.(m+1)qua Element of HFuncs
NAT, p, i, ff2] by A22;
Q[m,F1.m qua Element of HFuncs NAT, F1.(m+1)qua Element of HFuncs
NAT,p,i,f2] by A18;
hence p[m+1] by A24;
end;
A25: p[0] by A16,A17,A20,A21;
for m being Nat holds p[m] from NAT_1:sch 2(A25,A23);
hence thesis by A15,A19;
end;
end;
theorem Th48:
for i being Nat
for p, q being FinSequence of NAT st q in dom primrec(e1,e2,i,p)
ex k being Element of NAT st q = p+*(i,k)
proof let i be Nat;
set f1 = e1, f2 = e2;
let p, q being FinSequence of NAT such that
A1: q in dom primrec(f1,f2,i,p);
consider F being sequence of HFuncs NAT such that
A2: primrec(f1,f2,i,p) = F.(p/.i) and
A3: i in dom p & Del(p,i) in dom f1 implies F.0 = p+*(i,0) .--> (f1.Del(
p,i)) and
A4: not i in dom p or not Del(p,i) in dom f1 implies F.0 = {} and
A5: for m being Nat holds Q[m, F.m qua Element of HFuncs NAT,
F.(m+1)qua Element of HFuncs NAT, p, i, f2] by Def10;
defpred p[Nat] means q in dom (F.$1) implies ex k being Element
of NAT st q = p+*(i,k);
A6: for m be Nat st p[m] holds p[m+1]
proof
let m be Nat such that
A7: p[m] and
A8: q in dom (F.(m+1));
per cases;
suppose
i in dom p & p+*(i,m) in dom (F.m) & (p+*(i,m))^<*(F.m).(p+*(i,
m))*> in dom f2;
then F.(m+1) = (F.m)+*(p+*(i,m+1).--> f2.((p+*(i,m))^<*(F.m).(p+*(i,m))
*>)) by A5;
then
dom (F.(m+1)) = dom (F.m) \/ dom (p+*(i,m+1).--> f2.((p+*(i,m))^<*(
F.m).(p+*(i,m))*>)) by FUNCT_4:def 1;
then
A9: dom (F.(m+1)) = dom (F.m) \/ {p+*(i,m+1)};
thus ex k being Element of NAT st q = p+*(i,k)
proof
per cases by A8,A9,XBOOLE_0:def 3;
suppose
q in dom (F.m);
hence thesis by A7;
end;
suppose
q in {p+*(i,m+1)};
then q = p+*(i,m+1) by TARSKI:def 1;
hence thesis;
end;
end;
end;
suppose
not i in dom p or not p+*(i,m) in dom (F.m) or not (p+*(i,m))^
<*(F.m).(p+*(i,m))*> in dom f2;
hence thesis by A5,A7,A8;
end;
end;
A10: p[0]
proof
assume
A11: q in dom (F.0);
per cases;
suppose
i in dom p & Del(p,i) in dom f1;
then dom (F.0) = {p+*(i,0)} by A3;
then p+*(i,0) = q by A11,TARSKI:def 1;
hence thesis;
end;
suppose
not i in dom p or not Del(p,i) in dom f1;
hence thesis by A4,A11;
end;
end;
for n being Nat holds p[n] from NAT_1:sch 2(A10,A6);
hence thesis by A1,A2;
end;
theorem Th49:
for i being Nat
for p being FinSequence of NAT st not i in dom p
holds primrec(e1,e2,i,p) = {}
proof let i be Nat;
set f1 = e1, f2 = e2;
let p be FinSequence of NAT;
consider F being sequence of HFuncs NAT such that
A1: primrec(f1,f2,i,p) = F.(p/.i) and
i in dom p & Del(p,i) in dom f1 implies F.0 = p+*(i,0) .--> (f1.Del(p,i)
) and
A2: not i in dom p or not Del(p,i) in dom f1 implies F.0 = {} and
A3: for m being Nat holds Q[m, F.m qua Element of HFuncs NAT,
F.(m+1)qua Element of HFuncs NAT, p, i, f2] by Def10;
defpred p[Nat] means F.$1 = {};
assume
A4: not i in dom p;
then
A5: for m be Nat st p[m] holds p[m+1] by A3;
A6: p[0] by A4,A2;
for m being Nat holds p[m] from NAT_1:sch 2(A6, A5);
hence thesis by A1;
end;
theorem Th50:
for i being Nat
for p, q being FinSequence of NAT holds
primrec(e1,e2,i,p) tolerates primrec(e1,e2,i,q)
proof let i be Nat;
set f1 = e1, f2 = e2;
let p1,p2 be FinSequence of NAT;
per cases;
suppose
not i in dom p1 or not i in dom p2;
then primrec(f1,f2,i, p1) = {} or primrec(f1,f2,i, p2) = {} by Th49;
hence thesis;
end;
suppose
A1: i in dom p1 & i in dom p2;
reconsider m = p1/.i, n = p2/.i as Element of NAT;
consider F2 being sequence of HFuncs NAT such that
A2: primrec(f1,f2,i,p2) = F2.(p2/.i) and
A3: i in dom p2 & Del(p2,i) in dom f1 implies F2.0 = p2+*(i,0) .--> (
f1.Del(p2,i)) and
A4: not i in dom p2 or not Del(p2,i) in dom f1 implies F2.0 = {} and
A5: for m being Nat holds Q[m, F2.m qua Element of HFuncs
NAT, F2.(m+1)qua Element of HFuncs NAT, p2, i, f2] by Def10;
consider F1 being sequence of HFuncs NAT such that
A6: primrec(f1,f2,i,p1) = F1.(p1/.i) and
A7: i in dom p1 & Del(p1,i) in dom f1 implies F1.0 = p1+*(i,0) .--> (
f1.Del(p1,i)) and
A8: not i in dom p1 or not Del(p1,i) in dom f1 implies F1.0 = {} and
A9: for m being Nat holds Q[m, F1.m qua Element of HFuncs
NAT, F1.(m+1)qua Element of HFuncs NAT, p1, i, f2] by Def10;
defpred p[Nat] means for x being set st x in dom (F1.$1) ex n
being Element of NAT st x = p1+*(i,n) & n <= $1;
A10: now
let m be Nat such that
A11: p[m];
thus p[m+1]
proof
set p1c = (p1+*(i,m))^<*(F1.m).(p1+*(i,m))*>;
let x be set such that
A12: x in dom (F1.(m+1));
A13: m <= m+1 by NAT_1:11;
per cases;
suppose
i in dom p1 & p1+*(i,m) in dom (F1.m) & p1c in dom f2;
then F1.(m+1) = (F1.m)+*(p1+*(i,m+1).--> f2.(p1c)) by A9;
then dom (F1.(m+1)) = dom (F1.m) \/ dom (p1+*(i,m+1).--> f2.(p1c))
by FUNCT_4:def 1
.= dom (F1.m) \/ {p1+*(i,m+1)};
then
A14: x in dom (F1.m) or x in {p1+*(i,m+1)} by A12,XBOOLE_0:def 3;
thus ex n being Element of NAT st x = p1+*(i,n) & n <= m+1
proof
per cases by A14,TARSKI:def 1;
suppose
x in dom (F1.m);
then ex n being Element of NAT st x = p1+*(i,n) & n <= m by A11;
hence thesis by A13,XXREAL_0:2;
end;
suppose
x = p1+*(i,m+1);
hence thesis;
end;
end;
end;
suppose
not i in dom p1 or not p1+*(i,m) in dom (F1.m) or not p1c in dom f2;
then F1.(m+1) = F1.m by A9;
then ex n being Element of NAT st x = p1+*(i,n) & n <= m by A11,A12;
hence thesis by A13,XXREAL_0:2;
end;
end;
end;
A15: now
defpred r[Nat] means F1.$1 = F2.$1;
assume
A16: p1+*(i,0) = p2+*(i,0);
A17: r[0]
proof
per cases;
suppose
i in dom p1 & Del(p1,i) in dom f1;
hence thesis by A1,A7,A3,A16,Th4;
end;
suppose
not i in dom p1 or not Del(p1, i) in dom f1;
hence thesis by A1,A8,A4,A16,Th4;
end;
end;
A18: now
let m be Nat such that
A19: r[m];
A20: Q[m, F1.m qua Element of HFuncs NAT, F1.(m+1)qua Element of
HFuncs NAT, p1, i, f2] by A9;
A21: Q[m, F2.m qua Element of HFuncs NAT, F2.(m+1)qua Element of
HFuncs NAT, p2, i, f2] by A5;
p1+*(i,m) = p2+*(i,m) by A16,Th2;
hence r[m+1] by A1,A19,A20,A21,Th2;
end;
thus for m being Nat holds r[m] from NAT_1:sch 2(A17, A18);
end;
A22: p[0]
proof
let x be set such that
A23: x in dom (F1.0);
dom (F1.0) = {p1+*(i,0)} by A7,A8,A23;
then x = p1+*(i,0) by A23,TARSKI:def 1;
hence thesis;
end;
A24: for m being Nat holds p[m] from NAT_1:sch 2(A22, A10);
A25: for m, n being Nat holds F1.m c= F1.(m+n)
proof
let m be Nat;
defpred r[Nat] means F1.m c= F1.(m+$1);
A26: now
let n be Nat such that
A27: r[n];
set k = m+n;
F1.k qua set c= F1.(k+1) qua set
proof
set p1c = (p1+*(i,k))^<*(F1.k).(p1+*(i,k))*>;
let x be object such that
A28: x in F1.k;
per cases;
suppose
A29: i in dom p1 & p1+*(i,k) in dom (F1.k) & p1c in dom f2;
A30: dom (F1.k) misses dom (p1+*(i,k+1).--> f2.(p1c))
proof
assume not thesis;
then consider x being object such that
A31: x in dom (F1.k) /\ dom({p1+*(i,k+1)}--> f2.(p1c)) by XBOOLE_0:4;
x in dom (F1.k) by A31,XBOOLE_0:def 4;
then consider n1 being Element of NAT such that
A32: x = p1+*(i,n1) and
A33: n1 <= k by A24;
A34: k+1 = (p1+*(i,k+1)).i by A1,FUNCT_7:31;
A35: x = p1+*(i,k+1) by A31,TARSKI:def 1;
n1 = (p1+*(i,n1)).i by A1,FUNCT_7:31;
hence contradiction by A35,A32,A33,A34,NAT_1:13;
end;
F1.(k+1) = (F1.k)+*(p1+*(i,k+1).--> f2.(p1c)) by A9,A29;
then F1.k c= F1.(k+1) by A30,FUNCT_4:32;
hence thesis by A28;
end;
suppose
not i in dom p1 or not p1+*(i,k) in dom (F1.k) or not p1c
in dom f2;
hence thesis by A9,A28;
end;
end;
hence r[n+1] by A27,XBOOLE_1:1;
end;
A36: r[0];
thus for n being Nat holds r[n] from NAT_1:sch 2(A36, A26);
end;
defpred p[Nat] means for x being set st x in dom (F2.$1) ex n
being Element of NAT st x = p2+*(i,n) & n <= $1;
A37: now
let m be Nat such that
A38: p[m];
thus p[m+1]
proof
set p2c = (p2+*(i,m))^<*(F2.m).(p2+*(i,m))*>;
let x be set such that
A39: x in dom (F2.(m+1));
A40: m <= m+1 by NAT_1:11;
per cases;
suppose
i in dom p2 & p2+*(i,m) in dom (F2.m) & p2c in dom f2;
then F2.(m+1) = (F2.m)+*(p2+*(i,m+1).--> f2.(p2c)) by A5;
then dom (F2.(m+1)) = dom (F2.m) \/ dom (p2+*(i,m+1).--> f2.(p2c))
by FUNCT_4:def 1
.= dom (F2.m) \/ {p2+*(i,m+1)};
then
A41: x in dom (F2.m) or x in {p2+*(i,m+1)} by A39,XBOOLE_0:def 3;
thus ex n being Element of NAT st x = p2+*(i,n) & n <= m+1
proof
per cases by A41,TARSKI:def 1;
suppose
x in dom (F2.m);
then ex n being Element of NAT st x = p2+*(i,n) & n <= m by A38;
hence thesis by A40,XXREAL_0:2;
end;
suppose
x = p2+*(i,m+1);
hence thesis;
end;
end;
end;
suppose
not i in dom p2 or not p2+*(i,m) in dom (F2.m) or not p2c in dom f2;
then F2.(m+1) = F2.m by A5;
then ex n being Element of NAT st x = p2+*(i,n) & n <= m by A38,A39;
hence thesis by A40,XXREAL_0:2;
end;
end;
end;
A42: p[0]
proof
let x be set such that
A43: x in dom (F2.0);
dom (F2.0) = {p2+*(i,0)} by A3,A4,A43;
then x = p2+*(i,0) by A43,TARSKI:def 1;
hence thesis;
end;
A44: for m being Nat holds p[m] from NAT_1:sch 2(A42, A37);
A45: for m, n being Nat holds F2.m c= F2.(m+n)
proof
let m be Nat;
defpred r[Nat] means F2.m c= F2.(m+$1);
A46: now
let n be Nat such that
A47: r[n];
set k = m+n;
F2.k c= F2.(k+1)
proof
set p2c = (p2+*(i,k))^<*(F2.k).(p2+*(i,k))*>;
let x be object such that
A48: x in F2.k;
per cases;
suppose
A49: i in dom p2 & p2+*(i,k) in dom (F2.k) & p2c in dom f2;
A50: dom (F2.k) misses dom (p2+*(i,k+1).--> f2.(p2c))
proof
assume not thesis;
then consider x being object such that
A51: x in dom (F2.k) /\ dom({p2+*(i,k+1)}--> f2.(p2c)) by XBOOLE_0:4;
x in dom (F2.k) by A51,XBOOLE_0:def 4;
then consider n2 being Element of NAT such that
A52: x = p2+*(i,n2) and
A53: n2 <= k by A44;
A54: k+1 = (p2+*(i,k+1)).i by A1,FUNCT_7:31;
A55: x = p2+*(i,k+1) by A51,TARSKI:def 1;
n2 = (p2+*(i,n2)).i by A1,FUNCT_7:31;
hence contradiction by A55,A52,A53,A54,NAT_1:13;
end;
F2.(k+1) = (F2.k)+*(p2+*(i,k+1).--> f2.(p2c)) by A5,A49;
then F2.k c= F2.(k+1) by A50,FUNCT_4:32;
hence thesis by A48;
end;
suppose
not i in dom p2 or not p2+*(i,k) in dom (F2.k) or not
p2c in dom f2;
hence thesis by A5,A48;
end;
end;
hence r[n+1] by A47,XBOOLE_1:1;
end;
A56: r[0];
thus for n being Nat holds r[n] from NAT_1:sch 2(A56, A46);
end;
reconsider F1m = F1.m, F1n = F1.n, F2m = F2.m, F2n = F2.n as Element of
HFuncs NAT;
A57: now
assume
A58: p1+*(i,0) <> p2+*(i,0);
let m be Element of NAT;
assume dom (F1.m) /\ dom (F2.m) <> {};
then consider x being object such that
A59: x in dom(F1.m) /\ dom(F2.m) by XBOOLE_0:def 1;
x in dom(F2.m) by A59,XBOOLE_0:def 4;
then
A60: ex n2 being Element of NAT st x = p2+*(i,n2) & n2 <= m by A44;
x in dom(F1.m) by A59,XBOOLE_0:def 4;
then ex n1 being Element of NAT st x = p1+*(i,n1) & n1 <= m by A24;
hence contradiction by A58,A60,Th2;
end;
thus thesis
proof
per cases;
suppose
m <= n;
then consider k being Nat such that
A61: n = m+k by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
A62: n = m+k by A61;
thus primrec(f1,f2,i,p1) tolerates primrec(f1,f2,i,p2)
proof
per cases by A15,A57;
suppose
F1n = F2n;
hence thesis by A6,A2,A25,A62,PARTFUN1:58;
end;
suppose
dom (F1n) /\ dom (F2n) = {};
then dom (F1n) misses dom (F2n) by XBOOLE_0:def 7;
then F1n tolerates F2n by PARTFUN1:56;
hence thesis by A6,A2,A25,A62,PARTFUN1:58;
end;
end;
end;
suppose
m >= n;
then consider k being Nat such that
A63: m = n+k by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
A64: m = n+k by A63;
thus primrec(f1,f2,i,p1) tolerates primrec(f1,f2,i,p2)
proof
per cases by A15,A57;
suppose
F1m = F2m;
hence thesis by A6,A2,A45,A64,PARTFUN1:58;
end;
suppose
dom (F1m) /\ dom (F2m) = {};
then dom (F1m) misses dom (F2m) by XBOOLE_0:def 7;
then F1m tolerates F2m by PARTFUN1:56;
hence thesis by A6,A2,A45,A64,PARTFUN1:58;
end;
end;
end;
end;
end;
end;
theorem Th51:
for i being Nat
for p being FinSequence of NAT holds
dom primrec(e1,e2,i,p) c= (1+arity e1)-tuples_on NAT
proof let i be Nat;
set f1 = e1, f2 = e2;
let p be FinSequence of NAT;
per cases;
suppose
A1: i in dom p;
consider F being sequence of HFuncs NAT such that
A2: primrec(f1,f2,i,p) = F.(p/.i) and
A3: i in dom p & Del(p,i) in dom f1 implies F.0 = p+*(i,0) .--> (f1.
Del(p,i)) and
A4: not i in dom p or not Del(p,i) in dom f1 implies F.0 = {} and
A5: for m being Nat holds Q[m, F.m qua Element of HFuncs
NAT, F.(m+1)qua Element of HFuncs NAT, p, i, f2] by Def10;
defpred p[Nat] means dom (F.$1) c= (1+arity f1)-tuples_on NAT;
A6: now
let m be Nat such that
A7: p[m];
set pc = (p+*(i,m))^<*(F.m).(p+*(i,m))*>;
per cases;
suppose
A8: p+*(i,m) in dom (F.m) & pc in dom f2;
dom (p+*(i,m)) = dom p by FUNCT_7:30
.= dom (p+*(i,m+1)) by FUNCT_7:30;
then
A9: len (p+*(i,m)) = len (p+*(i,m+1)) by FINSEQ_3:29;
len (p+*(i,m)) = 1+arity f1 by A7,A8,CARD_1:def 7;
then p+*(i,m+1)is Element of (1+arity f1)-tuples_on NAT by A9,
FINSEQ_2:92;
then
A10: {p+*(i,m+1)} c= (1+arity f1)-tuples_on NAT by ZFMISC_1:31;
F.(m+1) = (F.m)+*(p+*(i,m+1).--> f2.(pc)) by A1,A5,A8;
then dom (F.(m+1)) = dom (F.m) \/ dom (p+*(i,m+1).--> f2.(pc)) by
FUNCT_4:def 1;
then dom (F.(m+1)) = dom (F.m) \/ {p+*(i,m+1)};
hence p[m+1] by A7,A10,XBOOLE_1:8;
end;
suppose
not p+*(i,m) in dom (F.m) or not pc in dom f2;
hence p[m+1] by A5,A7;
end;
end;
A11: p[0]
proof
per cases;
suppose
A12: Del(p,i) in dom f1;
dom f1 c= (arity f1)-tuples_on NAT by Th20;
then
A13: len Del(p,i) = arity f1 by A12,CARD_1:def 7;
A14: dom p = dom (p+*(i,0)) by FUNCT_7:30;
p <> <*>NAT by A1;
then consider n being Nat such that
A15: len p = n+1 by NAT_1:6;
len Del(p,i) = n by A1,A15,FINSEQ_3:109;
then len (p+*(i,0)) = 1+arity f1 by A13,A15,A14,FINSEQ_3:29;
then
A16: (p+*(i,0)) is Element of (1+arity f1)-tuples_on NAT by FINSEQ_2:92;
dom (F.0) = {p+*(i,0)} by A1,A3,A12;
hence thesis by A16,ZFMISC_1:31;
end;
suppose
not Del(p,i) in dom f1;
hence thesis by A4,XBOOLE_1:2;
end;
end;
for m being Nat holds p[m] from NAT_1:sch 2(A11,A6);
hence thesis by A2;
end;
suppose
not i in dom p;
then primrec(f1,f2,i,p) = {} by Th49;
hence thesis;
end;
end;
theorem Th52:
for p being FinSequence of NAT st e1 is empty
holds primrec(e1,e2,i,p) is empty
proof
set f1 = e1, f2 = e2;
let p be FinSequence of NAT;
consider F be sequence of HFuncs NAT such that
A1: primrec(f1,f2,i,p) = F.(p/.i) and
i in dom p & Del(p,i) in dom f1 implies F.0 = p+*(i,0) .--> (f1.Del(p,i
)) and
A2: not i in dom p or not Del(p,i) in dom f1 implies F.0 = {} and
A3: for m 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) by Def10;
defpred p[Nat] means F.$1 = {};
A4: for k be Nat st p[k] holds p[k+1] by A3,RELAT_1:38;
assume f1 is empty;
then
A5: p[0] by A2;
for k being Nat holds p[k] from NAT_1:sch 2(A5,A4);
hence thesis by A1;
end;
theorem Th53:
f1 is len-total & f2 is len-total & arity f1 +2 = arity f2 &
1 <= i & i <= 1+arity f1 implies p in dom primrec(f1,f2,i,p)
proof
assume that
A1: f1 is len-total and
A2: f2 is len-total and
A3: arity f1 +2 = arity f2 and
A4: 1 <= i and
A5: i <= 1+arity f1;
A6: len p = 1+arity f1 by CARD_1:def 7;
then
A7: i in dom p by A4,A5,FINSEQ_3:25;
then
A8: p/.i = p.i by PARTFUN1:def 6;
consider F being sequence of HFuncs NAT such that
A9: primrec(f1,f2,i,p) = F.(p/.i) and
A10: i in dom p & Del(p,i) in dom f1 implies F.0 = p+*(i,0) .--> (f1.Del
(p,i)) and
not i in dom p or not Del(p,i) in dom f1 implies F.0 = {} and
A11: for m 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) by Def10;
defpred p[Nat] means (p+*(i,$1)) in dom (F.$1);
A12: (p+*(i,p.i)) = p by FUNCT_7:35;
A13: now
let m be Nat such that
A14: p[m];
reconsider aa = (F.m).(p+*(i,m)) as Element of NAT;
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
set pc = (p+*(i,m))^<*(F.m).(p+*(i,m))*>;
reconsider p2 = <*aa*> as FinSequence of NAT;
reconsider p1 = (p+*(i,mm))^p2 as FinSequence of NAT;
A15: len p2 = 1 by CARD_1:def 7;
len (p+*(i,mm))=1+arity f1 by CARD_1:def 7;
then len p1 = arity f1+1+1 by A15,FINSEQ_1:22
.= arity f2 by A3;
then
A16: p1 is Element of (arity f2)-tuples_on NAT by FINSEQ_2:92;
p+*(i,m+1) in {p+*(i,m+1)} by TARSKI:def 1;
then
A17: p+*(i,m+1) in dom ({p+*(i,m+1)}--> f2.(pc));
dom f2 = (arity f2)-tuples_on NAT by A2,Th22;
then F.(m+1) = (F.m)+*(p+*(i,m+1).--> f2.(pc)) by A7,A11,A14,A16;
then dom(F.(m+1))=dom (F.m) \/ dom ({p+*(i,m+1)}--> f2.(pc))
by FUNCT_4:def 1;
hence p[m+1] by A17,XBOOLE_0:def 3;
end;
A18: now
reconsider Dpi = Del(p,i) as FinSequence of NAT by FINSEQ_3:105;
reconsider Dpi9 = Dpi as Element of (len Dpi)-tuples_on NAT by FINSEQ_2:92;
A19: dom f1 = (arity f1)-tuples_on NAT by A1,Th22;
len Del(p,i) = arity f1 by A6,A7,FINSEQ_3:109;
then Dpi9 in dom f1 by A19;
then dom (F.0) = {p+*(i,0)} by A4,A5,A6,A10,FINSEQ_3:25;
hence p[0] by TARSKI:def 1;
end;
for m being Nat holds p[m] from NAT_1:sch 2(A18, A13);
hence thesis by A8,A9,A12;
end;
definition
let f1,f2 be homogeneous to-naturals NAT*-defined Function;
let i be Nat;
func primrec(f1,f2,i) -> Element of HFuncs NAT means
:Def11:
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
proof
deffunc f(FinSequence of NAT) = primrec(f1,f2,i,$1);
reconsider ff1 = f1, ff2 = f2 as Element of HFuncs NAT by Th27;
set n = arity f1+1;
consider G being Function of n-tuples_on NAT, HFuncs NAT such that
A1: for p being Element of n-tuples_on NAT holds G.p = f(p) from
FUNCT_2:sch 4;
reconsider Y = rng G as non empty Subset of HFuncs NAT by RELAT_1:def 19;
Y is PartFunc-set of NAT*, NAT
proof
let f be Element of Y;
thus thesis;
end;
then reconsider Y as PFUNC_DOMAIN of NAT*, NAT;
A2: Y is compatible
proof
let f,g be Function;
assume f in Y;
then consider x being object such that
A3: x in dom G and
A4: f = G.x by FUNCT_1:def 3;
assume g in Y;
then consider y being object such that
A5: y in dom G and
A6: g = G.y by FUNCT_1:def 3;
reconsider x,y as Element of n-tuples_on NAT by A3,A5;
A7: g = primrec(ff1,ff2,i,y) by A1,A6;
f = primrec(ff1,ff2,i,x) by A1,A4;
hence thesis by A7,Th50;
end;
now
let x be Element of n-tuples_on NAT;
G.x = primrec(ff1,ff2,i,x) by A1;
hence dom (G.x) c= n-tuples_on NAT by Th51;
end;
then consider g being Element of HFuncs NAT such that
A8: g = Union G and
dom g c= n-tuples_on NAT by A2,Th38;
take g, G;
thus thesis by A1,A8;
end;
uniqueness
proof
let g1,g2 be Element of HFuncs NAT;
given G1 being Function of (arity f1+1)-tuples_on NAT, HFuncs NAT such
that
A9: g1 = Union G1 and
A10: for p being Element of (arity f1+1)-tuples_on NAT holds G1.p =
primrec(f1,f2,i,p);
given G2 being Function of (arity f1+1)-tuples_on NAT, HFuncs NAT such
that
A11: g2 = Union G2 and
A12: for p being Element of (arity f1+1)-tuples_on NAT holds G2.p =
primrec(f1,f2,i,p);
now
let p be Element of (arity f1+1)-tuples_on NAT;
thus G1.p = primrec(f1,f2,i,p) by A10
.= G2.p by A12;
end;
hence thesis by A9,A11,FUNCT_2:63;
end;
end;
theorem Th54:
e1 is empty implies primrec(e1,e2,i) is empty
proof
set f1 = e1, f2 = e2;
assume
A1: f1 is empty;
consider G being Function of (arity f1+1)-tuples_on NAT, HFuncs NAT such
that
A2: primrec(f1,f2,i) = Union G and
A3: for p being Element of (arity f1+1)-tuples_on NAT holds G.p =
primrec(f1,f2,i,p) by Def11;
A4: dom G = (arity f1+1)-tuples_on NAT by FUNCT_2:def 1;
now
set p = the Element of (arity f1+1)-tuples_on NAT;
let y be object;
hereby
assume y in rng G;
then consider x being object such that
A5: x in dom G and
A6: G.x = y by FUNCT_1:def 3;
reconsider p = x as Element of (arity f1+1)-tuples_on NAT by A5;
G.p = primrec(f1,f2,i,p) by A3
.= {} by A1,Th52;
hence y in {{}} by A6,TARSKI:def 1;
end;
assume y in {{}};
then
A7: y = {} by TARSKI:def 1;
G.p = primrec ( f1,f2,i,p) by A3
.= {} by A1,Th52;
hence y in rng G by A4,A7,FUNCT_1:3;
end;
then
A8: rng G = {{}} by TARSKI:2;
Union G = {} by A8,ZFMISC_1:25;
hence thesis by A2;
end;
theorem Th55:
dom primrec(f1,f2,i) c= (arity f1+1)-tuples_on NAT
proof
let x be object such that
A1: x in dom primrec(f1,f2,i);
consider G being Function of (arity f1+1)-tuples_on NAT, HFuncs NAT such
that
A2: primrec(f1,f2,i) = Union G and
A3: for p being Element of (arity f1+1)-tuples_on NAT holds G.p =
primrec(f1,f2,i,p) by Def11;
A4: rng G is compatible
proof
let f,g being Function such that
A5: f in rng G and
A6: g in rng G;
consider fx being object such that
A7: fx in dom G and
A8: f = G.fx by A5,FUNCT_1:def 3;
reconsider fx as Element of (arity f1+1)-tuples_on NAT by A7;
consider gx being object such that
A9: gx in dom G and
A10: g = G.gx by A6,FUNCT_1:def 3;
reconsider gx as Element of (arity f1+1)-tuples_on NAT by A9;
A11: G.gx = primrec(f1,f2,i,gx) by A3;
G.fx = primrec(f1,f2,i,fx) by A3;
hence thesis by A8,A10,A11,Th50;
end;
now
let x be Element of (arity f1+1)-tuples_on NAT;
G.x = primrec(f1,f2,i,x) by A3;
hence dom (G.x) c= (arity f1+1)-tuples_on NAT by Th51;
end;
then
ex F being Element of HFuncs NAT st F = Union G & dom F c= (arity f1+
1)-tuples_on NAT by A4,Th38;
hence thesis by A1,A2;
end;
theorem Th56:
f1 is len-total & f2 is len-total & arity f1 +2 = arity f2 &
1 <= i & i <= 1+arity f1 implies
dom primrec(f1,f2,i) = (arity f1+1)-tuples_on NAT &
arity primrec(f1,f2,i) = arity f1+1
proof
assume that
A1: f1 is len-total and
A2: f2 is len-total and
A3: arity f1 +2 = arity f2 and
A4: 1 <= i and
A5: i <= 1+arity f1;
set n = arity f1+1;
A6: n-tuples_on NAT c= dom primrec(f1,f2,i)
proof
let x be object;
assume x in n-tuples_on NAT;
then reconsider x9 = x as Element of n-tuples_on NAT;
consider G being Function of n-tuples_on NAT, HFuncs NAT such that
A7: primrec(f1,f2,i) = Union G and
A8: for p being Element of n-tuples_on NAT holds G.p = primrec(f1,f2,
i,p) by Def11;
reconsider rngG = rng G as non empty functional compatible set by A7,Th10;
A9: dom union rngG = union the set of all dom f where f is Element of rngG
by Th11;
dom G = n-tuples_on NAT by FUNCT_2:def 1;
then G.x9 in rng G by FUNCT_1:3;
then
A10: dom (G.x9) in the set of all dom f where f is Element of rngG;
A11: x9 in dom primrec(f1,f2,i,x9) by A1,A2,A3,A4,A5,Th53;
G.x9 = primrec(f1,f2,i,x9) by A8;
hence thesis by A7,A11,A9,A10,TARSKI:def 4;
end;
dom primrec(f1,f2,i) c= (arity f1+1)-tuples_on NAT by Th55;
hence dom primrec(f1,f2,i) = (arity f1+1)-tuples_on NAT by A6;
hence thesis by Th24;
end;
Lm2: now
let f1,f2 be non empty homogeneous to-naturals NAT*-defined Function;
let p be Element of (arity f1+1)-tuples_on NAT;
let i be Nat, m be Element of NAT;
set pm1 = p+*(i,m+1), pm = p+*(i,m);
let F1, F be sequence of HFuncs NAT such that
A1: i in dom pm1 & Del(pm1,i) in dom f1 implies F1.0 = {pm1+*(i,0)} -->
(f1 .Del(pm1,i)) and
A2: not i in dom pm1 or not Del(pm1,i) in dom f1 implies F1.0 = {} and
A3: for M being Nat holds Q[M, F1.M qua Element of HFuncs NAT
, F1.(M+1)qua Element of HFuncs NAT, pm1, i, f2] and
A4: i in dom pm & Del(pm,i) in dom f1 implies F.0 = {pm+*(i,0)} --> (f1
.Del(pm,i)) and
A5: not i in dom pm or not Del(pm,i) in dom f1 implies F.0 = {} and
A6: for M being Nat holds Q[M, F.M qua Element of HFuncs NAT,
F.(M+1) qua Element of HFuncs NAT, pm, i, f2];
A7: dom p = dom pm by FUNCT_7:30;
A8: pm+*(i,0) = p+*(i,0) by FUNCT_7:34
.= pm1+*(i,0) by FUNCT_7:34;
A9: dom p = dom pm1 by FUNCT_7:30;
A10: Del(pm,i) = Del(p,i) by Th3
.= Del(pm1,i) by Th3;
for x being object st x in NAT holds F.x = F1.x
proof
let x be object;
defpred p[Nat] means F.$1 = F1.$1;
A11: for k be Nat st p[k] holds p[k+1]
proof
let k be Nat such that
A12: p[k];
A13: pm+*(i,(k+1))=p+*(i,(k+1)) by FUNCT_7:34
.=pm1+*(i,(k+1)) by FUNCT_7:34;
A14: pm+*(i,k) = p+*(i,k) by FUNCT_7:34
.= pm1+*(i,k) by FUNCT_7:34;
per cases;
suppose
A15: i in dom pm & pm+*(i,k) in dom (F.k) & (pm+*(i,k))^<*(F.k).(
pm+*(i,k))*> in dom f2;
hence
F.(k+1) = (F.k)+*(pm+*(i,k+1).--> f2.((pm+*(i,k))^<*(F.k).(pm+*(i
,k))*>)) by A6
.= F1.(k+1) by A3,A7,A9,A12,A14,A13,A15;
end;
suppose
A16: not i in dom pm or not pm+*(i,k) in dom (F.k) or not (pm+*(i,
k))^<*(F.k).(pm+*(i,k))*> in dom f2;
hence F.(k+1) = F.k by A6
.= F1.(k+1) by A3,A7,A9,A12,A14,A16;
end;
end;
A17: p[0] by A1,A2,A4,A5,A7,A8,A10,FUNCT_7:30;
A18: for k being Nat holds p[k] from NAT_1:sch 2(A17, A11);
assume x in NAT;
hence thesis by A18;
end;
hence F1 = F by FUNCT_2:12;
end;
Lm3: now
let f1,f2 be non empty homogeneous to-naturals NAT*-defined Function;
let p be Element of (arity f1+1)-tuples_on NAT;
let i, m be Element of NAT such that
A1: i in dom p;
set pm = p+*(i,m), pm1 = p+*(i,(m+1));
let F be sequence of HFuncs NAT such that
A2: i in dom pm1 & Del(pm1,i) in dom f1 implies F.0 = {pm1+*(i,0)} --> (
f1. Del(pm1,i)) and
A3: not i in dom pm1 or not Del(pm1,i) in dom f1 implies F.0 = {} and
A4: for M being Nat holds Q[M, F.M qua Element of HFuncs NAT,
F.(M+1)qua Element of HFuncs NAT, pm1, i, f2];
thus F.(m+1).pm = F.m.pm
proof
per cases;
suppose
A5: i in dom pm1 & pm1+*(i,m) in dom (F.m) & (pm1+*(i,m))^<*(F.m).(
pm1+*(i,m))*> in dom f2;
A6: pm1 = pm1+*(i,m+1) by FUNCT_7:34;
A7: pm1.i = m+1 by A1,FUNCT_7:31;
pm.i = m by A1,FUNCT_7:31;
then pm <> pm1 by A7;
then
A8: not pm in dom ({pm1+*(i,m+1)}--> f2.((pm1+*(i,m))^<*(F.m).(pm1+*(i,
m))*>)) by A6,TARSKI:def 1;
F.(m+1) = (F.m)+*(pm1+*(i,m+1).--> f2.((pm1+*(i,m))^<*(F.m).(pm1+*(i
,m))*>)) by A4,A5;
hence thesis by A8,FUNCT_4:11;
end;
suppose
not i in dom pm1 or not pm1+*(i,m) in dom (F.m) or not (pm1+*(i
,m))^<*(F.m).(pm1+*(i,m))*> in dom f2;
hence thesis by A4;
end;
end;
A9: for m, k being Nat st p+*(i,k) in dom (F.m) holds k <= m
proof
defpred p[Nat] means for k being Nat st p+*(i,k) in
dom (F.$1) holds k <= $1;
A10: for m be Nat st p[m] holds p[m+1]
proof
let m be Nat such that
A11: p[m];
let k be Nat such that
A12: p+*(i,k) in dom (F.(m+1));
per cases;
suppose
i in dom pm1 & pm1+*(i,m) in dom (F.m) & (pm1+*(i,m))^<*(F.m)
.(pm1+*(i,m))*> in dom f2;
then F.(m+1) = (F.m)+*(pm1+*(i,m+1).--> f2.((pm1+*(i,m))^<*(F.m).(pm1
+*(i,m))*>))by A4;
then
dom (F.(m+1)) = dom (F.m) \/ dom ({pm1+*(i,m+1)}--> f2.((pm1+*(i,
m))^<*(F.m).(pm1+*(i,m))*>)) by FUNCT_4:def 1;
then
A13: dom (F.(m+1)) = dom (F.m) \/ {pm1+*(i,m+1)};
thus k <= (m+1)
proof
per cases by A12,A13,XBOOLE_0:def 3;
suppose
A14: p+*(i,k) in dom (F.m);
A15: m <= m+1 by NAT_1:11;
k <= m by A11,A14;
hence thesis by A15,XXREAL_0:2;
end;
suppose
p+*(i,k) in {pm1+*(i,m+1)};
then
A16: p+*(i,k)= pm1+*(i,m+1) by TARSKI:def 1
.=p+*(i,m+1) by FUNCT_7:34;
k = (p+*(i,k)).i by A1,FUNCT_7:31
.= m+1 by A1,A16,FUNCT_7:31;
hence thesis;
end;
end;
end;
suppose
not i in dom pm1 or not pm1+*(i,m) in dom (F.m) or not (pm1+*
(i,m))^<*(F.m).(pm1+*(i,m))*> in dom f2;
then F.(m+1) = F.m by A4;
then
A17: k <= m by A11,A12;
m <= m+1 by NAT_1:11;
hence thesis by A17,XXREAL_0:2;
end;
end;
A18: p[0]
proof
let k be Nat such that
A19: p+*(i,k) in dom (F.0);
per cases;
suppose
i in dom pm1 & Del(pm1,i) in dom f1;
then dom (F.0) = {pm1+*(i,0)} by A2;
then
A20: (p+*(i,k)) = (pm1+*(i,0)) by A19,TARSKI:def 1
.= p+*(i,0) by FUNCT_7:34;
k = (p+*(i,k)).i by A1,FUNCT_7:31
.= 0 by A1,A20,FUNCT_7:31;
hence thesis;
end;
suppose
not i in dom pm1 or not Del(pm1,i) in dom f1;
hence thesis by A3,A19;
end;
end;
thus for n be Nat holds p[n] from NAT_1:sch 2(A18, A10);
end;
thus not pm1 in dom (F.m)
proof
assume not thesis;
then m+1 <= m by A9;
hence contradiction by NAT_1:13;
end;
end;
definition let n be Nat, p be Element of n-tuples_on NAT;
let i,k be Nat;
redefine func p+*(i,k) -> Element of n-tuples_on NAT; :: redefines +* (FUNCT_7, definition)
coherence
proof
reconsider i,k as Element of NAT by ORDINAL1:def 12;
p+*(i,k) is Element of n-tuples_on NAT;
hence thesis;
end;
end;
Lm4: now
let f1,f2 be non empty homogeneous to-naturals NAT*-defined Function;
let p be Element of (arity f1+1)-tuples_on NAT;
let i, m be Element of NAT such that
A1: i in dom p;
let G be Function of (arity f1+1)-tuples_on NAT, HFuncs NAT such that
A2: for p being Element of (arity f1+1)-tuples_on NAT holds G.p =
primrec(f1,f2,i,p);
thus for k, n being Nat holds dom (G.(p+*(i,k))) c= dom (G.(p+*(i
,(k+n))))
proof
let k be Nat;
set pk = p+*(i,k);
defpred p[Nat] means dom (G.pk) c= dom(G.(p+*(i,(k+$1))));
A3: now
let n be Nat such that
A4: p[n];
reconsider m = k+n as Element of NAT by ORDINAL1:def 12;
set pkn1 = p+*(i,m+1);
set pkn = p+*(i,m);
consider F being sequence of HFuncs NAT such that
A5: primrec(f1,f2,i,pkn)= F.(pkn/.i) and
A6: i in dom pkn & Del(pkn,i) in dom f1 implies F.0 = pkn+*(i,0)
.--> (f1. Del(pkn,i)) and
A7: not i in dom pkn or not Del(pkn,i) in dom f1 implies F.0 = {} and
A8: for M being Nat holds Q[M, F.M qua Element of HFuncs
NAT, F.(M+1)qua Element of HFuncs NAT, pkn, i, f2] by Def10;
dom p = dom pkn1 by FUNCT_7:30;
then
A9: pkn1/.i = pkn1.i by A1,PARTFUN1:def 6
.= m+1 by A1,FUNCT_7:31;
consider F1 being sequence of HFuncs NAT such that
A10: primrec(f1,f2,i,pkn1)= F1.(pkn1/.i) and
A11: i in dom pkn1 & Del(pkn1,i) in dom f1 implies F1.0 = pkn1+*(i,0
) .--> (f1.Del(pkn1,i)) and
A12: not i in dom pkn1 or not Del(pkn1,i) in dom f1 implies F1.0 = {} and
A13: for M being Nat holds Q[M, F1.M qua Element of
HFuncs NAT, F1.(M+1)qua Element of HFuncs NAT, pkn1, i, f2] by Def10;
F1 = F by A6,A7,A8,A11,A12,A13,Lm2;
then
A14: G.(p+*(i,(k+(n+1)))) = F.(m+1) by A2,A10,A9;
dom p = dom pkn by FUNCT_7:30;
then pkn/.i = pkn.i by A1,PARTFUN1:def 6
.= m by A1,FUNCT_7:31;
then
A15: G.(p+*(i,(k+n))) = F.m by A2,A5;
per cases;
suppose
i in dom pkn & pkn+*(i,m) in dom (F.m) & (pkn+*(i,m))^<*(F.m)
.(pkn+*(i,m))*> in dom f2;
then F.(m+1) = (F.m)+*(pkn+*(i,m+1).--> f2.((pkn+*(i,m))^<*(F.m).(pkn
+*(i,m))*>)) by A8;
then
dom (F.(m+1)) = dom (F.m) \/ dom ({pkn+*(i,m+1)}--> f2.((pkn+*(i,
m))^<*(F.m).(pkn+*(i,m))*>)) by FUNCT_4:def 1;
then dom (F.m) c= dom (F.(m+1)) by XBOOLE_1:7;
hence p[n+1] by A4,A14,A15,XBOOLE_1:1;
end;
suppose
not i in dom pkn or not pkn+*(i,m) in dom (F.m) or not (pkn+*
(i,m))^<*(F.m).(pkn+*(i,m))*> in dom f2;
hence p[n+1] by A4,A8,A14,A15;
end;
end;
A16: p[0];
thus for n being Nat holds p[n] from NAT_1:sch 2(A16, A3);
end;
end;
Lm5: now
let f1,f2 be non empty homogeneous to-naturals NAT*-defined Function;
let p be Element of (arity f1+1)-tuples_on NAT;
let i, m be Element of NAT such that
A1: i in dom p;
let G be Function of (arity f1+1)-tuples_on NAT, HFuncs NAT such that
A2: for p being Element of (arity f1+1)-tuples_on NAT holds G.p =
primrec(f1,f2,i,p);
thus for k, n being Nat st not p+*(i,k) in dom (G.(p+*(i,k)))
holds not p+*(i,k) in dom (G.(p+*(i,(k+n))))
proof
let k be Nat;
set pk = p+*(i,k);
defpred p[Nat] means not pk in dom (G.pk) implies not pk in dom
(G.(p+*(i,(k+$1))));
A3: for n be Nat st p[n] holds p[n+1]
proof
let n be Nat such that
A4: p[n] and
A5: not pk in dom (G.pk);
reconsider m = k+n as Element of NAT by ORDINAL1:def 12;
set pkn = p+*(i,m);
consider F being sequence of HFuncs NAT such that
A6: primrec(f1,f2,i,pkn)= F.(pkn/.i) and
A7: i in dom pkn & Del(pkn,i) in dom f1 implies F.0 = pkn+*(i,0)
.--> (f1. Del(pkn,i)) and
A8: not i in dom pkn or not Del(pkn,i) in dom f1 implies F.0 = {} and
A9: for M being Nat holds Q[M, F.M qua Element of HFuncs
NAT, F.(M+1)qua Element of HFuncs NAT, pkn, i, f2] by Def10;
A10: dom p = dom pkn by FUNCT_7:30;
then pkn/.i = pkn.i by A1,PARTFUN1:def 6
.= m by A1,FUNCT_7:31;
then
A11: not pk in dom (F.m) by A2,A4,A5,A6;
set pkn1 = p+*(i,((k+n)+1));
consider F1 being sequence of HFuncs NAT such that
A12: primrec(f1,f2,i,pkn1)= F1.(pkn1/.i) and
A13: i in dom pkn1 & Del(pkn1,i) in dom f1 implies F1.0 = pkn1+*(i,0
) .--> (f1.Del(pkn1,i)) and
A14: not i in dom pkn1 or not Del(pkn1,i) in dom f1 implies F1.0 = {} and
A15: for M being Nat holds Q[M, F1.M qua Element of
HFuncs NAT, F1.(M+1)qua Element of HFuncs NAT, pkn1, i, f2] by Def10;
dom p = dom pkn1 by FUNCT_7:30;
then
A16: pkn1/.i = pkn1.i by A1,PARTFUN1:def 6
.= m+1 by A1,FUNCT_7:31;
F1 = F by A7,A8,A9,A13,A14,A15,Lm2;
then
A17: G.(p+*(i,(k+(n+1)))) = F.(m+1) by A2,A12,A16;
per cases;
suppose
i in dom pkn & pkn+*(i,m) in dom (F.m) & (pkn+*(i,m))^<*(F.m)
.(pkn+*(i,m))*> in dom f2;
then F.(m+1) = (F.m)+*(pkn+*(i,m+1).--> f2.((pkn+*(i,m))^<*(F.m).(pkn
+*(i,m))*>)) by A9;
then
dom (F.(m+1)) = dom (F.m) \/ dom ({pkn+*(i,m+1)}--> f2.((pkn+*(i,
m))^<*(F.m).(pkn+*(i,m))*>)) by FUNCT_4:def 1;
then
A18: dom (F.(m+1)) = dom (F.m) \/ {pkn+*(i,m+1)};
k <= k+n by NAT_1:11;
then
A19: k <> m+1 by NAT_1:13;
A20: pk.i = k by A1,FUNCT_7:31;
(pkn+*(i,m+1)).i = m+1 by A1,A10,FUNCT_7:31;
then not pk in {pkn+*(i,m+1)} by A19,A20,TARSKI:def 1;
hence thesis by A11,A17,A18,XBOOLE_0:def 3;
end;
suppose
not i in dom pkn or not pkn+*(i,m) in dom (F.m) or not (pkn+*
(i,m))^<*(F.m).(pkn+*(i,m))*> in dom f2;
hence thesis by A9,A11,A17;
end;
end;
A21: p[0];
thus for n being Nat holds p[n] from NAT_1:sch 2(A21, A3);
end;
end;
Lm6: for i,m being Nat holds
i in dom p implies (p+*(i,0) in dom primrec(f1,f2,i) iff Del(p,i) in dom
f1) & (p+*(i,0) in dom primrec(f1,f2,i) implies primrec(f1,f2,i).(p+*(i,0)) =
f1.Del(p,i)) & (p+*(i,m+1) in dom primrec(f1,f2,i) iff p+*(i,m) in dom primrec(
f1,f2,i) & (p+*(i,m))^<*primrec(f1,f2,i).(p+*(i,m))*> in dom f2) & (p+*(i,m+1)
in dom primrec(f1,f2,i) implies primrec(f1,f2,i).(p+*(i,m+1)) = f2.((p+*(i,m))^
<*primrec(f1,f2,i).(p+*(i,m))*>))
proof let i,m be Nat;
set p0 = p+*(i,0);
consider G being Function of (arity f1+1)-tuples_on NAT, HFuncs NAT such
that
A1: primrec(f1,f2,i) = Union G and
A2: for p being Element of (arity f1+1)-tuples_on NAT holds G.p =
primrec(f1,f2,i,p) by Def11;
reconsider rngG = rng G as functional compatible set by A1,Th10;
assume
A3: i in dom p;
A4: now
let k be Element of NAT such that
A5: p+*(i,k) in dom primrec(f1,f2,i) and
A6: not p+*(i,k) in dom (G.((p+*(i,k))));
union rngG <> {} by A1,A5;
then reconsider rngG = rng G as non empty functional compatible set;
set pk = p+*(i,k);
dom union rngG = union the set of all dom f where f is Element of rngG
by Th11;
then consider X being set such that
A7: pk in X and
A8: X in the set of all dom f where f is Element of rngG by A1,A5,
TARSKI:def 4;
consider f being Element of rngG such that
A9: X = dom f by A8;
consider pp being object such that
A10: pp in dom G and
A11: f = G.pp by FUNCT_1:def 3;
reconsider pp as Element of (arity f1+1)-tuples_on NAT by A10;
G.pp = primrec(f1,f2,i,pp) by A2;
then
A12: ex m being Element of NAT st pk = pp+*(i,m) by A7,A9,A11,Th48;
set ppi = pp.i;
A13: p+*(i,ppi) = pk+*(i,ppi) by FUNCT_7:34
.= pp+*(i,ppi) by A12,FUNCT_7:34
.= pp by FUNCT_7:35;
per cases by XXREAL_0:1;
suppose
k = ppi;
hence contradiction by A6,A7,A9,A11,A13;
end;
suppose
ppi < k;
then consider m being Nat such that
A14: k = ppi+m by NAT_1:10;
reconsider m as Element of NAT by ORDINAL1:def 12;
k = ppi+m by A14;
then dom (G.pp) c= dom (G.pk) by A3,A2,A13,Lm4;
hence contradiction by A6,A7,A9,A11;
end;
suppose
ppi > k;
then consider m being Nat such that
A15: ppi=k+m by NAT_1:10;
reconsider m as Element of NAT by ORDINAL1:def 12;
ppi=k+m by A15;
hence contradiction by A3,A2,A6,A7,A9,A11,A13,Lm5;
end;
end;
A16: dom p = dom p0 by FUNCT_7:30;
A17: now
A18: p0 in {p0} by TARSKI:def 1;
A19: p0/.i = p0.i by A3,A16,PARTFUN1:def 6
.= 0 by A3,FUNCT_7:31;
consider F being sequence of HFuncs NAT such that
A20: primrec(f1,f2,i,p0)= F.(p0/.i) and
A21: i in dom p0 & Del(p0,i) in dom f1 implies F.0 = p0+*(i,0) .--> (
f1.Del(p0,i)) and
A22: not i in dom p0 or not Del(p0,i) in dom f1 implies F.0 = {} and
for m being Nat holds Q[m, F.m qua Element of HFuncs NAT ,
F.(m+1)qua Element of HFuncs NAT, p0, i, f2] by Def10;
A23: G.p0 = primrec(f1,f2,i,p0) by A2;
thus p0 in dom (G.p0) iff Del(p,i) in dom f1
proof
thus p0 in dom (G.p0) implies Del(p,i) in dom f1 by A2,A20,A22,A19,Th3;
assume Del(p,i) in dom f1;
then dom (F.0) = { p0} by A3,A21,Th3,FUNCT_7:30,34;
hence thesis by A23,A20,A19,TARSKI:def 1;
end;
assume p0 in dom (G.p0);
then F.0 = {p0} --> (f1.Del(p0,i)) by A2,A20,A21,A22,A19,FUNCT_7:34;
then F.0 = {p0} --> (f1.Del(p,i)) by Th3;
hence (G.p0).p0 = f1.Del(p,i) by A23,A20,A19,A18,FUNCOP_1:7;
end;
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
set pm1 = p+*(i,mm+1), pm = p+*(i,mm), pc = <*(G.pm1).(pm1+*(i,m))*>;
A24: dom G = (arity f1+1)-tuples_on NAT by FUNCT_2:def 1;
then
A25: G.pm1 in rng G by FUNCT_1:def 3;
reconsider rngG as non empty functional compatible set;
A26: G.p0 in rng G by A24,FUNCT_1:def 3;
thus p+*(i,0) in dom primrec(f1,f2,i) iff Del(p,i) in dom f1
proof
thus p+*(i,0) in dom primrec(f1,f2,i) implies Del(p,i) in dom f1 by A4,A17;
assume
A27: Del(p,i) in dom f1;
dom (G.p0) in the set of all dom f where f is Element of rngG by A26;
then p0 in union the set of all dom f where f is Element of rngG by
A17,A27,TARSKI:def 4;
hence thesis by A1,Th11;
end;
hereby
assume
A28: p+*(i,0) in dom primrec(f1,f2,i);
then p0 in dom (G.p0) by A4;
then (union rngG).p0 = (G.p0).p0 by A26,Th12;
hence primrec(f1,f2,i).(p+*(i,0)) = f1.Del(p,i) by A1,A4,A17,A28;
end;
A29: dom p = dom pm1 by FUNCT_7:30;
A30: pm1+*(i,m+1) = pm1 by FUNCT_7:34;
A31: pm1+*(i,m) = pm by FUNCT_7:34;
A32: dom p = dom pm by FUNCT_7:30;
A33: now
A34: pm/.i = pm.i by A3,A32,PARTFUN1:def 6
.= m by A3,FUNCT_7:31;
consider F being sequence of HFuncs NAT such that
A35: primrec(f1,f2,i,pm)= F.(pm/.i) and
A36: i in dom pm & Del(pm,i) in dom f1 implies F.0 = pm+*(i,0) .--> (
f1.Del (pm,i)) and
A37: not i in dom pm or not Del(pm,i) in dom f1 implies F.0 = {} and
A38: for M being Nat holds Q[M, F.M qua Element of HFuncs
NAT, F.(M+1) qua Element of HFuncs NAT, pm, i, f2] by Def10;
A39: G.pm1 = primrec(f1,f2,i,pm1) by A2;
consider F1 being sequence of HFuncs NAT such that
A40: primrec(f1,f2,i,pm1)= F1.(pm1/.i) and
A41: i in dom pm1 & Del(pm1,i) in dom f1 implies F1.0 = pm1+*(i,0)
.--> (f1 .Del(pm1,i)) and
A42: not i in dom pm1 or not Del(pm1,i) in dom f1 implies F1.0 = {} and
A43: for M being Nat holds Q[M, F1.M qua Element of HFuncs
NAT, F1.(M+1) qua Element of HFuncs NAT, pm1, i, f2] by Def10;
A44: F1.(m+1).pm = F1.m.pm by A3,A41,A42,A43,Lm3;
A45: pm1 in {pm1} by TARSKI:def 1;
then
A46: pm1 in dom ({pm1}--> f2.((pm)^<*(F1.m).pm*>));
A47: G.pm = primrec(f1,f2,i,pm) by A2;
A48: pm1/.i = pm1.i by A3,A29,PARTFUN1:def 6
.= m+1 by A3,FUNCT_7:31;
A49: F1.m = F.m by A41,A42,A43,A36,A37,A38,Lm2;
A50: not pm1 in dom (F1.m) by A3,A41,A42,A43,Lm3;
thus
A51: pm1 in dom (G.pm1) iff pm in dom (G.pm) & pm^pc in dom f2
proof
hereby
assume
A52: pm1 in dom (G.pm1);
then
A53: pm1 in dom (F1.(m+1)) by A2,A40,A48;
assume
A54: not (pm in dom (G.pm) & pm^pc in dom f2);
per cases by A54;
suppose
not pm in dom (G.pm);
then not pm in dom (F1.m) by A2,A35,A34,A49;
hence contradiction by A31,A43,A50,A53;
end;
suppose
not pm^pc in dom f2;
hence contradiction by A31,A39,A40,A43,A48,A44,A50,A52;
end;
end;
assume that
A55: pm in dom (G.pm) and
A56: pm^pc in dom f2;
pm1 in {pm1} by TARSKI:def 1;
then pm1 in dom ({pm1}--> f2.((pm)^<*(F1.m).pm*>));
then
A57: pm1 in dom (F1.m) \/ dom ({pm1}--> f2.((pm)^<*(F1.m).pm*>)) by
XBOOLE_0:def 3;
F1.(m+1) = (F1.m)+*(pm1.--> f2.((pm)^<*(F1.m).pm*>)) by A3,A29,A31,A30
,A39,A47,A40,A43,A35,A48,A34,A49,A44,A55,A56;
hence thesis by A39,A40,A48,A57,FUNCT_4:def 1;
end;
assume
A58: pm1 in dom (G.pm1);
then pm^<*(F1.m).pm*> in dom f2 by A31,A39,A40,A43,A48,A51;
then F1.(m+1) = (F1.m)+*(pm1.--> f2.((pm)^<*(F1.m).pm*>)) by A3,A29,A31,A30
,A47,A43,A35,A34,A49,A51,A58;
hence G.(pm1).pm1 = ({pm1}-->f2.((pm)^<*(F1.m).pm*>)).pm1 by A39,A40,A48
,A46,FUNCT_4:13
.= f2.(pm^pc) by A31,A39,A40,A48,A44,A45,FUNCOP_1:7;
end;
thus p+*(i,m+1) in dom primrec(f1,f2,i) iff p+*(i,m) in dom primrec(f1,f2,i
) & (p+*(i,m))^<*primrec(f1,f2,i).(p+*(i,m))*> in dom f2
proof
hereby
assume
A59: p+*(i,m+1) in dom primrec(f1,f2,i);
G.pm in rng G by A24,FUNCT_1:def 3;
then dom (G.pm) in the set of all dom f where f is Element of rngG;
then pm in union the set of all dom f where f is Element of rngG
by A4,A33,A59,TARSKI:def 4;
hence p+*(i,m) in dom primrec(f1,f2,i) by A1,Th11;
A60: G.pm1 in rng G by A24,FUNCT_1:def 3;
dom (G.pm) c= dom (G.pm1) by A3,A2,Lm4;
then (union rngG).pm = (G.pm1).pm by A4,A33,A59,A60,Th12;
hence (p+*(i,m))^<*primrec(f1,f2,i).(p+*(i,m))*> in dom f2
by A1,A4,A33,A59,FUNCT_7:34;
end;
assume that
A61: p+*(i,m) in dom primrec(f1,f2,i) and
A62: (p+*(i,m))^<*primrec(f1,f2,i).(p+*(i,m))*> in dom f2;
A63: G.pm1 in rng G by A24,FUNCT_1:def 3;
G.pm1 in rng G by A24,FUNCT_1:def 3;
then
A64: dom (G.pm1)in the set of all dom f where f is Element of rngG;
A65: dom (G.pm) c= dom (G.pm1) by A3,A2,Lm4;
pm in dom (G.pm) by A4,A61;
then pm1 in union the set of all dom f where f is Element of rngG
by A1,A31,A33,A62,A64,A63,A65,Th12,TARSKI:def 4;
hence thesis by A1,Th11;
end;
assume
A66: p+*(i,m+1) in dom primrec(f1,f2,i);
A67: dom (G.pm) c= dom (G.pm1) by A3,A2,Lm4;
then
A68: (union rngG).pm1 = (G.pm1).pm1 by A4,A66,A25,Th12;
(union rngG).pm = (G.pm1).pm by A4,A33,A66,A25,A67,Th12;
hence thesis by A1,A4,A33,A66,A68,FUNCT_7:34;
end;
theorem
i in dom p implies (p+*(i,0) in dom primrec(f1,f2,i) iff Del(p,i) in dom f1)
by Lm6;
theorem
i in dom p & p+*(i,0) in dom primrec(f1,f2,i) implies
primrec(f1,f2,i).(p+*(i,0)) = f1.Del(p,i) by Lm6;
theorem Th59:
i in dom p & f1 is len-total implies
primrec(f1,f2,i).(p+*(i,0)) = f1.Del(p,i)
proof
assume that
A1: i in dom p and
A2: f1 is len-total;
A3: Del(p,i) is FinSequence of NAT by FINSEQ_3:105;
len p = arity f1+1 by CARD_1:def 7;
then len Del(p,i) = arity f1 by A1,FINSEQ_3:109;
then
A4: Del(p,i) is Element of (arity f1)-tuples_on NAT by A3,FINSEQ_2:92;
dom f1 = (arity f1)-tuples_on NAT by A2,Th22;
then p+*(i,0) in dom primrec(f1,f2,i) by A1,A4,Lm6;
hence thesis by A1,Lm6;
end;
theorem
i in dom p implies (p+*(i,m+1) in dom primrec(f1,f2,i) iff
p+*(i,m) in dom primrec(f1,f2,i) &
(p+*(i,m))^<*primrec(f1,f2,i).(p+*(i,m))*> in dom f2) by Lm6;
theorem
i in dom p & p+*(i,m+1) in dom primrec(f1,f2,i) implies
primrec(f1,f2,i).(p+*(i,m+1)) =
f2.((p+*(i,m))^<*primrec(f1,f2,i).(p+*(i,m))*>) by Lm6;
theorem Th62:
f1 is len-total & f2 is len-total & arity f1 +2 = arity f2 &
1 <= i & i <= 1+arity f1 implies
primrec(f1,f2,i).(p+*(i,m+1)) =
f2.((p+*(i,m))^<*primrec(f1,f2,i).(p+*(i,m))*>)
proof
assume that
A1: f1 is len-total and
A2: f2 is len-total and
A3: arity f1 +2 = arity f2 and
A4: 1 <= i and
A5: i <= 1+arity f1;
len p = arity f1 +1 by CARD_1:def 7;
then
A6: i in dom p by A4,A5,FINSEQ_3:25;
(p+*(i,m+1)) in (arity f1 +1)-tuples_on NAT;
then (p+*(i,m+1)) in dom primrec(f1,f2,i) by A1,A2,A3,A4,A5,Th56;
hence thesis by A6,Lm6;
end;
theorem Th63:
arity f1+2 = arity f2 & 1 <= i & i <= arity f1+1 implies
primrec(f1,f2,i) is_primitive-recursively_expressed_by f1,f2,i
proof
assume that
A1: arity f1+2 = arity f2 and
A2: 1 <= i and
A3: i <= arity f1+1;
take n = arity f1+1;
set g = primrec(f1,f2,i);
thus dom g c= n-tuples_on NAT by Th55;
thus i >= 1 & i <= n by A2,A3;
thus arity f1+1 = n;
thus n+1 = arity f2 by A1;
let p be FinSequence of NAT;
assume
A4: len p = n;
then
A5: i in dom p by A2,A3,FINSEQ_3:25;
A6: p is Element of n-tuples_on NAT by A4,FINSEQ_2:92;
hence p+*(i,0) in dom g iff Del(p,i) in dom f1 by A5,Lm6;
thus p+*(i,0) in dom g implies g.(p+*(i,0)) = f1.Del(p,i) by A6,A5,Lm6;
let m be Nat;
thus p+*(i,m+1) in dom g iff p+*(i,m) in dom g & (p+*(i,m))^<*g.(p+*(i,m))*>
in dom f2 by A6,A5,Lm6;
thus p+*(i,m+1) in dom g implies g.(p+*(i,m+1)) = f2.((p+*(i,m))^<*g.(p+*(i,
m))*>) by A6,A5,Lm6;
end;
theorem
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)
proof
assume that
A1: i >= 1 and
A2: i <= arity f1+1;
let g be Element of HFuncs NAT;
set n = arity f1+1, h = primrec(f1,f2,i);
given n9 being Element of NAT such that
A3: dom g c= n9-tuples_on NAT and
i >= 1 and
i <= n9 and
A4: (arity f1)+1 = n9 and
n9+1 = arity f2 and
A5: for p being FinSequence of NAT st len p = n9 holds (p+*(i,0) in dom
g iff Del(p,i) in dom f1) & (p+*(i,0) in dom g implies g.(p+*(i,0)) = f1.Del(p,
i)) & for n 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))*>));
A6: now
let p be Element of n-tuples_on NAT;
defpred p[Nat] means (p+*(i,$1) in dom g iff p+*(i,$1) in dom h
) & (p+*(i,$1) in dom g implies g.(p+*(i,$1)) = h.(p+*(i,$1)));
set k = p/.i;
A7: p = p+*(i,k) by FUNCT_7:38;
A8: len p = n by CARD_1:def 7;
then
A9: i in dom p by A1,A2,FINSEQ_3:25;
A10: for m be Nat st p[m] holds p[m+1]
proof
let m being Nat such that
A11: p+*(i,m) in dom g iff p+*(i,m) in dom h and
A12: p+*(i,m) in dom g implies g.(p+*(i,m)) = h.(p+*(i,m));
p+*(i,m+1) in dom g iff p+*(i,m) in dom g & (p+*(i,m))^<*g.(p+*(i,m
))*> in dom f2 by A4,A5,A8;
hence p+*(i,m+1) in dom g iff p+*(i,m+1) in dom h by A9,A11,A12,Lm6;
A13: p+*(i,m+1) in dom h iff p+*(i,m) in dom h & (p+*(i,m))^<*h.(p+*(i,m
))*> in dom f2 by A9,Lm6;
assume
A14: p+*(i,m+1) in dom g;
then g.(p+*(i,m+1)) = f2.((p+*(i,m))^<*g.(p+*(i,m))*>) by A4,A5,A8;
hence thesis by A4,A5,A8,A9,A11,A12,A13,A14,Lm6;
end;
A15: p+*(i,0) in dom h iff Del(p,i) in dom f1 by A9,Lm6;
then
p+*(i,0) in dom g implies g.(p+*(i,0)) = f1.Del(p,i) & h.(p+*(i,0)) =
f1.Del(p,i) by A4,A5,A8,A9,Lm6;
then
A16: p[0] by A4,A5,A8,A15;
for m being Nat holds p[m] from NAT_1:sch 2(A16,A10);
hence (p in dom g iff p in dom h) & (p in dom g implies g.p = h.p) by A7;
end;
A17: dom h c= n-tuples_on NAT by Th55;
then
A18: dom g = dom h by A3,A4,A6;
for x being object st x in dom h holds g.x = h.x by A17,A6;
hence thesis by A18;
end;
begin :: The set of primitive recursive functions
definition
let X be set;
attr X is composition_closed means
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
for g,f1,f2 being Element of HFuncs NAT, i being 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
:Def14:
0 const 0 in X & 1 succ 1 in X &
(for n,i being Nat st 1 <= i & i <= n holds n proj i in X)
& X is composition_closed & X is primitive-recursion_closed;
end;
theorem Th65:
HFuncs NAT is primitive-recursively_closed
proof
set X = HFuncs NAT;
thus 0 const 0 in X & 1 succ 1 in X & for n,i being Nat st 1<=i &
i <= n holds n proj i in X by Th30,Th32,Th34;
thus 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 by Th41;
let g be Element of HFuncs NAT;
thus thesis;
end;
registration
cluster primitive-recursively_closed non empty for Subset of HFuncs NAT;
existence
proof
HFuncs NAT c= HFuncs NAT;
then reconsider X = HFuncs NAT as non empty Subset of HFuncs NAT;
take X;
thus thesis by Th65;
end;
end;
reserve P for primitive-recursively_closed non empty Subset of HFuncs NAT;
Lm7: for X being non empty set, n,i be Element of NAT st 1 <= i & i <= n for x
being Element of X for p being Element of n-tuples_on X holds p+*(i,x) in n
-tuples_on X;
theorem Th66:
for g being Element of HFuncs NAT st e1 = {} &
g is_primitive-recursively_expressed_by e1, e2, i holds g = {}
proof
set f1 = e1, f2 = e2;
let g be Element of HFuncs(NAT);
assume
A1: f1 = {};
assume g is_primitive-recursively_expressed_by f1, f2, i;
then consider n being Element of NAT such that
A2: dom g c= n-tuples_on NAT and
i >= 1 and
i <= n and
(arity f1)+1 = n and
n+1 = arity f2 and
A3: for p 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))*>));
A4: now
let y be Element of n-tuples_on NAT;
defpred p[Nat] means not y+*(i,$1) in dom g;
A5: len y = n by CARD_1:def 7;
then
A6: for k being Nat st p[k] holds p[k+1] by A3;
A7: p[0] by A1,A3,A5;
thus for k being Nat holds p[k] from NAT_1:sch 2(A7, A6);
end;
assume g <> {};
then consider x being object such that
A8: x in dom g by XBOOLE_0:def 1;
reconsider x as Element of n-tuples_on NAT by A2,A8;
set xi = x.i;
x = x+*(i,xi) by FUNCT_7:35;
hence contradiction by A4,A8;
end;
theorem Th67:
for g being Element of HFuncs(NAT),
f1, f2 being quasi_total Element of HFuncs(NAT), i being Nat st
g is_primitive-recursively_expressed_by f1, f2, i holds g is quasi_total &
(f1 is non empty implies g is non empty)
proof
let g be Element of HFuncs(NAT),
f1, f2 be quasi_total Element of HFuncs(NAT),
i be Nat;
assume
A1: g is_primitive-recursively_expressed_by f1, f2, i;
then consider n being Element of NAT such that
A2: dom g c= n-tuples_on NAT and
A3: i >= 1 and
A4: i <= n and
A5: (arity f1)+1 = n and
A6: n+1 = arity f2 and
A7: for p 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))*>));
reconsider f29 = f2 as non empty quasi_total Element of HFuncs(NAT) by A6
,Th17;
per cases;
suppose
f1 is empty;
hence thesis by A1,Th66;
end;
suppose
f1 is non empty;
then
A8: dom f1 = (arity f1)-tuples_on NAT by Th21;
A9: g is quasi_total
proof
let x, y be FinSequence of NAT such that
A10: len x = len y and
A11: x in dom g;
defpred p[Nat] means y+*(i,$1) in dom g;
A12: len x = n by A2,A11,CARD_1:def 7;
A13: now
let k be Nat such that
A14: p[k];
A15: dom f29 = (arity f2)-tuples_on NAT by Th21;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
len ((y+*(i,k))^<*g.(y+*(i,k))*>) = len (y+*(i,k)) + len <*g.(y+*
(i,k))*> by FINSEQ_1:22
.= n+len <*g.(y+*(i,k))*> by A10,A12,FUNCT_7:97
.= n+1 by FINSEQ_1:39;
then (y+*(i,kk))^<*g.(y+*(i,kk))*> is Element of dom f2 by A6,A15,
FINSEQ_2:92;
then (y+*(i,k))^<*g.(y+*(i,k))*> in dom f29;
hence p[k+1] by A7,A10,A12,A14;
end;
y is Element of (len y)-tuples_on NAT by FINSEQ_2:92;
then Del(y,i) in (arity f1)-tuples_on NAT by A3,A4,A5,A10,A12,Th9;
then
A16: p[0] by A7,A8,A10,A12;
for k being Nat holds p[k] from NAT_1:sch 2(A16, A13);
then
A17: y+*(i,y/.i) in dom g;
i in dom y by A3,A4,A10,A12,FINSEQ_3:25;
then y.i = y/.i by PARTFUN1:def 6;
hence y in dom g by A17,FUNCT_7:35;
end;
consider pp being object such that
A18: pp in n-tuples_on NAT by XBOOLE_0:def 1;
pp is Element of n-tuples_on NAT by A18;
then reconsider p = pp as FinSequence of NAT;
A19: len p = n by A18,CARD_1:def 7;
Del(p,i) in (arity f1)-tuples_on NAT by A3,A4,A5,A18,Th9;
hence thesis by A7,A19,A8,A9;
end;
end;
theorem Th68:
n const c in P
proof
defpred p[Nat] means 0 const $1 in P;
defpred r[Nat] means for c being Nat holds $1 const c in P;
A1: P is composition_closed by Def14;
A2: for i be Nat st p[i] holds p[i+1]
proof
reconsider 1succ1 = 1 succ 1 as quasi_total Element of HFuncs NAT by Th28;
let i be Nat;
A3: (1 succ 1) in P by Def14;
A4: <*>NAT is Element of 0-tuples_on NAT by FINSEQ_2:131;
then
A5: (0 const i).{} = i;
reconsider 0consti = 0 const i as Element of HFuncs NAT by Th27;
set F = <*0 const i*>;
<*0consti*> is FinSequence of HFuncs NAT;
then reconsider F as with_the_same_arity FinSequence of HFuncs NAT;
assume 0 const i in P;
then
A6: {0 const i} c= P by ZFMISC_1:31;
A7: arity (1 succ 1) = len F by FINSEQ_1:39;
A8: rng F = {0 const i} by FINSEQ_1:39;
reconsider i1=i as Element of NAT by ORDINAL1:def 12;
now
let h be Element of HFuncs NAT;
assume h in rng F;
then h = 0 const i1 by A8,TARSKI:def 1;
hence h is quasi_total by Th28;
end;
then reconsider
g = (1succ1)*<:F:> as quasi_total Element of HFuncs NAT by A7,Th45;
A9: arity (0 const (i+1)) = 0;
A10: (0 const (i+1)).{} = i+1 by A4;
A11: dom (1 succ 1) = 1-tuples_on NAT by Def7;
A12: arity (0 const i1) = 0;
dom (0 const i1) = 0 -tuples_on NAT;
then
A14: <:F:>.{} = <*i*> by A4,A5,FINSEQ_3:141;
reconsider ii= <*i1*> as Element of 1-tuples_on NAT by FINSEQ_2:131;
A15: dom <:<*0 const i*>:> = dom (0 const i) by FINSEQ_3:141;
then g.{} = (1 succ 1).(<:F:>.{}) by A4,FUNCT_1:13;
then
A16: g.{} = (ii.1)+1 by A14,Def7
.= i1+1;
dom (0 const i) = 0-tuples_on NAT;
then <:<*0 const i*>:>.{} = ii by A4,A5,FINSEQ_3:141;
then
A18: {} in dom g by A4,A15,A11,FUNCT_1:11;
0 const i in rng F by A8,TARSKI:def 1;
then arity F = 0 by A12,Def4;
then arity g = 0 by A18,Th43,RELAT_1:38;
then 0 const (i+1) = (1 succ 1)*<:<*0 const i*>:> by A9,A10,A18,A16,Th47,
RELAT_1:38;
hence thesis by A1,A6,A8,A3,A7;
end;
A19: P is primitive-recursion_closed by Def14;
A20: now
let n be Nat such that
A21: r[n];
thus r[n+1]
proof
let i;
reconsider i,nn=n as Element of NAT by ORDINAL1:def 12;
set g=(nn+1) const i, f1=nn const i,j=n+1,f2=(nn+2) proj (nn+2);
A23: n+(1+1) = j+1;
then 1 <= n+2 by NAT_1:11;
then
A24: f2 in P by Def14;
A26: dom f2 = (n+2)-tuples_on NAT by Th35;
A30: g is_primitive-recursively_expressed_by f1,f2,n+1
proof
take m = arity g;
thus dom g c= m-tuples_on NAT;
thus j >= 1 & j <= m by NAT_1:11;
thus (arity f1)+1 = m & m+1 = arity f2;
let p be FinSequence of NAT;
assume len p = m;
then
A31: p is Element of j-tuples_on NAT by FINSEQ_2:92;
A32: j >= 1 by NAT_1:11;
hence p+*(j,0) in dom g implies Del(p,j) in dom f1 by A31,Th9;
thus Del(p,j) in dom f1 implies p+*(j,0) in dom g by A31,A32,Lm7;
f1.Del(p,j) = i by A31,A32,Th9,FUNCOP_1:7;
hence p+*(j,0) in dom g implies g.(p+*(j,0)) = f1.Del(p,j)
by FUNCOP_1:7;
let m be Nat;
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
A33: p+*(j,mm) in j-tuples_on NAT by A31,A32,Lm7;
then
A34: (p+*(j,mm))^<*i*> is Tuple of n+2, NAT by A23; then
A35: (p+*(j,m))^<*i*> is Element of (n+2)-tuples_on NAT by FINSEQ_2:131;
hereby
hereby
assume p+*(j,m+1) in dom g;
p+*(j,mm) in dom g by A31,A32,Lm7;
hence p+*(j,m) in dom g;
g.(p+*(j,mm)) = i by A31,A32,Lm7,FUNCOP_1:7;
hence (p+*(j,m))^<*g.(p+*(j,m))*> in dom f2
by A26,A34,FINSEQ_2:131;
end;
thus p+*(j,m) in dom g & (p+*(j,m))^<*g.(p+*(j,m))*> in dom f2
implies p+*(j,m+1) in dom g by A31,A32,Lm7;
end;
assume p+*(j,m+1) in dom g;
len (p+*(j,m)) = j by A33,CARD_1:def 7;
then
A36: ((p+*(j,m))^<*i*>).(j+1) = i by FINSEQ_1:42;
thus g.(p+*(j,m+1)) = i by A31,A32,Lm7,FUNCOP_1:7
.= f2.((p+*(j,m))^<*i*>) by A36,A35,Th37
.= f2.((p+*(j,mm))^<*g.(p+*(j,mm))*>) by A31,A32,Lm7,FUNCOP_1:7
.= f2.((p+*(j,m))^<*g.(p+*(j,m))*>);
end;
A37: f1 in P by A21;
(n+1) const i is Element of HFuncs NAT by Th27;
hence thesis by A19,A30,A37,A24;
end;
end;
A38: p[0] by Def14;
for i being Nat holds p[i] from NAT_1:sch 2(A38,A2);
then
A39: r[0];
for n being Nat holds r[n] from NAT_1:sch 2(A39,A20);
hence thesis;
end;
theorem Th69:
1 <= i & i <= n implies n succ i in P
proof
A1: 1 succ 1 in P by Def14;
A2: arity (1 succ 1) = len <*n proj i*> by FINSEQ_1:39;
reconsider nproji = n proj i as Element of HFuncs NAT by Th27;
assume that
A3: 1 <= i and
A4: i <= n;
A5: <*nproji*> is with_the_same_arity FinSequence of HFuncs NAT;
now
rng (n proj i) = NAT by A3,A4,Th35;
then
A6: rng <:<*n proj i*>:> = 1-tuples_on NAT by Th8;
thus dom (n succ i) = n-tuples_on NAT by Def7;
A7: dom (n proj i) = n-tuples_on NAT by Th35;
then
A8: dom <:<*n proj i*>:> = n-tuples_on NAT by FINSEQ_3:141;
dom (1 succ 1) = 1-tuples_on NAT by Def7;
hence
dom ((1 succ 1)*<:<*n proj i*>:>)=n-tuples_on NAT by A8,A6,RELAT_1:27;
let x be object;
assume x in n-tuples_on NAT;
then reconsider x9 = x as Element of n-tuples_on NAT;
set xi = x9.i;
A10: (n succ i).x = xi+1 by Def7;
reconsider ii= <*xi*> as Element of 1-tuples_on NAT by FINSEQ_2:131;
((1 succ 1)*<:<*n proj i*>:>).x9 = (1 succ 1).(<:<*n proj i*>:>.x9)
by A8,FUNCT_1:13
.= (1 succ 1).<*(n proj i).x9*> by A7,FINSEQ_3:141
.= (1 succ 1).<*x9.i*> by Th37
.= (ii.1)+1 by Def7
.= xi+1;
hence (n succ i).x = ((1 succ 1)*<:<*n proj i*>:>).x by A10;
end;
then
A11: n succ i = (1 succ 1)*<:<*n proj i*>:>;
A12: rng <*n proj i*> c= P
proof
let x be object;
assume x in rng <*n proj i*>;
then x in {n proj i} by FINSEQ_1:39;
then x = n proj i by TARSKI:def 1;
hence thesis by A3,A4,Def14;
end;
P is composition_closed by Def14;
hence thesis by A11,A1,A2,A12,A5;
end;
theorem Th70:
{} in P
proof
reconsider F = {} as with_the_same_arity Element of (HFuncs NAT)* by
FINSEQ_1:49;
set f = 0 const 0;
A1: rng {} c= P;
A2: arity f = 0;
A3: P is composition_closed by Def14;
f in P by Th68;
then f*<:F:> in P by A2,A1,A3,CARD_1:27;
hence thesis by FUNCT_6:40;
end;
theorem Th71:
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
proof
let f be Element of P, F being with_the_same_arity FinSequence of P;
assume
A1: arity f = len F;
A2: rng F c= P by FINSEQ_1:def 4;
per cases;
suppose
f is empty;
then f*<:F:> = {};
hence thesis by Th70;
end;
suppose
f is non empty;
then reconsider f9 = f as non empty Element of HFuncs NAT;
A3: P* c= (HFuncs NAT)* by FINSEQ_1:62;
F in P* by FINSEQ_1:def 11;
then reconsider F9 = F as with_the_same_arity Element of (HFuncs NAT)*
by A3;
P is composition_closed by Def14;
then f9*<:F9:> in P by A1,A2;
hence thesis;
end;
end;
theorem Th72:
for f1,f2 being Element of P st arity f1+2 = arity f2
for i being Nat st
1 <= i & i <= arity f1+1 holds primrec(f1,f2,i) in P
proof
let f1,f2 be Element of P;
assume
A1: arity f1+2 = arity f2;
let i be Nat;
assume that
A2: 1 <= i and
A3: i <= arity f1+1;
A4: P is primitive-recursion_closed by Def14;
per cases;
suppose
f1 is empty;
then primrec(f1,f2,i) is empty by Th54;
hence thesis by Th70;
end;
suppose
f1 is non empty;
then primrec(f1,f2,i) is_primitive-recursively_expressed_by f1,f2,i
by A1,A2,A3,Th17,Th63;
hence thesis by A4;
end;
end;
definition
func PrimRec -> Subset of HFuncs(NAT) equals
meet {R where R is Subset of HFuncs(NAT): R is primitive-recursively_closed};
coherence
proof
set S = { R where R is Subset of HFuncs(NAT) :
R is primitive-recursively_closed };
A1: {HFuncs(NAT)} c= bool HFuncs(NAT) by ZFMISC_1:68;
HFuncs(NAT) in {HFuncs(NAT)} by TARSKI:def 1;
then HFuncs(NAT) in S by A1,Th65;
then meet S c= HFuncs(NAT) by SETFAM_1:def 1;
hence thesis;
end;
end;
theorem Th73:
for X being Subset of HFuncs(NAT) st X is primitive-recursively_closed
holds PrimRec c= X
proof
let X be Subset of HFuncs(NAT);
set S = { R where R is Subset of HFuncs(NAT) : R is
primitive-recursively_closed };
assume X is primitive-recursively_closed;
then
A1: X in S;
let x be object;
assume x in PrimRec;
hence thesis by A1,SETFAM_1:def 1;
end;
registration
cluster PrimRec -> non empty primitive-recursively_closed;
coherence
proof
set S = { R where R is Subset of HFuncs(NAT) : R is
primitive-recursively_closed };
A1: {HFuncs(NAT)} c= bool HFuncs(NAT) by ZFMISC_1:68;
HFuncs(NAT) in {HFuncs(NAT)} by TARSKI:def 1;
then
A2: HFuncs(NAT) in S by A1,Th65;
A3: now
let Y be set;
assume Y in S;
then ex R being Subset of HFuncs(NAT) st R = Y & R is
primitive-recursively_closed;
hence 0 const 0 in Y;
end;
hence PrimRec is non empty by A2,SETFAM_1:def 1;
thus PrimRec is primitive-recursively_closed
proof
thus 0 const 0 in PrimRec by A2,A3,SETFAM_1:def 1;
now
let Y be set;
assume Y in S;
then ex R being Subset of HFuncs(NAT) st R = Y & R is
primitive-recursively_closed;
hence 1 succ 1 in Y;
end;
hence 1 succ 1 in PrimRec by A2,SETFAM_1:def 1;
hereby
let n, i;
assume that
A4: 1 <= i and
A5: i <= n;
now
let Y be set;
assume Y in S;
then ex R being Subset of HFuncs(NAT) st R = Y & R is
primitive-recursively_closed;
hence n proj i in Y by A4,A5;
end;
hence n proj i in PrimRec by A2,SETFAM_1:def 1;
end;
hereby
let f be Element of HFuncs NAT, F being with_the_same_arity
FinSequence of HFuncs NAT such that
A6: f in PrimRec and
A7: arity f = len F and
A8: rng F c= PrimRec;
now
let Y be set;
assume
A9: Y in S;
then consider R being Subset of HFuncs(NAT) such that
A10: R = Y and
A11: R is primitive-recursively_closed;
A12: R is composition_closed by A11;
A13: PrimRec c= R by A9,A10,SETFAM_1:3;
then rng F c= R by A8;
hence f*<:F:> in Y by A6,A7,A10,A12,A13;
end;
hence f*<:F:> in PrimRec by A2,SETFAM_1:def 1;
end;
hereby
let g, f1, f2 be Element of HFuncs NAT, i being Nat such
that
A14: g is_primitive-recursively_expressed_by f1,f2,i and
A15: f1 in PrimRec and
A16: f2 in PrimRec;
now
let Y be set;
assume
A17: Y in S;
then consider R being Subset of HFuncs(NAT) such that
A18: R = Y and
A19: R is primitive-recursively_closed;
A20: f2 in R by A16,A17,A18,SETFAM_1:def 1;
A21: R is primitive-recursion_closed by A19;
f1 in R by A15,A17,A18,SETFAM_1:def 1;
hence g in Y by A14,A18,A21,A20;
end;
hence g in PrimRec by A2,SETFAM_1:def 1;
end;
end;
end;
end;
registration
cluster -> homogeneous for Element of PrimRec;
coherence;
end;
definition
let x be set;
attr x is primitive-recursive means
:Def16:
x in PrimRec;
end;
registration
cluster primitive-recursive -> Relation-like Function-like for set;
coherence;
end;
registration
cluster primitive-recursive -> homogeneous to-naturals NAT*-defined for
Relation;
coherence;
end;
registration
cluster -> primitive-recursive for Element of PrimRec;
coherence;
end;
registration
cluster primitive-recursive for Function;
existence
proof
set x = the Element of PrimRec;
take x;
thus thesis;
end;
cluster primitive-recursive for Element of HFuncs NAT;
existence
proof
take the Element of PrimRec;
thus thesis;
end;
end;
definition
func initial-funcs -> Subset of HFuncs NAT equals
{ 0 const 0, 1 succ 1 } \/
{ n proj i where n,i is Element of NAT: 1 <= i & i <= n };
coherence
proof
set Q1 = {0 const 0, 1 succ 1}, Q2 = {n proj i where n,i is Element of NAT
: 1 <= i & i <= n};
A1: Q2 c= HFuncs NAT
proof
let x be object;
assume x in Q2;
then ex n, i being Element of NAT st x = n proj i & 1 <= i & i <= n;
hence thesis by Th34;
end;
Q1 c= HFuncs NAT
proof
let x be object;
assume x in Q1;
then x = 0 const 0 or x = 1 succ 1 by TARSKI:def 2;
hence thesis by Th30,Th32;
end;
hence thesis by A1,XBOOLE_1:8;
end;
let Q be Subset of HFuncs NAT;
func PR-closure Q -> Subset of HFuncs NAT equals
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};
coherence
proof
set Q1 = {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};
Q1 c= HFuncs NAT
proof
let x be object;
assume x in Q1;
then
ex g being Element of HFuncs NAT st x = g & 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;
hence thesis;
end;
hence thesis by XBOOLE_1:8;
end;
func composition-closure Q -> Subset of HFuncs NAT equals
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
proof
set Q1 = {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};
Q1 c= HFuncs NAT
proof
let x be object;
assume x in Q1;
then ex f being Element of HFuncs NAT , F being with_the_same_arity
Element of (HFuncs NAT)* st x = f*<:F:> & f in Q & arity f = len F & rng F
c= Q;
hence thesis by Th41;
end;
hence thesis by XBOOLE_1:8;
end;
end;
definition
func PrimRec-Approximation -> sequence of bool HFuncs NAT means
:Def20:
it.0 = initial-funcs &
for m being Nat holds
it.(m+1) = (PR-closure (it.m)) \/ (composition-closure (it.m));
existence
proof
deffunc f(set,Subset of HFuncs(NAT)) = (PR-closure $2) \/ (
composition-closure $2);
consider A being sequence of bool HFuncs NAT such that
A1: A.0 = initial-funcs and
A2: for m being Nat holds A.(m+1) = f(m,A.m) from NAT_1:sch 12;
take A;
thus A.0 = initial-funcs by A1;
let m being Nat;
thus thesis by A2;
end;
uniqueness
proof
deffunc f(set,Subset of HFuncs(NAT)) = (PR-closure $2) \/ (
composition-closure $2);
let it1, it2 be sequence of bool HFuncs NAT such that
A3: it1.0 = initial-funcs and
A4: for m being Nat holds it1.(m+1) = (PR-closure (it1.m)) \/ (
composition-closure (it1.m)) and
A5: it2.0 = initial-funcs and
A6: for m being Nat holds it2.(m+1) = (PR-closure (it2.m)) \/ (
composition-closure (it2.m));
A7: for m being Nat holds it1.(m+1) = f(m,it1.m) by A4;
A8: for m being Nat holds it2.(m+1) = f(m,it2.m) by A6;
A9: it2.0 = initial-funcs by A5;
A10: it1.0 = initial-funcs by A3;
thus it1 = it2 from NAT_1:sch 16(A10,A7, A9,A8);
end;
end;
theorem Th74:
m <= n implies PrimRec-Approximation.m c= PrimRec-Approximation. n
proof
set prd = PrimRec-Approximation;
defpred p[Nat] means m <= $1 implies prd.m c= prd.$1;
A1: for n be Nat st p[n] holds p[n+1]
proof
let n be Nat such that
A2: p[n] and
A3: m <= n+1;
prd.(n+1) = (PR-closure (prd.n)) \/ (composition-closure (prd.n)) by Def20;
then
A4: PR-closure (prd.n) c= prd.(n+1) by XBOOLE_1:7;
prd.n c= PR-closure (prd.n) by XBOOLE_1:7;
then
A5: prd.n c= prd.(n+1) by A4;
per cases by A3,XXREAL_0:1;
suppose
m < n+1;
hence thesis by A2,A5,NAT_1:13;
end;
suppose
m = n+1;
hence thesis;
end;
end;
A6: p[0];
for n being Nat holds p[n] from NAT_1:sch 2(A6,A1);
hence thesis;
end;
theorem Th75:
Union PrimRec-Approximation is primitive-recursively_closed
proof
set PROJ = {n proj i where n,i is Element of NAT: 1 <= i & i <= n};
set prd = PrimRec-Approximation;
set UP = Union prd;
A1: dom prd = NAT by FUNCT_2:def 1;
A2: prd.0 = {0 const 0, 1 succ 1} \/ PROJ by Def20;
0 const 0 in {0 const 0, 1 succ 1} by TARSKI:def 2;
then 0 const 0 in prd.0 by A2,XBOOLE_0:def 3;
hence 0 const 0 in UP by A1,CARD_5:2;
1 succ 1 in {0 const 0, 1 succ 1} by TARSKI:def 2;
then 1 succ 1 in prd.0 by A2,XBOOLE_0:def 3;
hence 1 succ 1 in UP by A1,CARD_5:2;
hereby
let n,i;
assume that
A3: 1 <= i and
A4: i <= n;
n in NAT & i in NAT by ORDINAL1:def 12;
then n proj i in PROJ by A3,A4;
then n proj i in prd.0 by A2,XBOOLE_0:def 3;
hence n proj i in UP by A1,CARD_5:2;
end;
hereby
deffunc mcocl(Element of NAT) = {f*<:F:> where f is Element of HFuncs NAT,
F is with_the_same_arity Element of (HFuncs NAT)*: f in prd.$1 & arity f = len
F & rng F c= prd.$1};
let f be Element of HFuncs NAT, F be with_the_same_arity FinSequence of
HFuncs NAT such that
A5: f in UP and
A6: arity f = len F and
A7: rng F c= UP;
consider kf being object such that
A8: kf in dom prd and
A9: f in prd.kf by A5,CARD_5:2;
reconsider kf as Element of NAT by A8;
per cases;
suppose
arity f = 0;
then F = {} by A6;
then
A10: rng F c= prd.kf;
F is with_the_same_arity Element of (HFuncs NAT)* by FINSEQ_1:def 11;
then f*<:F:> in mcocl(kf) by A6,A9,A10;
then f*<:F:> in prd.kf \/ mcocl(kf) by XBOOLE_0:def 3;
then f*<:F:> in PR-closure (prd.kf) \/ composition-closure(prd.kf) by
XBOOLE_0:def 3;
then f*<:F:> in prd.(kf+1) by Def20;
hence f*<:F:> in UP by A1,CARD_5:2;
end;
suppose
A11: arity f <> 0;
defpred B[object,object] means
ex k being Element of NAT st F.$1 in prd.k & $2
= k;
A12: for x being object st x in Seg len F ex y being Element of NAT st B[x,y]
proof
let x be object;
assume x in Seg len F;
then x in dom F by FINSEQ_1:def 3;
then F.x in rng F by FUNCT_1:def 3;
then consider k being object such that
A13: k in dom prd and
A14: F.x in prd.k by A7,CARD_5:2;
reconsider k as Element of NAT by A13;
take k;
take k1 = k;
thus F.x in prd.k1 by A14;
thus thesis;
end;
consider fKF being Function of Seg len F, NAT such that
A15: for x being object st x in Seg len F holds B[x,fKF.x] from
MONOID_1:sch 1(A12);
set KF = rng fKF;
reconsider KF as non empty finite Subset of NAT by A6,A11,RELAT_1:def 19;
set K = max KF;
set k = max(kf, K);
reconsider k as Element of NAT by ORDINAL1:def 12;
A16: dom fKF = Seg len F by FUNCT_2:def 1;
A17: rng F c= prd.k
proof
let x be object;
A18: K <= k by XXREAL_0:25;
assume x in rng F;
then consider d being object such that
A19: d in dom F and
A20: x = F.d by FUNCT_1:def 3;
A21: d in Seg len F by A19,FINSEQ_1:def 3;
then consider m being Element of NAT such that
A22: F.d in prd.m and
A23: fKF.d = m by A15;
m in KF by A16,A21,A23,FUNCT_1:3;
then m <= K by XXREAL_2:def 8;
then prd.m c= prd.k by A18,Th74,XXREAL_0:2;
hence thesis by A20,A22;
end;
A24: F is with_the_same_arity Element of (HFuncs NAT)* by FINSEQ_1:def 11;
prd.kf c= prd.k by Th74,XXREAL_0:25;
then f*<:F:> in mcocl(k) by A6,A9,A17,A24;
then f*<:F:> in prd.k \/ mcocl(k) by XBOOLE_0:def 3;
then f*<:F:> in PR-closure (prd.k) \/ composition-closure(prd.k)
by XBOOLE_0:def 3;
then f*<:F:> in prd.(k+1) by Def20;
hence f*<:F:> in UP by A1,CARD_5:2;
end;
end;
deffunc mprcl(Element of NAT) = {g where g is Element of HFuncs NAT: ex f1,
f2 being Element of HFuncs NAT, i being Element of NAT st f1 in prd.$1 & f2 in
prd.$1 & g is_primitive-recursively_expressed_by f1,f2,i};
let g, f1, f2 be Element of HFuncs NAT, i be Nat such that
A25: g is_primitive-recursively_expressed_by f1,f2,i and
A26: f1 in UP and
A27: f2 in UP;
B1: i in NAT by ORDINAL1:def 12;
consider k2 being object such that
A28: k2 in dom prd and
A29: f2 in prd.k2 by A27,CARD_5:2;
reconsider k2 as Element of NAT by A28;
consider k1 being object such that
A30: k1 in dom prd and
A31: f1 in prd.k1 by A26,CARD_5:2;
reconsider k1 as Element of NAT by A30;
per cases;
suppose
k1 <= k2;
then prd.k1 c= prd.k2 by Th74;
then g in mprcl(k2) by A25,A31,A29,B1;
then g in prd.k2 \/ mprcl(k2) by XBOOLE_0:def 3;
then g in PR-closure (prd.k2) \/ composition-closure(prd.k2)
by XBOOLE_0:def 3;
then g in prd.(k2+1) by Def20;
hence thesis by A1,CARD_5:2;
end;
suppose
k2 <= k1;
then prd.k2 c= prd.k1 by Th74;
then g in mprcl(k1) by A25,A31,A29,B1;
then g in prd.k1 \/ mprcl(k1) by XBOOLE_0:def 3;
then g in PR-closure (prd.k1) \/ composition-closure(prd.k1)
by XBOOLE_0:def 3;
then g in prd.(k1+1) by Def20;
hence thesis by A1,CARD_5:2;
end;
end;
theorem Th76:
PrimRec = Union PrimRec-Approximation
proof
set prd = PrimRec-Approximation;
defpred p[Nat] means prd.$1 c= PrimRec;
A1: now
let m being Nat such that
A2: p[m];
thus p[m+1]
proof
set mcocl = {f*<:F:> where f is Element of HFuncs NAT, F is
with_the_same_arity Element of (HFuncs NAT)*: f in prd.m & arity f = len F &
rng F c= prd.m};
set mprcl = {g where g is Element of HFuncs NAT: ex f1,f2 being Element
of HFuncs NAT, i being Element of NAT st f1 in prd.m & f2 in prd.m & g
is_primitive-recursively_expressed_by f1,f2,i};
let x be object;
A3: prd.(m+1) = (PR-closure (prd.m)) \/ (composition-closure (prd.m))
by Def20;
assume
A4: x in prd.(m+1);
per cases by A4,A3,XBOOLE_0:def 3;
suppose
A5: x in PR-closure (prd.m);
thus thesis
proof
per cases by A5,XBOOLE_0:def 3;
suppose
x in prd.m;
hence thesis by A2;
end;
suppose
A6: x in mprcl;
A7: PrimRec is primitive-recursion_closed by Def14;
ex g being Element of HFuncs NAT st x = g & ex f1,f2 being
Element of HFuncs NAT, i being Element of NAT st f1 in prd.m & f2 in prd. m & g
is_primitive-recursively_expressed_by f1,f2,i by A6;
hence thesis by A2,A7;
end;
end;
end;
suppose
A8: x in composition-closure (prd.m);
thus thesis
proof
per cases by A8,XBOOLE_0:def 3;
suppose
x in prd.m;
hence thesis by A2;
end;
suppose
A9: x in mcocl;
A10: PrimRec is composition_closed by Def14;
consider f being Element of HFuncs NAT, F being
with_the_same_arity Element of (HFuncs NAT)* such that
A11: x = f*<:F:> and
A12: f in prd.m and
A13: arity f = len F and
A14: rng F c= prd.m by A9;
rng F c= PrimRec by A2,A14,XBOOLE_1:1;
hence thesis by A2,A11,A12,A13,A10;
end;
end;
end;
end;
end;
A15: p[0]
proof
let x be object;
assume
A16: x in prd.0;
prd.0 = {0 const 0, 1 succ 1} \/ {n proj i where n,i is Element of NAT
: 1 <= i & i <= n} by Def20;
then
A17: x in {0 const 0, 1 succ 1} or x in {n proj i where n,i is Element of
NAT: 1 <= i & i <= n} by A16,XBOOLE_0:def 3;
per cases by A17,TARSKI:def 2;
suppose
x = 0 const 0;
hence thesis by Def14;
end;
suppose
x = 1 succ 1;
hence thesis by Def14;
end;
suppose
x in {n proj i where n,i is Element of NAT: 1 <= i & i <= n};
then ex n, i being Element of NAT st x = n proj i & 1 <= i & i <= n;
hence thesis by Def14;
end;
end;
A18: for k being Nat holds p[k] from NAT_1:sch 2(A15, A1);
A19: Union prd c= PrimRec
proof
let x be object;
assume that
A20: x in Union prd and
A21: not x in PrimRec;
consider X being set such that
A22: x in X and
A23: X in rng prd by A20,TARSKI:def 4;
consider m being object such that
A24: m in dom prd and
A25: prd.m = X by A23,FUNCT_1:def 3;
reconsider m as Element of NAT by A24;
prd.m c= PrimRec by A18;
hence contradiction by A21,A22,A25;
end;
PrimRec c= Union prd by Th73,Th75;
hence thesis by A19,XBOOLE_0:def 10;
end;
theorem Th77:
for f being Element of HFuncs(NAT) st
f in PrimRec-Approximation.m holds f is quasi_total
proof
defpred p[Nat] means for f being Element of HFuncs(NAT) st f in
PrimRec-Approximation.$1 holds f is quasi_total;
set prd = PrimRec-Approximation;
A1: for m be Nat st p[m] holds p[m+1]
proof
let m be Nat;
assume
A2: p[m];
let f be Element of HFuncs(NAT);
assume f in prd.(m+1);
then
A3: f in (PR-closure (prd.m)) \/ (composition-closure (prd.m)) by Def20;
per cases by A3,XBOOLE_0:def 3;
suppose
A4: f in (PR-closure (prd.m));
thus f is quasi_total
proof
per cases by A4,XBOOLE_0:def 3;
suppose
f in prd.m;
hence thesis by A2;
end;
suppose
f in {g where g is Element of HFuncs NAT: ex f1,f2 being
Element of HFuncs NAT, i being Element of NAT st f1 in prd.m & f2 in prd.m & g
is_primitive-recursively_expressed_by f1,f2,i};
then consider g being Element of HFuncs NAT such that
A5: f = g and
A6: ex f1,f2 being Element of HFuncs NAT, i being Element of
NAT st f1 in prd.m & f2 in prd.m & g is_primitive-recursively_expressed_by f1,
f2,i;
consider f1, f2 being Element of HFuncs NAT, i being Element of NAT
such that
A7: f1 in prd.m and
A8: f2 in prd.m and
A9: g is_primitive-recursively_expressed_by f1,f2,i by A6;
A10: f2 is quasi_total by A2,A8;
f1 is quasi_total by A2,A7;
hence thesis by A5,A9,A10,Th67;
end;
end;
end;
suppose
A11: f in (composition-closure (prd.m));
thus f is quasi_total
proof
per cases by A11,XBOOLE_0:def 3;
suppose
f in prd.m;
hence thesis by A2;
end;
suppose
f in {h*<:F:> where h is Element of HFuncs NAT, F is
with_the_same_arity Element of (HFuncs NAT)*: h in prd.m & arity h = len F &
rng F c= prd.m};
then consider
h being Element of HFuncs NAT, F being with_the_same_arity
Element of (HFuncs NAT)* such that
A12: f = h*<:F:> and
A13: h in prd.m and
A14: arity h = len F and
A15: rng F c= prd.m;
A16: for h being Element of HFuncs NAT st h in rng F holds h is
quasi_total by A2,A15;
h is quasi_total by A2,A13;
hence thesis by A12,A14,A16,Th45;
end;
end;
end;
end;
A17: p[0]
proof
let f be Element of HFuncs(NAT);
assume f in prd.0;
then f in initial-funcs by Def20;
then
A18: f in {0 const 0, 1 succ 1} or f in {n proj i where n,i is Element of
NAT: 1 <= i & i <= n} by XBOOLE_0:def 3;
per cases by A18,TARSKI:def 2;
suppose
f = 0 const 0;
hence thesis by Th28;
end;
suppose
f = 1 succ 1;
hence thesis by Th28;
end;
suppose
f in {n proj i where n,i is Element of NAT: 1 <= i & i <= n};
then ex n, i being Element of NAT st f = n proj i & 1 <= i & i <= n;
hence thesis by Th28;
end;
end;
for m being Nat holds p[m] from NAT_1:sch 2(A17, A1);
hence thesis;
end;
registration
cluster -> quasi_total homogeneous for Element of PrimRec;
coherence
proof
set prd = PrimRec-Approximation;
let f be Element of PrimRec;
consider X being set such that
A1: f in X and
A2: X in rng prd by Th76,TARSKI:def 4;
ex m being object st m in dom prd & prd.m = X by A2,FUNCT_1:def 3;
hence thesis by A1,Th77;
end;
end;
registration
cluster primitive-recursive -> quasi_total for Element of HFuncs NAT;
coherence;
end;
registration
cluster primitive-recursive -> len-total for NAT*-defined Function;
coherence
proof
let x be NAT*-defined Function;
assume x in PrimRec;
then x is Element of PrimRec;
hence thesis;
end;
cluster non empty for Element of PrimRec;
existence
proof
0 const 0 in PrimRec by Th68;
hence thesis;
end;
end;
begin :: Examples
definition
let n be set;
let f be homogeneous Relation;
attr f is n-ary means
:Def21:
arity f = n;
end;
registration
let n be non zero Nat;
cluster n-ary -> non empty for homogeneous Function;
coherence
proof
let f be homogeneous Function;
assume arity f = n;
then ex x being FinSequence st x in dom f by MARGREL1:def 25;
hence thesis;
end;
end;
registration
let n,m be Nat;
cluster n const m -> primitive-recursive;
coherence by Th68;
end;
registration
let n be non zero Nat;
cluster n succ n -> primitive-recursive;
coherence
proof
0+1 <= n by NAT_1:13;
hence n succ n in PrimRec by Th69;
end;
cluster n proj n -> primitive-recursive;
coherence
proof
0+1 <= n by NAT_1:13;
hence n proj n in PrimRec by Def14;
end;
cluster n proj 1 -> primitive-recursive;
coherence
proof
1 <= n by NAT_1:14;
then n proj 1 in PrimRec by Def14;
hence thesis;
end;
end;
registration
let n,i;
cluster n const i -> n-ary;
coherence;
end;
registration
let n be non zero Nat;
let i be Nat;
cluster n succ i -> n-ary;
coherence;
cluster n proj i -> n-ary;
coherence;
end;
registration
let n be Nat;
cluster n-ary primitive-recursive non empty for homogeneous Function;
existence
proof
take f = n const n;
thus f is n-ary;
thus f in PrimRec by Def16;
thus thesis;
end;
end;
registration
let n be Nat;
cluster non empty n-ary len-total to-naturals for homogeneous NAT*-defined
Function;
existence
proof
n const 0 is n-ary;
hence thesis;
end;
end;
registration
let f be 0-ary non empty primitive-recursive Function;
let g be 2-ary primitive-recursive Function;
cluster primrec(f,g,1) -> primitive-recursive 1-ary;
coherence
proof
A1: g in PrimRec by Def16;
A2: arity f = 0 by Def21;
f is Element of PrimRec by Def16;
then dom f = 0-tuples_on NAT by A2,Th21
.= {<*>NAT} by FINSEQ_2:94;
then
A3: {} in dom f by TARSKI:def 1;
A4: f in PrimRec by Def16;
A5: 1 <= 0+1;
arity g = 0+2 by Def21;
hence primrec(f,g,1) in PrimRec by A5,A2,A4,A1,Th72;
reconsider ii= <*0*> as Element of 1-tuples_on NAT by FINSEQ_2:131;
dom <*0*> = {1} by FINSEQ_1:2,38;
then
A6: 1 in dom <*0*> by TARSKI:def 1;
Del(<*0*>,1) = {} by WSIERP_1:19;
then ii+*(1,0) in dom primrec(f,g,1) by A5,A2,A3,A6,Lm6;
then
A7: <*0*> in dom primrec(f,g,1) by FUNCT_7:95;
len <*0*> = 1 by FINSEQ_1:39;
hence arity primrec(f,g,1) = 1 by A7,MARGREL1:def 25;
end;
end;
registration
let f be 1-ary primitive-recursive Function;
let g be 3-ary primitive-recursive Function;
cluster primrec(f,g,1) -> primitive-recursive 2-ary;
coherence
proof
A1: g in PrimRec by Def16;
A2: 1 <= 1+1;
A3: arity g = 1+2 by Def21;
A4: arity f = 1 by Def21;
f in PrimRec by Def16;
hence primrec(f,g,1) in PrimRec by A2,A4,A3,A1,Th72;
thus arity primrec(f,g,1) = 2 by A2,A4,A3,Th56;
end;
cluster primrec(f,g,2) -> primitive-recursive 2-ary;
coherence
proof
A5: g in PrimRec by Def16;
A6: 2 <= 1+1;
A7: arity g = 1+2 by Def21;
A8: arity f = 1 by Def21;
f in PrimRec by Def16;
hence primrec(f,g,2) in PrimRec by A6,A8,A7,A5,Th72;
thus arity primrec(f,g,2) = 2 by A6,A8,A7,Th56;
end;
end;
theorem Th78:
for f1 be 1-ary len-total to-naturals homogeneous NAT*-defined Function,
f2 be non empty to-naturals homogeneous NAT*-defined Function holds
primrec(f1,f2,2).<*i,0*> = f1.<*i*>
proof
let f1 be 1-ary len-total to-naturals homogeneous NAT*-defined Function,
f2 be non empty to-naturals homogeneous NAT*-defined Function;
reconsider i1=i as Element of NAT by ORDINAL1:def 12;
arity f1 = 1 by Def21;
then reconsider p = <*i1,0*> as Element of (arity f1 +1)-tuples_on NAT
by FINSEQ_2:101;
len p = 2 by FINSEQ_1:44;
then
A1: 2 in dom p by FINSEQ_3:25;
p+*(2,0) = p by Th1;
hence primrec(f1,f2,2).<*i,0*> = f1.Del(p,2) by A1,Th59
.= f1.<*i*> by WSIERP_1:19;
end;
theorem Th79:
f1 is len-total & arity f1 = 0 implies primrec(f1,f2,1).<*0*> = f1.{}
proof
assume that
A1: f1 is len-total and
A2: arity f1 = 0;
reconsider p = <*0*> as Element of (arity f1 +1)-tuples_on NAT
by A2,FINSEQ_2:131;
len p = 1 by FINSEQ_1:39;
then
A3: 1 in dom p by FINSEQ_3:25;
p+*(1,0) = p by FUNCT_7:95;
hence primrec(f1,f2,1).<*0*> = f1.Del(p,1) by A1,A3,Th59
.= f1.{} by WSIERP_1:19;
end;
theorem Th80:
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*>*>
proof
let f1 be 1-ary len-total to-naturals homogeneous NAT*-defined Function,
f2 be 3-ary len-total to-naturals homogeneous NAT*-defined Function;
reconsider i1 = i, j1 = j as Element of NAT by ORDINAL1:def 12;
A1: arity f1 = 1 by Def21;
then reconsider p = <*i1,j1*> as Element of (arity f1 +1)-tuples_on NAT
by FINSEQ_2:101;
A2: p+*(2,j+1) = <*i,j+1*> by Th1;
A3: p+*(2,j) = <*i,j*> by Th1;
arity f1 +2 = arity f2 by A1,Def21;
hence
primrec(f1,f2,2).<*i,j+1*> = f2.((p+*(2,j))^<*primrec(f1,f2,2).(p+*(2,j
))*>) by A1,A2,Th62
.= f2.<*i,j,primrec(f1,f2,2).<*i,j*>*> by A3,FINSEQ_1:43;
end;
theorem Th81:
f1 is len-total & f2 is len-total & arity f1 = 0 & arity f2 = 2
implies primrec(f1,f2,1).<*i+1*> = f2.<*i,primrec(f1,f2,1).<*i*>*>
proof
assume that
A1: f1 is len-total and
A2: f2 is len-total and
A3: arity f1 = 0 and
A4: arity f2 = 2;
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
reconsider p = <*i1*> as Element of (arity f1 +1)-tuples_on NAT
by A3,FINSEQ_2:131;
A5: p+*(1,i+1) = <*i+1*> by FUNCT_7:95;
A6: p+*(1,i) = <*i*> by FUNCT_7:95;
arity f1 +2 = arity f2 by A3,A4;
hence
primrec(f1,f2,1).<*i+1*> = f2.((p+*(1,i))^<*primrec(f1,f2,1).(p+*(1,i))
*>) by A1,A2,A3,A5,Th62
.= f2.<*i,primrec(f1,f2,1).<*i*>*> by A6,FINSEQ_1:def 9;
end;
Lm8: now
reconsider z3 = <*0,0,0*> as FinSequence of NAT;
let g be quasi_total homogeneous non empty PartFunc of NAT*, NAT;
set G = g*<:<*3 proj 1, 3 proj 3*>:>;
A1: rng G c= NAT by RELAT_1:def 19;
assume
A2: arity g = 2;
then
A3: dom g = 2-tuples_on NAT by Th21;
thus
A4: dom <:<*3 proj 1,3 proj 3*>:>=dom (3 proj 1)/\dom (3 proj 3) by
FINSEQ_3:142;
hence
A5: dom <:<*3 proj 1, 3 proj 3*>:> = (3-tuples_on NAT) /\ dom (3 proj 3
) by Th35
.= (3-tuples_on NAT) /\ (3-tuples_on NAT) by Th35
.= (3-tuples_on NAT);
now
set f = <*3 proj 1, 3 proj 3*>;
let x be object;
set F = <:f:>;
A6: product rngs f = product <*rng (3 proj 1),rng (3 proj 3)*> by FINSEQ_3:133
.= product <*NAT, rng (3 proj 3)*> by Th35
.=product <*NAT, NAT*> by Th35
.= 2-tuples_on NAT by FINSEQ_3:128;
hereby
A7: rng F c= product rngs f by FUNCT_6:29;
assume x in rng F;
hence x in dom g by A3,A6,A7;
end;
assume x in dom g;
then x is Element of 2-tuples_on NAT by A2,Th21;
then consider d1, d2 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;
F.x9 = <*(3 proj 1).x9, (3 proj 3).x9*> by A4,A5,FINSEQ_3:142
.= <*x9.1, (3 proj 3).x9*> by Th37
.= <*x9.1, x9.3*> by Th37
.= x by A8;
hence x in rng F by A5,FUNCT_1:def 3;
end;
then rng <:<*3 proj 1, 3 proj 3*>:> = dom g by TARSKI:2;
hence
A9: dom (g*<:<*3 proj 1, 3 proj 3*>:>) = 3-tuples_on NAT by A5,RELAT_1:27;
then reconsider G as PartFunc of NAT*, NAT by A1,FINSEQ_2:142,RELSET_1:4;
reconsider G as homogeneous PartFunc of NAT*, NAT by A9,MARGREL1:def 21;
take G;
thus G = g*<:<*3 proj 1, 3 proj 3*>:>;
G is Element of PFuncs(NAT* , NAT) by PARTFUN1:45;
then G in HFuncs NAT;
hence G is Element of HFuncs NAT;
len z3 = 3 by FINSEQ_1:45;
then
A10: z3 is Element of 3-tuples_on NAT by FINSEQ_2:92;
for x 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;
hence G is quasi_total non empty by A9,Th21;
end;
definition
let g be Function;
func (1,2)->(1,?,2) g -> Function equals
g * <:<*3 proj 1, 3 proj 3*>:>;
coherence;
end;
registration
let g be to-naturals NAT*-defined Function;
cluster (1,2)->(1,?,2) g -> to-naturals NAT*-defined;
coherence
proof
set G = (1,2)->(1,?,2) g;
A1: (3-tuples_on NAT) c= NAT* by FINSEQ_2:142;
dom <:<*3 proj 1, 3 proj 3*>:> = dom (3 proj 1) /\ dom (3 proj 3)
by FINSEQ_3:142;
then
A2: dom <:<*3 proj 1, 3 proj 3*>:> = (3-tuples_on NAT) /\ dom (3 proj 3)
by Th35
.= (3-tuples_on NAT)/\(3-tuples_on NAT) by Th35
.= (3-tuples_on NAT);
dom G c= dom <:<*3 proj 1, 3 proj 3*>:> by RELAT_1:25;
then dom G c= NAT* by A2,A1;
hence thesis;
end;
end;
registration
let g be homogeneous Function;
cluster (1,2)->(1,?,2) g -> homogeneous;
coherence
proof
set G = (1,2)->(1,?,2) g;
dom <:<*3 proj 1, 3 proj 3*>:> = dom (3 proj 1) /\ dom (3 proj 3)
by FINSEQ_3:142;
then dom <:<*3 proj 1, 3 proj 3*>:> = (3-tuples_on NAT) /\ dom (3 proj 3)
by Th35
.= (3-tuples_on NAT)/\(3-tuples_on NAT) by Th35
.=(3-tuples_on NAT);
then dom G c= 3-tuples_on NAT by RELAT_1:25;
hence dom G is with_common_domain;
end;
end;
registration
let g be 2-ary len-total to-naturals homogeneous NAT*-defined Function;
cluster (1,2)->(1,?,2) g -> non empty 3-ary len-total;
coherence
proof
A1: g is quasi_total homogeneous non empty PartFunc of NAT*, NAT by Th16;
arity g = 2 by Def21;
then consider G being homogeneous PartFunc of NAT*, NAT such that
A2: G = g*<:<*3 proj 1, 3 proj 3*>:> and
G is Element of HFuncs NAT and
A3: arity G = 3 and
A4: G is quasi_total non empty by A1,Lm8;
reconsider G9 = G as quasi_total non empty homogeneous PartFunc of NAT*,
NAT by A4;
G9 is non empty 3-ary len-total to-naturals homogeneous NAT*
-defined Function by A3,Def21;
hence thesis by A2;
end;
end;
theorem Th82:
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*>
proof
let f be 2-ary len-total to-naturals homogeneous NAT*-defined Function;
reconsider ff=f as quasi_total homogeneous non empty PartFunc of NAT*, NAT
by Th16;
reconsider i1 = i, j1 = j,k1 = k as Element of NAT by ORDINAL1:def 12;
reconsider ijk = <*i1,j1,k1*> as Element of 3-tuples_on NAT
by FINSEQ_2:104;
A1: arity ff = 2 by Def21;
then
A2: dom <:<*3 proj 1, 3 proj 3*>:> = dom (3 proj 1) /\ dom (3 proj 3) by Lm8;
A3: dom <:<*3 proj 1, 3 proj 3*>:> = (3-tuples_on NAT) by A1,Lm8;
dom (ff*<:<*3 proj 1, 3 proj 3*>:>) = 3-tuples_on NAT by A1,Lm8;
hence ((1,2)->(1,?,2) f).<*i,j,k*> = f.(<:<*3 proj 1, 3 proj 3*>:>.ijk) by
FUNCT_1:12
.= f.<*(3 proj 1).ijk, (3 proj 3).ijk*> by A2,A3,FINSEQ_3:142
.= f.<*ijk.1, (3 proj 3).ijk*> by Th37
.= f.<*ijk.1, ijk.3*> by Th37
.= f.<*i,k*>;
end;
theorem Th83:
for g being 2-ary primitive-recursive Function holds
(1,2)->(1,?,2) g in PrimRec
proof
A1: 3 proj 3 in PrimRec by Def14;
A2: 2-tuples_on PrimRec c= (PrimRec)* by FINSEQ_2:142;
3 proj 1 in PrimRec by Def14;
then <*3 proj 1, 3 proj 3*> in 2-tuples_on PrimRec by A1,FINSEQ_2:101;
then reconsider F = <*3 proj 1, 3 proj 3*> as Element of (PrimRec)* by A2;
F is with_the_same_arity
proof
let f,g be Function;
assume that
A3: f in rng F and
A4: g in rng F;
A5: rng F = {3 proj 1, 3 proj 3} by FINSEQ_2:127;
hence f is empty implies g is empty or dom g = {{}} by A3,TARSKI:def 2;
assume that
f is non empty and
g is non empty;
take 3, NAT;
f = 3 proj 1 or f = 3 proj 3 by A3,A5,TARSKI:def 2;
hence dom f c= 3-tuples_on NAT by Th35;
g = 3 proj 1 or g = 3 proj 3 by A4,A5,TARSKI:def 2;
hence thesis by Th35;
end;
then reconsider F as with_the_same_arity Element of (PrimRec)*;
let g be 2-ary primitive-recursive Function;
arity g = 2 by Def21;
then
A6: arity g = len F by FINSEQ_1:44;
g is Element of PrimRec by Def16;
hence thesis by A6,Th71;
end;
registration
let f be 2-ary primitive-recursive homogeneous Function;
cluster (1,2)->(1,?,2) f -> primitive-recursive 3-ary;
coherence by Th83;
end;
definition
func [+] -> 2-ary primitive-recursive Function equals
primrec(1 proj 1, 3 succ 3, 2);
coherence;
end;
theorem Th84:
[+].<*i,j*> = i+j
proof
reconsider i,j as Element of NAT by ORDINAL1:def 12;
reconsider q = <*i*> as Element of 1-tuples_on NAT by FINSEQ_2:131;
defpred p[Nat] means [+].<*i,$1*> = i+$1;
A1: now
let j be Nat;
reconsider jj=j as Element of NAT by ORDINAL1:def 12;
reconsider r = <*i,jj,i+jj*> as Element of 3-tuples_on NAT by FINSEQ_2:104;
assume p[j];
then [+].<*i,jj+1*> = (3 succ 3).r by Th80
.= (r.3)+1 by Def7
.= i+(j+1);
hence p[j+1];
end;
[+].<*i,0*> = (1 proj 1).q by Th78
.= q.1 by Th37
.= i+0;
then
A2: p[0];
for j being Nat holds p[j] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
definition
func [*] -> 2-ary primitive-recursive Function equals
primrec(1 const 0, (1,2)->(1,?,2) [+], 2);
coherence;
end;
theorem Th85:
[*].<*i,j*> = i*j
proof
reconsider i1=i as Element of NAT by ORDINAL1:def 12;
defpred p[Nat] means [*].<*i,$1*> = i*$1;
A1: now
let j be Nat;
reconsider jj=j as Element of NAT by ORDINAL1:def 12;
assume p[j];
then [*].<*i1,jj+1*> = ((1,2)->(1,?,2) [+]).<*i,jj,i*jj*> by Th80
.= [+].<*i1,i1*jj*> by Th82
.= (i*1)+i*jj by Th84
.= i*(j+1);
hence p[j+1];
end;
reconsider ii = <*i1*> as Element of 1-tuples_on NAT by FINSEQ_2:98;
[*].<*i,0*> = (1 const 0).ii by Th78
.= i*0;
then
A2: p[0];
for i be Nat holds p[i] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
registration
let g,h be 2-ary primitive-recursive homogeneous Function;
cluster <*g,h*> -> with_the_same_arity;
coherence
proof
reconsider g, h as Element of PrimRec by Def16;
A1: rng <*g,h*> = {g,h} by FINSEQ_2:127;
A2: now
let f1,f2 be homogeneous Function;
assume that
A3: f1 in rng <*g,h*> and
A4: f2 in rng <*g,h*>;
f1 = g or f1 = h by A1,A3,TARSKI:def 2;
then
A5: arity f1 = 2 by Def21;
f2 = g or f2 = h by A1,A4,TARSKI:def 2;
hence arity f1 = arity f2 by A5,Def21;
end;
rng <*g,h*> c= PrimRec by FINSEQ_1:def 4;
hence thesis by A2,Th29,XBOOLE_1:1;
end;
end;
registration
let f,g,h be 2-ary primitive-recursive Function;
cluster f*<:<*g,h*>:> -> primitive-recursive;
coherence
proof
reconsider g9 = g, h9 = h as Element of PrimRec by Def16;
A1: f in PrimRec by Def16;
A2: rng <*g9,h9*> c= PrimRec by FINSEQ_1:def 4;
then rng <*g,h*> c= HFuncs NAT by XBOOLE_1:1;
then reconsider
F = <*g,h*> as with_the_same_arity FinSequence of HFuncs NAT by
FINSEQ_1:def 4;
A3: PrimRec is composition_closed by Def14;
A4: arity f = 2 by Def21;
len F = 2 by FINSEQ_1:44;
hence f*<:<*g,h*>:> in PrimRec by A2,A1,A3,A4;
end;
end;
registration
let f,g,h be 2-ary primitive-recursive Function;
cluster f*<:<*g,h*>:> -> 2-ary;
coherence
proof
set x = the Element of 2-tuples_on NAT;
reconsider f9 = f, fgh = f*<:<*g,h*>:>, g9 = g, h9 = h as Element of
PrimRec by Def16;
A1: f9 = f;
rng <*g9,h9*> c= PrimRec by FINSEQ_1:def 4;
then rng <*g,h*> c= HFuncs NAT by XBOOLE_1:1;
then reconsider
F = <*g,h*> as with_the_same_arity FinSequence of HFuncs NAT by
FINSEQ_1:def 4;
A2: dom <:F:> = dom g /\ dom h by FINSEQ_3:142;
A3: arity g = 2 by Def21;
rng F = {g, h } by FINSEQ_2:127;
then g in rng F by TARSKI:def 2;
then
A4: arity F = 2 by A3,Def4;
arity f = 2 by Def21;
then
A5: dom f9 = 2-tuples_on NAT by Lm1;
arity h = 2 by Def21;
then
A6: dom h9 = 2-tuples_on NAT by Lm1;
A7: dom g9 = 2-tuples_on NAT by A3,Lm1;
then <:F:>.x = <*g9.x,h9.x*> by A6,A2,FINSEQ_3:142;
then <:F:>.x is Element of 2-tuples_on NAT by FINSEQ_2:101;
then fgh is non empty by A5,A7,A6,A2,FUNCT_1:11,RELAT_1:38;
hence arity (f*<:<*g,h*>:>) = 2 by A1,A4,Th43;
end;
end;
registration
let f be 1-ary primitive-recursive Function;
let g be primitive-recursive Function;
cluster f*<:<*g*>:> -> primitive-recursive;
coherence
proof
reconsider g9 = g as Element of PrimRec by Def16;
A1: f in PrimRec by Def16;
A2: rng <*g9*> c= PrimRec by FINSEQ_1:def 4;
then rng <*g*> c= HFuncs NAT by XBOOLE_1:1;
then reconsider
F = <*g9*> as with_the_same_arity FinSequence of HFuncs NAT by
FINSEQ_1:def 4;
A3: PrimRec is composition_closed by Def14;
A4: arity f = 1 by Def21;
len F = 1 by FINSEQ_1:39;
hence f*<:<*g*>:> in PrimRec by A2,A1,A3,A4;
end;
end;
registration
let f be 1-ary primitive-recursive Function;
let g be 2-ary primitive-recursive Function;
cluster f*<:<*g*>:> -> 2-ary;
coherence
proof
set x = the Element of 2-tuples_on NAT;
reconsider f9 = f, fg = f*<:<*g*>:>, g9 = g as Element of PrimRec by Def16;
A1: f9 = f;
rng <*g9*> c= PrimRec by FINSEQ_1:def 4;
then rng <*g*> c= HFuncs NAT by XBOOLE_1:1;
then reconsider
F = <*g9*> as with_the_same_arity FinSequence of HFuncs NAT by
FINSEQ_1:def 4;
A2: dom <:F:> = dom g by FINSEQ_3:141;
arity f = 1 by Def21;
then
A3: dom f9 = 1-tuples_on NAT by Lm1;
A4: arity g = 2 by Def21;
rng F = { g} by FINSEQ_1:39;
then g in rng F by TARSKI:def 1;
then
A5: arity F = 2 by A4,Def4;
A6: dom g9 = 2-tuples_on NAT by A4,Lm1;
then <:F:>.x = <*g9.x*> by FINSEQ_3:141;
then <:F:>.x in 1-tuples_on NAT by FINSEQ_2:98;
then fg is non empty by A6,A2,A3,FUNCT_1:11,RELAT_1:38;
hence arity (f*<:<*g*>:>) = 2 by A1,A5,Th43;
end;
end;
definition
func [!] -> 1-ary primitive-recursive Function equals
primrec(0 const 1, [*]*<:<*(1 succ 1)*<:<*2 proj 1*>:>, 2 proj 2*>:>, 1);
coherence;
end;
scheme
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) -> Nat, g(set,set) -> Nat}: for i, j
being Element of NAT holds (F()*<:<*G()*>:>).<*i,j*> = f(g(i,j))
provided
A1: for i being Element of NAT holds F().<*i*> = f(i) and
A2: for i,j being Element of NAT holds G().<*i,j*> = g(i,j)
proof
let i, j be Element of NAT;
arity G() = 2 by Def21;
then
A3: dom G() = 2-tuples_on NAT by Th22;
B1: g(i,j) in NAT by ORDINAL1:def 12;
dom <:<*G()*>:> = dom G() by FINSEQ_3:141;
hence (F()*<:<*G()*>:>).<*i,j*> = F().(<:<*G()*>:>.<*i,j*>) by A3,
FINSEQ_2:101,FUNCT_1:13
.= F().<*G().<*i,j*>*> by A3,FINSEQ_2:101,FINSEQ_3:141
.= F().<*g(i,j)*> by A2
.= f(g(i,j)) by A1,B1;
end;
scheme
Primrec2{F,G,H() -> 2-ary len-total to-naturals homogeneous NAT*-defined
Function, f,g,h(set,set) -> Nat}: for i, j being Element of NAT
holds (F()*<:<*G(),H()*>:>).<*i,j*> = f(g(i,j),h(i,j))
provided
A1: for i,j being Element of NAT holds F().<*i,j*> = f(i,j) and
A2: for i,j being Element of NAT holds G().<*i,j*> = g(i,j) and
A3: for i,j being Element of NAT holds H().<*i,j*> = h(i,j)
proof
let i, j being Element of NAT;
arity G() = 2 by Def21;
then
A4: dom G() = 2-tuples_on NAT by Th22;
arity H() = 2 by Def21;
then
A5: dom H() = 2-tuples_on NAT by Th22;
B1: g(i,j) in NAT & h(i,j) in NAT by ORDINAL1:def 12;
A6: dom <:<*G(),H()*>:> = dom G() /\ dom H() by FINSEQ_3:142;
hence (F()*<:<*G(),H()*>:>).<*i,j*> = F().(<:<*G(),H()*>:>.<*i,j*>) by A4,A5,
FINSEQ_2:101,FUNCT_1:13
.= F().<*G().<*i,j*>,H().<*i,j*>*> by A6,A4,A5,FINSEQ_2:101,FINSEQ_3:142
.= F().<*g(i,j),H().<*i,j*>*> by A2
.= F().<*g(i,j),h(i,j)*> by A3
.= f(g(i,j),h(i,j)) by A1,B1;
end;
theorem
[!].<*i*> = i!
proof
defpred p[Nat] means [!].<*$1*> = $1!;
deffunc c(Element of NAT,Element of NAT) = $2;
deffunc a(Element of NAT,Element of NAT) = $1*$2;
deffunc g(Element of NAT,Element of NAT) = $1;
deffunc f(Element of NAT) = $1+1;
set g = [*]*<:<*(1 succ 1)*<:<*2 proj 1*>:>, 2 proj 2*>:>;
deffunc b(Element of NAT,Element of NAT) = f(g($1,$2));
A1: for i,j being Element of NAT holds (2 proj 1).<*i,j*> = g(i,j)
proof
let i,j be Element of NAT;
reconsider ij = <*i,j*> as Element of 2-tuples_on NAT by FINSEQ_2:101;
thus (2 proj 1).<*i,j*> = ij.1 by Th37
.= i;
end;
A2: for i being Element of NAT holds (1 succ 1).<*i*> = f(i)
proof
let i be Element of NAT;
reconsider ij = <*i*> as Element of 1-tuples_on NAT by FINSEQ_2:131;
thus (1 succ 1).<*i*> = ij.1+1 by Def7
.= i+1;
end;
for i, j being Element of NAT holds ((1 succ 1)*<:<*2 proj 1*>:>).<*i,j
*> = f(g(i,j)) from Primrec1(A2,A1);
then
A3: for i, j being Element of NAT holds ((1 succ 1)*<:<*2 proj 1*>:>).<*i,j
*> = b (i,j);
A4: for i, j being Element of NAT holds (2 proj 2).<*i,j*> = c(i,j)
proof
let i,j be Element of NAT;
reconsider ij = <*i,j*> as Element of 2-tuples_on NAT by FINSEQ_2:101;
thus (2 proj 2).<*i,j*> = ij.2 by Th37
.= j;
end;
A5: for i, j being Element of NAT holds [*].<*i,j*> = a(i,j) by Th85;
A6: for i, j being Element of NAT holds g.<*i,j*> = a(b(i,j),c(i,j)) from
Primrec2(A5,A3,A4);
A7: arity (0 const 1) = 0;
A8: arity g = 2 by Def21;
A9: now
let i be Nat;
reconsider i1=i as Element of NAT by ORDINAL1:def 12;
reconsider ie = i! as Element of NAT;
assume p[i];
then [!].<*i1+1*> = g.<*i1,ie*> by A8,A7,Th81
.= (i1+1)*ie by A6
.= (i+1)! by NEWTON:15;
hence p[i+1];
end;
0-tuples_on NAT = {{}} by Th5;
then
A10: {} in 0-tuples_on NAT by TARSKI:def 1;
[!].<*0*> = (0 const 1).{} by A7,Th79
.= 0! by A10,FUNCOP_1:7,NEWTON:12;
then
A11: p[0];
for i being Nat holds p[i] from NAT_1:sch 2(A11, A9);
hence thesis;
end;
definition
func [^] -> 2-ary primitive-recursive Function equals
primrec(1 const 1, (1,2)->(1,?,2) [*], 2);
coherence;
end;
theorem
[^].<*i,j*> = i |^ j
proof
defpred p[Nat] means [^].<*i,$1*> = i |^ $1;
reconsider i as Element of NAT by ORDINAL1:def 12;
A1: now
let j be Nat;
reconsider jj=j as Element of NAT by ORDINAL1:def 12;
reconsider ij = i|^jj as Element of NAT;
assume p[j];
then [^].<*i,jj+1*> = ((1,2)->(1,?,2) [*]).<*i,jj,ij*> by Th80
.= [*].<*i,ij*> by Th82
.= i*ij by Th85
.= i|^(j+1) by NEWTON:6;
hence p[j+1];
end;
reconsider ii = <*i*> as Element of 1-tuples_on NAT by FINSEQ_2:131;
[^].<*i,0*>=(1 const 1).ii by Th78
.= i|^0 by NEWTON:4;
then
A2: p[0];
for j being Nat holds p[j] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
definition
func [pred] -> 1-ary primitive-recursive Function equals
primrec(0 const 0, 2 proj 1, 1);
coherence;
end;
theorem Th88:
[pred].<*0*> = 0 & [pred].<*i+1*> = i
proof
defpred p[Nat] means [pred].<*$1+1*> = $1;
reconsider p0 = <*0, 0*> as Element of 2-tuples_on NAT by FINSEQ_2:101;
A2: arity (0 const 0) = 0;
A3: arity (2 proj 1) = 2;
A4: now
let i be Nat;
reconsider i1=i as Element of NAT by ORDINAL1:def 12;
reconsider p0 = <*i1+1,i1*> as Element of 2-tuples_on NAT by FINSEQ_2:101;
assume p[i];
then [pred].<*(i+1)+1*> = (2 proj 1).p0 by A2,A3,Th81
.= <*i+1, i*>.1 by Th37
.= i+1;
hence p[i+1];
end;
thus [pred].<*0*> = (0 const 0).{} by A2,Th79
.= 0;
then [pred].<*0+1*> = (2 proj 1).p0 by A2,A3,Th81
.= <*0, 0*>.1 by Th37
.= 0;
then
A5: p[0];
for i being Nat holds p[i] from NAT_1:sch 2(A5, A4);
hence thesis;
end;
definition
func [-] -> 2-ary primitive-recursive Function equals
primrec(1 proj 1,(1,2)->(1,?,2) ([pred]*<:<*2 proj 2*>:>), 2);
coherence;
end;
theorem
[-].<*i,j*> = i -' j
proof
set F = <*2 proj 2*>;
set g = [pred]*<:F:>;
rng F c= PrimRec
proof
let x be object;
assume x in rng F;
then x in {2 proj 2} by FINSEQ_1:39;
then x = 2 proj 2 by TARSKI:def 1;
hence thesis by Def14;
end;
then reconsider F as with_the_same_arity FinSequence of PrimRec
by FINSEQ_1:def 4;
defpred p[Nat] means [-].<*i,$1*> = i -' $1;
A1: for i, j holds g.<*i,0*> = 0 & g.<*i,j+1*> = j
proof
let i, j;
reconsider i1 = i, j1 = j as Element of NAT by ORDINAL1:def 12;
reconsider i0 = <*i1,0*> as Element of 2-tuples_on NAT by FINSEQ_2:101;
reconsider ij = <*i1,j1+1*> as Element of 2-tuples_on NAT by FINSEQ_2:101;
A2: dom (2 proj 2) = 2-tuples_on NAT by Th35;
A3: dom <:F:> = dom (2 proj 2) by FINSEQ_3:141;
hence g.<*i,0*> = [pred].(<:F:>.i0) by A2,FUNCT_1:13
.= [pred].<*(2 proj 2).i0*> by A2,FINSEQ_3:141
.= [pred].<*i0.2*> by Th37
.= 0 by Th88;
thus g.<*i,j+1*> = [pred].(<:F:>.ij) by A3,A2,FUNCT_1:13
.= [pred].<*(2 proj 2).ij*> by A2,FINSEQ_3:141
.= [pred].<*ij.2*> by Th37
.= j by Th88;
end;
A4: now
let j be Nat;
assume
A5: p[j];
A6: now
per cases by NAT_1:6;
suppose
A7: i-'j = 0;
then i <= j by NAT_D:36;
then i < j+1 by NAT_1:13;
then
A8: i-(j+1) < 0 by XREAL_1:49;
thus g.<*i,i-'j*> = 0 by A1,A7
.= i-'(j+1) by A8,XREAL_0:def 2;
end;
suppose
ex k being Nat st i-'j = k+1;
then consider k being Nat such that
A9: i-'j = k+1;
reconsider k as Element of NAT by ORDINAL1:def 12;
i - j = k+1 by A9,XREAL_0:def 2;
then
A10: i-(j+1) = k;
thus g.<*i,i-'j*> = k by A1,A9
.= i-'(j+1) by A10,XREAL_0:def 2;
end;
end;
reconsider jj=j as Element of NAT by ORDINAL1:def 12;
[-].<*i,jj+1*> =((1,2)->(1,?,2) g).<*i,jj,[-].<*i,jj*>*> by Th80
.= i-'(jj+1) by A5,A6,Th82;
hence p[j+1];
end;
reconsider i as Element of NAT by ORDINAL1:def 12;
reconsider ii = <*i*> as Element of 1-tuples_on NAT by FINSEQ_2:98;
[-].<*i,0*> = (1 proj 1).<*i*> by Th78
.= ii.1 by Th37
.= i+0-'0 by NAT_D:34
.= i-'0;
then
A11: p[0];
for j being Nat holds p[j] from NAT_1:sch 2(A11, A4);
hence thesis;
end;