Copyright (c) 2001 Association of Mizar Users
environ
vocabulary RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, FUNCT_4, MATRIX_2, BOOLE,
PARTFUN1, SETFAM_1, FUNCT_6, MSUALG_6, FRAENKEL, TARSKI, RFUNCT_3,
SEQM_3, UNIALG_1, FUNCOP_1, FUNCT_2, PRALG_3, ORDINAL1, FINSEQ_4,
BORSUK_1, PROB_1, FUNCT_5, FINSET_1, SQUARE_1, BINTREE1, CARD_3,
MONOID_0, QC_LANG1, GROUP_1, ARYTM_1, COMPUT_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
NAT_1, RELAT_1, RELSET_1, FUNCT_1, FINSEQ_1, FINSEQ_2, SETFAM_1,
MATRIX_2, FRAENKEL, FUNCT_2, FUNCT_4, FUNCT_5, PROB_1, CARD_3, PRE_CIRC,
FINSEQ_4, PARTFUN1, RFUNCT_3, PRALG_3, UNIALG_1, FUNCT_6, FUNCT_7,
FINSET_1, SQUARE_1, NEWTON, SEQM_3, BINARITH, CARD_4;
constructors DOMAIN_1, MATRIX_2, FINSEQ_4, PRALG_3, RFUNCT_3, FUNCT_7,
PRE_CIRC, BINARITH, SEQM_3, CARD_4, PROB_1;
clusters XREAL_0, PARTFUN1, RELAT_1, RELSET_1, FUNCT_1, FUNCOP_1, ALTCAT_1,
FINSEQ_1, FINSEQ_2, FUNCT_7, FINSET_1, SUBSET_1, NAT_1, FRAENKEL,
MEMBERED, PRE_CIRC, NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions FRAENKEL, PARTFUN1, RFUNCT_3, UNIALG_1, FUNCT_1, RELAT_1, SEQM_3,
TARSKI;
theorems TARSKI, AXIOMS, NAT_1, ZFMISC_1, RELAT_1, RELSET_1, FINSEQ_1,
FUNCOP_1, PARTFUN1, FINSEQ_2, MSUALG_1, FINSEQ_4, FUNCT_6, FUNCT_1,
RFUNCT_3, PROB_1, FUNCT_2, GRFUNC_1, FUNCT_7, FUNCT_4, FINSEQ_3,
GOBOARD1, REAL_1, SUBSET_1, MATRIX_2, PRALG_3, SETFAM_1, CARD_5,
SQUARE_1, PRE_CIRC, FINSET_1, UNIALG_1, SEQM_3, FUNCT_5, CARD_1, CARD_3,
FRAENKEL, NEWTON, BINARITH, REAL_2, JORDAN4, JORDAN2B, SCMFSA10,
WSIERP_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, ORDINAL2;
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;
definition
let X be non empty set, n be Nat, p be Element of n-tuples_on X,
i be Nat, x be Element of X;
redefine func p+*(i,x) -> Element of n-tuples_on X;
coherence proof dom (p+*(i,x)) = dom p by FUNCT_7:32;
then len (p+*(i,x)) = len p by FINSEQ_3:31 .= n by FINSEQ_2:109;
hence p+*(i,x) is Element of n-tuples_on X by FINSEQ_2:110;
end;
end;
definition
let n be Nat, t be Element of n-tuples_on NAT, i be Nat;
redefine func t.i -> Element of NAT;
coherence proof
per cases;
suppose i in dom t; hence thesis by FINSEQ_2:13;
suppose not i in dom t; hence thesis by CARD_1:51,FUNCT_1:def 4;
end;
end;
canceled 2;
theorem Th3:
<*x,y*>+*(1,z) = <*z,y*> & <*x,y*>+*(2,z) = <*x,z*>
proof set a = <*x,y*>+*(1,z), b = <*x,y*>+*(2,z);
A1: len <*x,y*> = 2 & <*x,y*>.1 = x & <*x,y*>.2 = y by FINSEQ_1:61;
then A2: 1 in dom <*x,y*> & 2 in dom <*x,y*> by FINSEQ_3:27;
then len a = 2 & a.1 = z & a.2 = y by A1,FUNCT_7:33,34,JORDAN2B:12;
hence <*x,y*>+*(1,z) = <*z,y*> by FINSEQ_1:61;
len b = 2 & b.1 = x & b.2 = z by A1,A2,FUNCT_7:33,34,JORDAN2B:12;
hence <*x,y*>+*(2,z) = <*x,z*> by FINSEQ_1:61;
end;
canceled;
theorem Th5:
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 (f+*(i,x)) = dom f by FUNCT_7:32;
A3: dom (g+*(i,y)) = dom g by FUNCT_7:32;
A4: dom (g+*(i,z)) = dom g by FUNCT_7:32;
now
thus dom (f+*(i,z)) = dom f by FUNCT_7:32;
thus dom (g+*(i,z)) = dom f by A1,A3,A4,FUNCT_7:32;
let a be set; assume
A5: a in dom f;
per cases;
suppose A6: a = i;
hence (f+*(i,z)).a = z by A5,FUNCT_7:33
.= g+*(i,z).a by A1,A2,A3,A5,A6,FUNCT_7:33;
suppose A7: a <> i;
hence (f+*(i,z)).a = f.a by FUNCT_7:34 .= (g+*(i,y)).a by A1,A7,FUNCT_7:34
.= g.a by A7,FUNCT_7:34 .= (g+*(i,z)).a by A7,FUNCT_7:34;
end;
hence f+*(i,z) = g+*(i,z) by FUNCT_1:9;
end;
theorem Th6:
Del(p+*(i,x),i) = Del(p,i)
proof set f = p;
per cases;
suppose A1: i in dom f;
then 1 <= i & i <= len f by FINSEQ_3:27;
then 0 <> len f by AXIOMS:22;
then consider j being Nat such that
A2: len f = j+1 by NAT_1:22;
A3: dom (f+*(i,x)) = dom f by FUNCT_7:32;
then A4: len (f+*(i,x)) = len f by FINSEQ_3:31;
now thus len Del(f+*(i,x),i) = j by A1,A2,A3,A4,GOBOARD1:6;
thus len Del(f,i) = j by A1,A2,GOBOARD1:6;
let a be Nat; assume a in Seg j;
then A5: 1 <= a & a <= j by FINSEQ_1:3;
per cases;
suppose A6: a < i;
hence Del(f+*(i,x),i).a = (f+*(i,x)).a by A2,A4,GOBOARD1:8
.= f.a by A6,FUNCT_7:34 .= Del(f,i).a by A2,A6,GOBOARD1:8;
suppose A7: i <= a;
then A8: i < a+1 by NAT_1:38;
thus Del(f+*(i,x),i).a = (f+*(i,x)).(a+1) by A1,A2,A3,A4,A5,A7,GOBOARD1:9
.= f.(a+1) by A8,FUNCT_7:34 .= Del(f,i).a by A1,A2,A5,A7,GOBOARD1:9;
end;
hence Del(f+*(i,x),i) = Del(f,i) by FINSEQ_2:10;
suppose not i in dom f;
hence Del(f+*(i,x),i) = Del(f,i) by FUNCT_7:def 3;
end;
theorem Th7:
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 dx = Del(x,i), dy = Del(y,i); set xi = x+*(i,a), yi = y+*(i,a);
A2: dom xi = dom x & dom yi = dom y by FUNCT_7:32;
A3: Seg len xi = dom xi & Seg len x = dom x & Seg len yi = dom yi &
Seg len y = dom y by FINSEQ_1:def 3;
then A4: len xi = len x & len yi = len y by A2,FINSEQ_1:8;
per cases;
suppose A5: i in dom x;
now thus len dx = len dx; x <> {} by A5,FINSEQ_1:26;
then len x <> 0 by FINSEQ_1:25; then consider m being Nat such that
A6: len x = m+1 by NAT_1:22;
A7: len dx = m by A5,A6,GOBOARD1:6;
hence len dy = len dx by A1,A3,A4,A5,A6,GOBOARD1:6;
let j be Nat such that
A8: j in Seg len dx;
A9: 1 <= j & j <= m by A7,A8,FINSEQ_1:3;
per cases;
suppose A10: j < i;
hence dx.j = x.j by A6,GOBOARD1:8 .= yi.j by A1,A10,FUNCT_7:34
.= y.j by A10,FUNCT_7:34 .= dy.j by A1,A4,A6,A10,GOBOARD1:8;
suppose A11: i <= j; then A12: j+1 > i by NAT_1:38;
thus dx.j = x.(j+1) by A5,A6,A9,A11,GOBOARD1:9
.= yi.(j+1) by A1,A12,FUNCT_7:34 .= y.(j+1) by A12,FUNCT_7:34
.= dy.j by A1,A3,A4,A5,A6,A9,A11,GOBOARD1:9;
end;
hence Del(x,i) = Del(y,i) by FINSEQ_2:10;
suppose not i in dom x; then xi = x & yi = y by A1,A2,FUNCT_7:def 3;
hence Del(x,i) = Del(y,i) by A1;
end;
theorem Th8:
0-tuples_on X = {{}}
proof set S = {s where s is Element of X*: len s = 0};
A1: 0-tuples_on X = S by FINSEQ_2:def 4;
A2: len <*>(X*) = 0 by FINSEQ_1:25;
now let x be set;
hereby assume x in S; then consider s being Element of X* such that
A3: x = s & len s = 0; s = {} by A3,FINSEQ_1:25;
hence x in {{}} by A3,TARSKI:def 1;
end;
assume x in {{}};
then A4: x = {} by TARSKI:def 1; <*>(X*) is Element of X* by FINSEQ_1:66
;
hence x in S by A2,A4;
end;
hence thesis by A1,TARSKI:2;
end;
theorem
n <> 0 implies n-tuples_on {} = {}
proof assume that
A1: n <> 0 and
A2: n-tuples_on {} <> {};
A3: n-tuples_on {} = {s where s is Element of {}*
: len s = n} by FINSEQ_2:def 4;
consider x such that
A4: x in n-tuples_on {} by A2,XBOOLE_0:def 1;
consider s being Element of {}* such that
A5: s = x & len s = n by A3,A4;
rng s c= {} by FINSEQ_1:def 4; then rng s = {} by XBOOLE_1:3;
then s = {} by RELAT_1:64;
hence contradiction by A1,A5,FINSEQ_1:25;
end;
theorem Th10:
{} in rng f implies <:f:> = {}
proof assume
A1: {} in rng f;
A2: dom <:f:> = meet doms f by FUNCT_6:49 .= meet rng doms f by FUNCT_6:def 4;
consider x being set such that
A3: x in dom f & f.x = {} by A1,FUNCT_1:def 5;
A4: dom doms f = f"SubFuncs rng f by FUNCT_6:def 2;
then A5: x in dom doms f by A3,FUNCT_6:28;
then (doms f).x = {} by A3,A4,FUNCT_5:10,FUNCT_6:def 2;
then {} in rng doms f by A5,FUNCT_1:12; then meet rng doms f = {} by
SETFAM_1:5;
hence <:f:> = {} by A2,RELAT_1:64;
end;
theorem Th11:
rng f = D implies rng <:<*f*>:> = 1-tuples_on D
proof set X = D; assume
A1: rng f = X;
A2: dom <:<*f*>:> = dom f by FUNCT_6:61;
now let x be set;
hereby assume x in rng <:<*f*>:>; then consider y being set such that
A3: y in dom <:<*f*>:> & <:<*f*>:>.y = x by FUNCT_1:def 5;
A4: <:<*f*>:>.y = <*f.y*> by A2,A3,FUNCT_6:61;
reconsider fy = f.y as Element of X by A1,A2,A3,FUNCT_1:12; <*fy*> is
Element of 1-tuples_on X;
hence x in 1-tuples_on X by A3,A4;
end; assume x in 1-tuples_on X; then consider d being Element of X such
that
A5: x = <*d*> by FINSEQ_2:117; consider y being set such that
A6: y in dom f & f.y = d by A1,FUNCT_1:def 5;
<:<*f*>:>.y = <*d*> by A6,FUNCT_6:61;
hence x in rng <:<*f*>:> by A2,A5,A6,FUNCT_1:12;
end;
hence rng <:<*f*>:> = 1-tuples_on X by TARSKI:2;
end;
theorem Th12:
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
A1: 1 <= i & i <= n+1;
let p be Element of (n+1)-tuples_on X;
A2: len p = n+1 by FINSEQ_2:109;
then A3: i in dom p by A1,FINSEQ_3:27;
A4: Del(p,i) is FinSequence of X by MATRIX_2:9;
len Del(p,i) = n by A2,A3,GOBOARD1:6;
then Del(p,i) is Element of n-tuples_on X by A4,FINSEQ_2:110;
hence Del(p,i) in n-tuples_on X;
end;
theorem Th13:
for X being set, Y being FinSequenceSet of X holds Y c= X*
proof let X be set, Y be FinSequenceSet of X;
let x be set; assume x in Y; then x is FinSequence of X by FINSEQ_2:def 3;
hence thesis by FINSEQ_1:def 11;
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;
definition
cluster non empty functional compatible set;
existence proof set A = {{}};
A1: A is compatible proof let f, g be Function; assume f in A & g in A;
then f={} by TARSKI:def 1; then f c= g by XBOOLE_1:2;
hence f tolerates g by PARTFUN1:135;
end; take A; thus thesis by A1;
end;
end;
definition
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 set;
assume
A1: [x,y1] in union X & [x,y2] in union X; then consider f being set such
that
A2: [x,y1] in f & f in X by TARSKI:def 4; consider g being set such that
A3: [x,y2] in g & g in X by A1,TARSKI:def 4;
reconsider f, g as Function by A2,A3,FRAENKEL:def 1;
A4: x in dom f & x in dom g by A2,A3,RELAT_1:def 4;
then A5: f.x = y1 & g.x = y2 by A2,A3,FUNCT_1:def 4;
A6: x in dom f /\ dom g by A4,XBOOLE_0:def 3
; f tolerates g by A2,A3,Def1
;
hence y1 = y2 by A5,A6,PARTFUN1:def 6;
end;
thus union X is Relation-like proof let x be set; assume
x in union X; then consider f being set such that
A7: x in f & f in X by TARSKI:def 4;
f is Function by A7,FRAENKEL:def 1; then consider y, z being set such
that
A8: x = [y,z] by A7,RELAT_1:def 1; thus thesis by A8;
end;
end;
end;
theorem Th14:
X is functional compatible iff union X is Function
proof
A1: now assume
A2: union X is Function;
thus X is functional proof let f be set; assume
A3: f in X;
A4: f is Function-like proof let x, y1, y2 be set; assume
[x,y1] in f & [x, y2] in f;
then [x,y1] in union X & [x,y2] in union X by A3,TARSKI:def 4;
hence y1 = y2 by A2,FUNCT_1:def 1;
end;
f is Relation-like proof let x be set; assume x in f;
then x in union X by A3,TARSKI:def 4;
hence ex y, z being set st x = [y,z] by A2,RELAT_1:def 1;
end;
hence f is Function by A4;
end;
thus X is compatible proof let f,g be Function such that
A5: f in X & g in X;
let x be set; assume x in dom f /\ dom g;
then A6: x in dom f & x in dom g by XBOOLE_0:def 3
; then consider y1 being set such that
A7: [x,y1] in f by RELAT_1:def 4;
consider y2 being set such that
A8: [x,y2] in g by A6,RELAT_1:def 4;
[x,y1] in union X & [x,y2] in union X by A5,A7,A8,TARSKI:def 4;
then A9: y1 = y2 by A2,FUNCT_1:def 1;
thus f.x = y1 by A6,A7,FUNCT_1:def 4 .= g.x by A6,A8,A9,FUNCT_1:def 4;
end;
end;
now assume X is functional compatible;
then reconsider X' = X as functional compatible set; union X' is
Function;
hence union X is Function;
end;
hence X is functional compatible iff union X is Function by A1;
end;
definition
let X,Y be set;
cluster non empty compatible PFUNC_DOMAIN of X,Y;
existence proof set A = {{}};
now let x be Element of A;
A1: x = {} by TARSKI:def 1; dom {} c= X & rng {} c= Y by XBOOLE_1:2;
hence x is PartFunc of X, Y by A1,RELSET_1:11;
end;
then A2: A is PFUNC_DOMAIN of X,Y by RFUNCT_3:def 3;
A is compatible proof let f, g be Function;
assume f in A & g in A; then f = {} by TARSKI:def 1; then f c= g by XBOOLE_1
:2;
hence f tolerates g by PARTFUN1:135;
end;
hence thesis by A2;
end;
end;
theorem Th15:
for X being non empty functional compatible set
holds dom union X = union {dom f where f is Element of X: not contradiction}
proof let X be non empty functional compatible set;
set F = {dom f where f is Element of X: not contradiction};
now let x be set;
hereby assume x in dom union X; then consider y being set such that
A1: [x,y] in union X by RELAT_1:def 4; consider Z being set such that
A2: [x,y] in Z & Z in X by A1,TARSKI:def 4;
reconsider Z as Element of X by A2;
A3: x in dom Z by A2,RELAT_1:20; dom Z in F;
hence x in union F by A3,TARSKI:def 4;
end; assume x in union F; then consider Z being set such that
A4: x in Z & Z in F by TARSKI:def 4; consider f being Element of X such that
A5: Z = dom f & not contradiction by A4; consider y being set such that
A6: [x, y] in f by A4,A5,RELAT_1:def 4; [x, y] in union X by A6,TARSKI:def 4
;
hence x in dom union X by RELAT_1:20;
end;
hence dom union X = union {dom f where f is Element of X: not contradiction}
by TARSKI:2;
end;
theorem Th16:
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 set; assume
x in dom f; then consider y being set such that
A2: [x,y] in f by RELAT_1:def 4; [x, y] in union X by A1,A2,TARSKI:def 4;
hence x in dom union X by RELAT_1:20;
end; let x being set; assume x in dom f; then consider y being set such that
A3: [x,y] in f by RELAT_1:def 4; [x, y] in union X by A1,A3,TARSKI:def 4;
hence (union X).x = y by FUNCT_1:8 .= f.x by A3,FUNCT_1:8;
end;
theorem Th17:
for X being non empty functional compatible set
holds rng union X = union {rng f where f is Element of X: not contradiction}
proof let X be non empty functional compatible set;
set F = {rng f where f is Element of X: not contradiction};
now let y be set;
hereby assume y in rng union X; then consider x being set such that
A1: [x,y] in union X by RELAT_1:def 5; consider Z being set such that
A2: [x,y] in Z & Z in X by A1,TARSKI:def 4;
reconsider Z as Element of X by A2;
A3: y in rng Z by A2,RELAT_1:20; rng Z in F;
hence y in union F by A3,TARSKI:def 4;
end; assume y in union F; then consider Z being set such that
A4: y in Z & Z in F by TARSKI:def 4; consider f being Element of X such that
A5: Z = rng f & not contradiction by A4; consider x being set such that
A6: [x, y] in f by A4,A5,RELAT_1:def 5;
[x, y] in union X by A6,TARSKI:def 4;
hence y in rng union X by RELAT_1:20;
end;
hence thesis by TARSKI:2;
end;
definition let X,Y;
cluster -> functional PFUNC_DOMAIN of X,Y;
coherence
proof
let P be PFUNC_DOMAIN of X,Y;
let x be set;
assume x in P;
hence thesis by RFUNCT_3:def 3;
end;
end;
theorem Th18:
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 = {dom f where f is Element of D: not contradiction};
set F = {rng f where f is Element of D: not contradiction};
reconsider u = union D as Function;
A1: dom u c= X proof let x be set; assume x in dom u;
then x in union E by Th15; then consider Z being set such that
A2: x in Z & Z in E by TARSKI:def 4; consider f being Element of D such that
A3: Z = dom f & not contradiction by A2;
thus x in X by A2,A3;
end;
rng u c= Y proof let y be set; assume y in rng u;
then y in union F by Th17; then consider Z being set such that
A4: y in Z & Z in F by TARSKI:def 4; consider f being Element of D such that
A5: Z = rng f & not contradiction by A4; rng f c= Y by RELSET_1:12;
hence y in Y by A4,A5;
end;
hence thesis by A1,RELSET_1:11;
end;
begin :: Homogeneous relations
definition
let f be Relation;
redefine attr f is natural-yielding;
synonym f is to-naturals;
end;
definition
let f be Relation;
attr f is from-natural-fseqs means
:Def2: dom f c= NAT*;
end;
definition
cluster from-natural-fseqs to-naturals Function;
existence proof take f={}; thus dom f c= NAT* & rng f c= NAT by XBOOLE_1:2
; end;
end;
definition
let f be from-natural-fseqs Relation;
attr f is len-total means:Def3:
for x,y being FinSequence of NAT
st len x = len y & x in dom f holds y in dom f;
end;
definition
let f be Relation;
attr f is homogeneous means :Def4:
for x,y being FinSequence st x in dom f & y in dom f holds len x = len y;
end;
theorem Th19:
dom R c= n-tuples_on D implies R is homogeneous
proof set X = D; assume
A1: dom R c= n-tuples_on X; let x,y be FinSequence such that
A2: x in dom R & y in dom R;
reconsider x' = x, y' = y as Element of n-tuples_on X by A1,A2;
len x' = n & len y' = n by FINSEQ_2:109;
hence len x = len y;
end;
definition
cluster {} -> homogeneous;
coherence proof let x,y be FinSequence; assume x in dom {}; thus thesis; end
;
end;
definition
let p be FinSequence, x be set;
cluster {p} --> x -> non empty homogeneous;
coherence proof set f = {p} --> x;
A1: dom f = {p} by FUNCOP_1:19;
thus f is non empty by FUNCOP_1:19,RELAT_1:60; let x,y be FinSequence;
assume
x in dom f & y in dom f; then x = p & y = p by A1,TARSKI:def 1;
hence thesis;
end;
end;
definition
cluster non empty homogeneous Function;
existence proof consider p being FinSequence;take {p}-->0; thus thesis; end;
end;
definition
let f be homogeneous Function, g be Function;
cluster g*f -> homogeneous;
coherence proof let x,y be FinSequence such that
A1: x in dom (g*f) & y in dom (g*f); dom (g*f) c= dom f by RELAT_1:44; hence
thesis by A1,Def4;
end;
end;
definition
let X,Y be set;
cluster homogeneous PartFunc of X*, Y;
existence proof set f = {}; dom f c= X* & rng f c= Y by XBOOLE_1:2;
then reconsider f as PartFunc of X*, Y by RELSET_1:11;
take f; let x,y be FinSequence; assume
x in dom f & y in dom f;
hence thesis by RELAT_1:60;
end;
end;
definition
let X,Y be non empty set;
cluster non empty homogeneous PartFunc of X*, Y;
existence proof consider n being Nat, y being Element of Y;
reconsider Z = n-tuples_on X as non empty Subset of X* by Th13;
reconsider f = Z --> y as PartFunc of X*, Y;
take f;
A1: dom f = Z by FUNCOP_1:19;
thus f is non empty by FUNCOP_1:19,RELAT_1:60;
let x,y be FinSequence; assume x in dom f & y in dom f;
then len x = n & len y = n by A1,FINSEQ_2:109;
hence thesis;
end;
end;
definition
let X be non empty set;
cluster non empty homogeneous quasi_total PartFunc of X*, X;
existence proof consider n being Nat, y being Element of X;
reconsider Z = n-tuples_on X as non empty Subset of X* by Th13;
reconsider f = Z --> y as PartFunc of X*, X;
take f;
A1: dom f = Z by FUNCOP_1:19;
thus f is non empty by FUNCOP_1:19,RELAT_1:60;
thus f is homogeneous proof let x,y be FinSequence; assume
x in dom f & y in dom f; then len x = n & len y = n by A1,FINSEQ_2:109
;
hence thesis;
end;
let p,q be FinSequence of X; assume len p = len q & p in dom f;
then len q = n by A1,FINSEQ_2:109; then q is Element of Z by FINSEQ_2:110
;
hence thesis by A1;
end;
end;
definition
cluster non empty homogeneous to-naturals len-total
(from-natural-fseqs Function);
existence proof consider n, m being Nat;
reconsider Z = n-tuples_on NAT as non empty Subset of NAT* by Th13;
set f = Z --> m;
A1: dom f = Z & rng f c= {m} by FUNCOP_1:19;
then reconsider f as from-natural-fseqs Function by Def2;
take f;
A2: f is homogeneous proof let x,y be FinSequence; assume
x in dom f & y in dom f; then len x = n & len y = n by A1,FINSEQ_2:109;
hence thesis;
end; {m} is Subset of NAT by SUBSET_1:55;
then A3: rng f c= NAT by A1,XBOOLE_1:1;
f is len-total proof let x,y be FinSequence of NAT such that
A4: len x = len y and
A5: x in dom f;
A6: y is Element of (len y)-tuples_on NAT by FINSEQ_2:110;
len x = n by A1,A5,FINSEQ_2:109;
hence y in dom f by A1,A4,A6;
end;
hence thesis by A2,A3,FUNCOP_1:19,RELAT_1:60,SEQM_3:def 8;
end;
end;
definition
cluster -> to-naturals from-natural-fseqs PartFunc of NAT*, NAT;
coherence proof let f be PartFunc of NAT*,NAT; A1: rng f c=NAT by RELSET_1:12;
dom f c= NAT*;
hence thesis by A1,Def2,SEQM_3:def 8;
end;
end;
definition
cluster quasi_total -> len-total PartFunc of NAT*,NAT;
coherence proof let f be PartFunc of NAT*,NAT; assume
A1: f is quasi_total; let x,y be FinSequence of NAT such that
A2: len x = len y & x in dom f;
thus y in dom f by A1,A2,UNIALG_1:def 2;
end;
end;
theorem Th20:
for g being len-total to-naturals (from-natural-fseqs Function)
holds g is quasi_total PartFunc of NAT*, NAT
proof let g be len-total to-naturals (from-natural-fseqs Function);
A1: dom g c= NAT* by Def2;
rng g c= NAT by SEQM_3:def 8;
then reconsider g' = g as PartFunc of NAT*, NAT by A1,RELSET_1:11;
for x,y being FinSequence of NAT
st len x = len y & x in dom g holds y in dom g by Def3;
then g' is quasi_total by UNIALG_1:def 2;
hence g is quasi_total PartFunc of NAT*, NAT;
end;
definition
let f be homogeneous Relation;
func arity f -> Nat means :Def5:
for x being FinSequence st x in dom f holds it = len x
if ex x being FinSequence st x in dom f
otherwise it = 0;
existence proof
hereby given x being FinSequence such that
A1: x in dom f; take i = len x;
thus for x being FinSequence st x in dom f holds i = len x by A1,Def4;
end; thus thesis;
end;
uniqueness proof let i1, i2 be Nat;
hereby given x being FinSequence such that
A2: x in dom f;assume for x being FinSequence st x in dom f holds i1 = len x
;
then i1 = len x by A2;
hence (for x being FinSequence st x in dom f holds i2 = len x) implies
i1 = i2 by A2;
end; thus thesis;
end;
correctness;
end;
theorem Th21:
arity {} = 0
proof not ex x being FinSequence st x in dom {}; hence thesis by Def5; end;
theorem Th22:
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 arity f = len {} by Def5 .= 0 by FINSEQ_1:25;
end;
theorem Th23:
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 set; assume
A1: x in dom f;
per cases;
suppose A2: X is empty;
then x = <*>(X*) by A1,FUNCT_7:19,TARSKI:def 1;
then A3: arity f = len <*>(X*) by A1,Def5;
A4: len <*>(X*) = 0 by FINSEQ_1:25; 0-tuples_on X = {{}} by Th8;
hence x in (arity f)-tuples_on X by A1,A2,A3,A4,FUNCT_7:19;
suppose X is non empty; then reconsider X' = X as non empty set;
reconsider x' = x as FinSequence of X' by A1,FINSEQ_1:def 11;
len x' = arity f by A1,Def5;
then x' is Element of (arity f)-tuples_on X' by FINSEQ_2:110;
hence x in (arity f)-tuples_on X;
end;
theorem Th24:
for f being homogeneous from-natural-fseqs Function
holds dom f c= (arity f)-tuples_on NAT
proof let f be homogeneous from-natural-fseqs Function; let x be set; assume
A1: x in dom f; dom f c= NAT* by Def2;
then reconsider x' = x as FinSequence of NAT by A1,FINSEQ_1:def 11;
len x' = arity f by A1,Def5;
then x' is Element of (arity f)-tuples_on NAT by FINSEQ_2:110;
hence x in (arity f)-tuples_on NAT;
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 Th23;
hereby assume f is quasi_total non empty;
then reconsider f' = f as quasi_total non empty homogeneous PartFunc of X*,
X;
consider x being set such that
A2: x in dom f' by XBOOLE_0:def 1;
reconsider x' = x as FinSequence of X by A2,FINSEQ_1:def 11;
A3: len x' = arity f by A2,Def5;
now let z be set; 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 z' = z as Element of (arity f)-tuples_on X;
len z'=arity f by FINSEQ_2:109;
hence z in dom f by A2,A3,UNIALG_1:def 2;
end;
hence dom f = (arity f)-tuples_on X by TARSKI:2;
end;
assume A4: dom f = (arity f)-tuples_on X;
thus f is quasi_total proof let x, y be FinSequence of X; assume
A5: len x = len y & x in dom f; then len x = arity f by A4,FINSEQ_2:109;
then y is Element of (arity f)-tuples_on X by A5,FINSEQ_2:110;
hence y in dom f by A4;
end;
thus f is non empty by A4,RELAT_1:60;
end;
theorem Th25:
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 rng f c= {} by RELSET_1:12;
then rng f = {} by XBOOLE_1:3;
then f = {} by RELAT_1:64;
hence f is quasi_total non empty iff dom f = (arity f)-tuples_on X by Th8,
Th21,RELAT_1:60;
suppose X is non empty;
hence f is quasi_total non empty iff dom f = (arity f)-tuples_on X by Lm1;
end;
theorem Th26:
for f being homogeneous to-naturals from-natural-fseqs Function
holds f is len-total non empty iff dom f = (arity f)-tuples_on NAT
proof let f being homogeneous to-naturals from-natural-fseqs Function;
A1: dom f c= (arity f)-tuples_on NAT by Th24;
hereby assume f is len-total non empty;
then reconsider f' = f as quasi_total non empty homogeneous
PartFunc of NAT*, NAT by Th20;
consider x being set such that
A2: x in dom f' by XBOOLE_0:def 1;
reconsider x' = x as FinSequence of NAT by A2,FINSEQ_1:def 11;
A3: len x' = arity f by A2,Def5;
now let z be set;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 z' = z as Element of (arity f)-tuples_on NAT;
len z' = arity f by FINSEQ_2:109;
hence z in dom f by A2,A3,UNIALG_1:def 2;
end;
hence dom f = (arity f)-tuples_on NAT by TARSKI:2;
end; assume A4: dom f = (arity f)-tuples_on NAT;
thus f is len-total proof let x, y be FinSequence of NAT; assume
A5: len x = len y & x in dom f; then len x = arity f by A4,FINSEQ_2:109;
then y is Element of (arity f)-tuples_on NAT by A5,FINSEQ_2:110;
hence y in dom f by A4;
end;
thus f is non empty by A4,RELAT_1:60;
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; assume
A1: dom f c= n-tuples_on D; consider x being set such that
A2: x in dom f by XBOOLE_0:def 1;
reconsider x as Element of n-tuples_on D by A1,A2;
A3: x in dom f by A2;
for x being FinSequence st x in dom f holds n = len x by A1,FINSEQ_2:109;
hence arity f = n by A3,Def5;
end;
theorem Th28:
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; assume
A1: dom f = n-tuples_on D; consider x being set such that
A2: x in n-tuples_on D by XBOOLE_0:def 1;
reconsider x as Element of n-tuples_on D by A2;
A3: x in dom f by A1;
for x be FinSequence st x in dom f holds len x = n by A1,FINSEQ_2:109;
hence arity f = n by A3,Def5;
end;
definition
let R be Relation;
attr R is with_the_same_arity means:Def6:
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 Nat, X being non empty set
st dom f c= n-tuples_on X & dom g c= n-tuples_on X);
end;
definition
cluster {} -> with_the_same_arity;
coherence proof let f, g be Function; thus thesis; end;
end;
definition
cluster with_the_same_arity FinSequence;
existence proof take {}; thus thesis; end;
let X be set;
cluster with_the_same_arity FinSequence of X;
existence proof take <*>X; thus thesis; end;
cluster with_the_same_arity 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 -> Nat means:Def7:
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,Def6;
suppose g is empty; hence i = arity g by A3;
suppose dom g = {{}}; hence i = arity g by A3,Th21,Th22;
end;
suppose A4: g is empty;
thus i = arity g proof
per cases by A1,A2,A4,Def6;
suppose f is empty; hence i = arity g by A4;
suppose dom f = {{}}; hence i = arity g by A4,Th21,Th22;
end;
suppose A5: f is non empty & g is non empty;
then consider n being Nat, X being non empty set such that
A6: dom f c= n-tuples_on X & dom g c= n-tuples_on X by A1,A2,Def6;
consider a being Element of dom f; A7: dom f <> {} by A5,RELAT_1:64;
then a in dom f; then reconsider a as Element of n-tuples_on X by A6;
A8: arity f = len a by A7,Def5 .= n by FINSEQ_2:109;
consider a being Element of dom g; A9: dom g <> {} by A5,RELAT_1:64;
then a in dom g; then reconsider a as Element of n-tuples_on X by A6;
arity g = len a by A9,Def5;
hence i = arity g by A8,FINSEQ_2:109;
end;
thus thesis;
end;
uniqueness proof let i1, i2 be 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 for f being homogeneous Function holds not f in rng F
by FINSEQ_1:25,RELAT_1:60;
hence arity F = 0 by Def7;
end;
definition
let X be set;
func HFuncs X -> PFUNC_DOMAIN of X*, X equals:Def8:
{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 PARTFUN1:56;
then {} in PFuncs(X*, X) by PARTFUN1:119; then {} in H;
hence H is non empty;
let x be set; assume x in H;
then ex g being Element of PFuncs(X*, X) st x = g & g is homogeneous;
hence x is Function;
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 Th30:
{} in HFuncs X
proof set f = {}; dom f c= X* & rng f c= X by XBOOLE_1:2;
then reconsider f as PartFunc of X*, X by RELSET_1:11;
reconsider f as Element of PFuncs(X*, X) by PARTFUN1:119;
f in {g where g is Element of PFuncs(X*, X): g is homogeneous};
hence {} in HFuncs X by Def8;
end;
definition
let X be non empty set;
cluster non empty homogeneous quasi_total Element of HFuncs X;
existence proof consider x being Element of X; set p = <*>X;
p in X* by FINSEQ_1:def 11;
then reconsider Y = {p} as Subset of X* by ZFMISC_1:37;
{p} --> x is homogeneous & Y --> x in PFuncs(X*, X);
then {p} --> x in {f where f is Element of PFuncs(X*
, X): f is homogeneous};
then reconsider f = {p} --> x as Element of HFuncs X by Def8;
take f;
A1: dom f = {p} by FUNCOP_1:19;
thus f is non empty homogeneous; let a,b be FinSequence of X such that
A2: len a = len b; assume a in dom f; then a = p by A1,TARSKI:def 1;
then len b = 0 by A2,FINSEQ_1:25; then b = {} by FINSEQ_1:25;
hence thesis by A1,TARSKI:def 1;
end;
end;
definition
let X be set;
cluster -> homogeneous Element of HFuncs X;
coherence proof let f be Element of HFuncs X;
HFuncs X = {g where g is Element of PFuncs(X*, X): g is homogeneous} &
f in HFuncs X by Def8;
then ex g being Element of PFuncs(X*, X) st f = g & g is homogeneous;
hence thesis;
end;
end;
definition
let X be non empty set, S be non empty Subset of HFuncs X;
cluster -> homogeneous Element of S;
coherence proof let f be Element of S;
HFuncs X = {g where g is Element of PFuncs(X*, X): g is homogeneous} &
f in HFuncs X by Def8;
then ex g being Element of PFuncs(X*, X) st f = g & g is homogeneous;
hence thesis;
end;
end;
theorem Th31:
for f being to-naturals homogeneous from-natural-fseqs Function
holds f is Element of HFuncs NAT
proof let f be to-naturals homogeneous from-natural-fseqs Function;
dom f c= NAT* & rng f c= NAT by Def2,SEQM_3:def 8;
then f is PartFunc of NAT*,NAT by RELSET_1:11;
then reconsider f'=f as Element of PFuncs(NAT*,NAT) by PARTFUN1:119;
f' in {f1 where f1 is Element of PFuncs(NAT*,NAT): f1 is homogeneous};
hence f is Element of HFuncs NAT by Def8;
end;
theorem Th32:
for f being len-total to-naturals (homogeneous from-natural-fseqs Function)
holds f is quasi_total Element of HFuncs NAT
proof let f be len-total to-naturals (homogeneous from-natural-fseqs Function);
reconsider f'=f as Element of HFuncs NAT by Th31;
f' is quasi_total proof
let x,y be FinSequence of NAT; assume len x = len y & x in dom f';
hence y in dom f' by Def3;
end;
hence f is quasi_total Element of HFuncs NAT;
end;
theorem Th33:
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
A3: f in rng R & g in rng R;
then reconsider f' = f, g' = g as Element of HFuncs X by A1;
A4: arity f' = arity g' by A2,A3;
hereby assume f is empty;
then dom g' c= 0-tuples_on X by A4,Th21,Th23; then dom g' c= {<*>X} by
FINSEQ_2:112;
then dom g = {} or dom g = {{}} by ZFMISC_1:39;
hence g is empty or dom g = {{}} by RELAT_1:64;
end; assume f is non empty & g is non empty;
then reconsider f' as non empty Element of HFuncs X;
take n = arity f', X;
thus dom f c= n-tuples_on X & dom g c= n-tuples_on X by A4,Th23;
end;
definition
let n, m be Nat;
func n const m -> homogeneous to-naturals from-natural-fseqs Function equals
:Def9: (n-tuples_on NAT) --> m;
coherence proof set X=NAT; set f = (n-tuples_on X)-->m;
A1: dom f = n-tuples_on X by FUNCOP_1:19;
A2: n-tuples_on X c= X* by MSUALG_1:12;
rng f c= {m} & {m} c= X by FUNCOP_1:19,ZFMISC_1:37;
then A3: rng f c= X by XBOOLE_1:1;
f is homogeneous proof let x,y be FinSequence; assume
x in dom f & y in dom f; then len x = n & len y = n by A1,FINSEQ_2:
109
;
hence len x = len y;
end;
hence thesis by A1,A2,A3,Def2,SEQM_3:def 8;
end;
end;
theorem Th34:
n const m in HFuncs NAT
proof set X=NAT; set f=n const m;
A1: dom f c= NAT* by Def2;
rng f c= NAT by SEQM_3:def 8;
then f is PartFunc of X*, X by A1,RELSET_1:11;
then f is Element of PFuncs(X*, X) by PARTFUN1:119;
then f in {g where g is Element of PFuncs(X*, X): g is homogeneous};
hence thesis by Def8;
end;
definition
let n,m be Nat;
cluster n const m -> len-total non empty;
coherence proof set X = NAT;
A1: dom (n const m) = dom ((n-tuples_on X)-->m) by Def9
.= n-tuples_on X by FUNCOP_1:19;
n const m is len-total proof let x, y be FinSequence of X; assume
A2: len x = len y & x in dom (n const m); then len x = n by A1,FINSEQ_2:109
;
then y is Element of n-tuples_on X by A2,FINSEQ_2:110;
hence y in dom (n const m) by A1;
end;
hence thesis by A1,RELAT_1:60;
end;
end;
theorem Th35:
arity (n const m) = n
proof set X = NAT;
A1: dom (n const m) = dom ((n-tuples_on X)-->m) by Def9
.= n-tuples_on X by FUNCOP_1:19;
consider d being Element of n-tuples_on X;
A2: d in dom (n const m) by A1;
for x be FinSequence st x in dom (n const m) holds n=len x by A1,FINSEQ_2:
109;
hence arity (n const m) = n by A2,Def5;
end;
theorem Th36:
for t being Element of n-tuples_on NAT holds (n const m).t = m
proof set X = NAT; let t be Element of n-tuples_on X;
thus (n const m).t = ((n-tuples_on X) --> m).t by Def9 .= m by FUNCOP_1:13;
end;
definition
let n,i be Nat;
func n succ i -> homogeneous to-naturals from-natural-fseqs Function means:
Def10: dom it = n-tuples_on NAT &
for p being Element of n-tuples_on NAT holds it.p = (p/.i)+1;
existence proof
defpred p[set] means $1 in n-tuples_on NAT;
deffunc f(Element of NAT*) = ($1/.i)+1;
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 LambdaPFD;
A3: n-tuples_on NAT c= NAT* by MSUALG_1:12;
then A4: for x be set 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:119;
f is homogeneous proof let x,y be FinSequence; assume
x in dom f & y in dom f; then len x = n & len y = n by A5,FINSEQ_2:109;
hence len x = len y;
end; then f in {g where g is Element of PFuncs(NAT*,NAT):g is homogeneous};
then reconsider f as Element of HFuncs NAT by Def8;
take f; thus dom f = n-tuples_on NAT by A4,TARSKI:2;
let p be Element of n-tuples_on NAT; p in n-tuples_on NAT; then reconsider
p' = p as Element of NAT* by A3;
thus f.p = f/.p' by A5,FINSEQ_4:def 4 .= (p/.i)+1 by A2,A5;
end;
uniqueness proof let it1, it2 be homogeneous to-naturals from-natural-fseqs
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 set; assume x in n-tuples_on NAT;
then reconsider x' = x as Element of n-tuples_on NAT;
thus it1.x = (x'/.i)+1 by A7 .= it2.x by A9;
end;
hence it1 = it2 by A6,A8,FUNCT_1:9;
end;
end;
theorem Th37:
n succ i in HFuncs NAT
proof set X=NAT; set f=n succ i;
A1: dom f c= NAT* by Def2;
rng f c= NAT by SEQM_3:def 8;
then f is PartFunc of X*, X by A1,RELSET_1:11;
then f is Element of PFuncs(X*, X) by PARTFUN1:119;
then f in {g where g is Element of PFuncs(X*, X): g is homogeneous};
hence thesis by Def8;
end;
definition
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 Def10;
(n succ i) is len-total proof let x, y be FinSequence of NAT; assume
A2: len x = len y & x in dom (n succ i); then len x = n by A1,FINSEQ_2:109
;
then y is Element of n-tuples_on NAT by A2,FINSEQ_2:110;
hence y in dom (n succ i) by A1;
end; hence thesis by A1,RELAT_1:60;
end;
end;
theorem Th38:
arity (n succ i) = n
proof
A1: dom (n succ i) = n-tuples_on NAT by Def10; consider d being set such that
A2: d in dom (n succ i) by XBOOLE_0:def 1;
reconsider d as Element of n-tuples_on NAT by A2,Def10;
A3: d in dom (n succ i) by A2;
for y be FinSequence st y in dom (n succ i) holds n= len y by A1,FINSEQ_2:
109;
hence arity (n succ i) = n by A3,Def5;
end;
definition
let n,i be Nat;
func n proj i -> homogeneous to-naturals from-natural-fseqs Function equals
:Def11: proj(n|->NAT, i);
correctness proof
A1: dom proj(n|->NAT, i) = product(n|->NAT) by PRALG_3:def 2
.= n-tuples_on NAT by FUNCT_6:9;
A2: HFuncs NAT = {f where f is Element of PFuncs(NAT*, NAT): f is homogeneous}
by Def8;
now set P = proj(n|->NAT, i);
A3: P is homogeneous proof let x,y be FinSequence such that
A4: x in dom P & y in dom P;
thus len x = n by A1,A4,FINSEQ_2:109 .= len y by A1,A4,FINSEQ_2:109;
end;
A5: dom P c= NAT* by A1,MSUALG_1:12;
rng P c= NAT proof let x be set; assume x in rng P;
then consider d being set such that
A6: d in dom P & x = P.d by FUNCT_1:def 5;
reconsider d as Element of n-tuples_on NAT by A1,A6;
reconsider d as FinSequence of NAT;
A7: P.d = d.i by A6,PRALG_3:def 2;
i in dom d or not i in dom d;
then d.i in rng d & rng d c= NAT or d.i = {}
by FINSEQ_1:def 4,FUNCT_1:12,def 4;
hence x in NAT by A6,A7,CARD_1:51;
end; then reconsider P as PartFunc of NAT*, NAT by A5,RELSET_1:11;
P is Element of PFuncs(NAT*, NAT) by PARTFUN1:119;
then P in HFuncs NAT by A2,A3;
hence proj(n|->NAT, i) is Element of HFuncs NAT;
end;
hence thesis;
end;
end;
theorem Th39:
n proj i in HFuncs NAT proof set X=NAT; set f=n proj i;
A1: dom f c= NAT* by Def2;
rng f c= NAT by SEQM_3:def 8;
then f is PartFunc of X*, X by A1,RELSET_1:11;
then f is Element of PFuncs(X*, X) by PARTFUN1:119;
then f in {g where g is Element of PFuncs(X*, X): g is homogeneous};
hence thesis by Def8;
end;
theorem Th40:
dom (n proj i) = n-tuples_on NAT &
(1 <= i & i <= n implies rng (n proj i) = NAT)
proof
A1: n proj i = proj(n|->NAT, i) by Def11;
hence
A2: dom (n proj i)= product(n|->NAT) by PRALG_3:def 2
.= n-tuples_on NAT by FUNCT_6:9;
assume
A3: 1 <= i & i <= n;
now let x be set;
hereby assume x in rng (n proj i); then consider d being set such that
A4: d in dom (n proj i) & x = (n proj i).d by FUNCT_1:def 5;
reconsider d as Element of n-tuples_on NAT by A2,A4;
reconsider d as FinSequence of NAT;
A5: (n proj i).d = d.i by A1,A4,PRALG_3:def 2;
len d = n by FINSEQ_2:109; then i in dom d by A3,FINSEQ_3:27;
then d.i in rng d & rng d c= NAT by FINSEQ_1:def 4,FUNCT_1:12;
hence x in NAT by A4,A5;
end;
assume x in NAT; then reconsider x' = x as Nat;
reconsider d = n |-> x' as FinSequence of NAT by FINSEQ_2:77;
A6: d is Element of n-tuples_on NAT by FINSEQ_2:132;
then A7: (n proj i).d = d.i by A1,A2,PRALG_3:def 2;
i in Seg n by A3,FINSEQ_1:3; then d.i = x' by FINSEQ_2:70;
hence x in rng (n proj i) by A2,A6,A7,FUNCT_1:def 5;
end; hence thesis by TARSKI:2;
end;
definition
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 Th40;
n proj i is len-total proof let x, y be FinSequence of NAT; assume
A2: len x=len y & x in dom (n proj i); then len x=n by A1,FINSEQ_2:109;
then y is Element of n-tuples_on NAT by A2,FINSEQ_2:110;
hence y in dom (n proj i) by A1;
end;
hence thesis by A1,RELAT_1:60;
end;
end;
theorem Th41:
arity (n proj i) = n
proof
A1: dom (n proj i) = n-tuples_on NAT by Th40; consider d being set such that
A2: d in n-tuples_on NAT by XBOOLE_0:def 1;
reconsider d as Element of n-tuples_on NAT by A2;
A3: d in dom (n proj i) by A1;
for x be FinSequence st x in dom (n proj i) holds n= len x
by A1,FINSEQ_2:109;
hence arity (n proj i) = n by A3,Def5;
end;
theorem Th42:
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;
A1: dom (n proj i) = n-tuples_on NAT by Th40;
(n proj i) = proj(n|->NAT, i) by Def11;
hence (n proj i).t = t.i by A1,PRALG_3:def 2;
end;
definition let X be set;
cluster HFuncs X -> functional;
coherence;
end;
theorem Th43:
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;
per cases;
suppose A3: F is empty; reconsider f ={} as Element of HFuncs Y by Th30;
take f; thus f = Union F by A3,PROB_1:def 3,RELAT_1:60,ZFMISC_1:2;
thus dom f c= n-tuples_on Y by RELAT_1:60,XBOOLE_1:2;
thus thesis;
suppose A4: F <> {};
A5: Union F = union rng F by PROB_1:def 3;
A6: rng F is functional proof let x be set; assume
A7: x in rng F; rng F c= HFuncs Y by RELSET_1:12;
then x is Element of HFuncs Y by A7;
hence thesis;
end; then reconsider f = Union F as Function by A1,A5,Th14;
reconsider rngF = rng F as non empty functional compatible set by A1,A4,A6,
RELAT_1:64;
set D = {dom g where g is Element of rngF: not contradiction};
A8: dom f c= n-tuples_on Y proof let x be set; assume x in dom f;
then x in union D by A5,Th15; then consider d being set such that
A9: x in d & d in D by TARSKI:def 4;
consider g being Element of rngF such that
A10: d = dom g & not contradiction by A9; consider e being set such that
A11: e in dom F & F.e = g by FUNCT_1:def 5;
reconsider e as Element of X by A11;
dom (F.e) c= n-tuples_on Y by A2;
hence x in n-tuples_on Y by A9,A10,A11;
end;
n-tuples_on Y c= Y* by MSUALG_1:12;
then A12: dom f c= Y* by A8,XBOOLE_1:1;
rng f c= Y proof let y be set; assume y in rng f;
then consider x being set such that
A13: x in dom f & f.x = y by FUNCT_1:def 5;
x in union D by A5,A13,Th15; then consider d being set such that
A14: x in d & d in D by TARSKI:def 4;
consider g being Element of rngF such that
A15: d = dom g & not contradiction by A14;
g in rngF & rng F c= HFuncs Y by RELSET_1:12;
then reconsider g as Element of HFuncs Y;
A16: f.x = g.x by A5,A14,A15,Th16;
A17: rng g c= Y by RELSET_1:12; g.x in rng g by A14,A15,FUNCT_1:12;
hence y in Y by A13,A16,A17;
end; then reconsider f as PartFunc of Y*, Y by A12,RELSET_1:11;
reconsider f as Element of PFuncs(Y*, Y) by PARTFUN1:119;
f is homogeneous proof let x,y be FinSequence; assume
x in dom f&y in dom f;
then len x = n & len y = n by A8,FINSEQ_2:109;
hence len x = len y;
end; 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 by Def8;
take f; thus f = Union F; thus dom f c= n-tuples_on Y by A8;
end;
theorem
for F being Function of NAT, HFuncs D
st for i holds F.i c= F.(i+1) holds Union F in HFuncs D
proof set X = D; let F be Function of NAT, HFuncs X such that
A1: for i being Nat holds F.i c= F.(i+1);
A2: Union F = union rng F by PROB_1:def 3;
rng F c= HFuncs X & dom F = NAT by FUNCT_2:def 1,RELSET_1:12;
then F.0 in rng F by FUNCT_1:12;
then reconsider Y = rng F as non empty Subset of HFuncs X by RELSET_1:12;
A3: Y is PartFunc-set of X*, X
proof
let f be Element of Y; f is Element of HFuncs X; hence thesis;
end;
A4: now let n be Nat;
defpred p[Nat] means F.n c= F.(n+$1);
A5: p[0];
A6: now let i be Nat such that
A7: p[i]; F.(n+i) c= F.(n+i+1) by A1;
then F.n c= F.(n+i+1) by A7,XBOOLE_1:1;
hence p[i+1] by XCMPLX_1:1;
end;
A8: for i being Nat holds p[i] from Ind(A5,A6);
let m be Nat; assume n <= m; then ex i being Nat st m = n+i by NAT_1:28;
hence F.n c= F.m by A8;
end;
A9: Y is compatible proof let f,g be Function; assume f in Y;
then consider i being set such that
A10: i in dom F & f = F.i by FUNCT_1:def 5;
assume g in Y; then consider j being set such that
A11: j in dom F & g = F.j by FUNCT_1:def 5;
reconsider i,j as Nat by A10,A11;
i <= j or j <= i; then f c= g or g c= f by A4,A10,A11;
hence f tolerates g by PARTFUN1:135;
end; then Union F is PartFunc of X*, X by A2,A3,Th18;
then reconsider f = Union F as Element of PFuncs(X*, X) by PARTFUN1:119;
A12: dom f=union {dom g where g is Element of Y: not contradiction} by A2,A9,
Th15;
f is homogeneous proof let x,y be FinSequence; assume x in dom f;
then consider A1 being set such that
A13: x in A1 & A1 in {dom g where g is Element of Y: not contradiction}
by A12,TARSKI:def 4; consider g1 being Element of Y such that
A14: A1 = dom g1 by A13;
assume y in dom f; then consider A2 being set such that
A15: y in A2 & A2 in {dom g where g is Element of Y: not contradiction}
by A12,TARSKI:def 4; consider g2 being Element of Y such that
A16: A2 = dom g2 by A15; consider i1 being set such that
A17: i1 in dom F & g1 = F.i1 by FUNCT_1:def 5;
consider i2 being set such that
A18: i2 in dom F & g2 = F.i2 by FUNCT_1:def 5;
reconsider i1, i2 as Nat by A17,A18;
i1 <= i2 or i2 <= i1; then g1 c= g2 or g2 c= g1 by A4,A17,A18;
then dom g1 c= dom g2 or dom g2 c= dom g1 by GRFUNC_1:8;
hence thesis by A13,A14,A15,A16,Def4;
end; then f in {g where g is Element of PFuncs(X*, X): g is homogeneous};
hence thesis by Def8;
end;
theorem Th45:
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 let x be set such that
A1: x in dom <:F:>;
A2: dom <:F:> = meet doms F by FUNCT_6:49
.= meet rng doms F by FUNCT_6:def 4;
A3: dom doms F=F"SubFuncs rng F by FUNCT_6:def 2; consider y being set such
that
A4: y in rng doms F by A1,A2,SETFAM_1:2,XBOOLE_0:def 1; consider z being set
such that
A5: z in dom doms F & (doms F).z = y by A4,FUNCT_1:def 5;
z in dom F by A3,A5,FUNCT_6:28;
then A6: F.z in rng F & rng F c= HFuncs X by FUNCT_1:12,RELSET_1:12;
then reconsider Fz = F.z as Element of HFuncs X;
A7: (doms F).z = proj1(F.z) by A3,A5,FUNCT_6:def 2 .= dom Fz by FUNCT_5:21;
A8: x in y by A1,A2,A4,SETFAM_1:def 1;
dom Fz c= (arity Fz)-tuples_on X by Th23;
then x in (arity Fz)-tuples_on X by A5,A7,A8;
hence x in (arity F)-tuples_on X by A6,Def7;
end;
end;
definition
let X be non empty set;
let F be with_the_same_arity FinSequence of HFuncs X;
cluster <:F:> -> homogeneous;
coherence proof let x,y be FinSequence such that
A1: x in dom <:F:> & y in dom <:F:>;
dom <:F:> c= (arity F)-tuples_on X by Th45;
then len x = arity F & len y = arity F by A1,FINSEQ_2:109;
hence len x = len y;
end;
end;
theorem Th46:
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;
dom (f*<:F:>) c=dom <:F:>&dom <:F:> c=(arity F)-tuples_on X by Th45,RELAT_1:
44
;
hence A1: dom (f*<:F:>) c= (arity F)-tuples_on X by XBOOLE_1:1;
(arity F)-tuples_on X c= X* by MSUALG_1:12;
then A2: dom (f*<:F:>) c= X* by A1,XBOOLE_1:1;
rng (f*<:F:>) c= rng f & rng f c= X by RELAT_1:45,RELSET_1:12;
hence rng (f*<:F:>) c= X by XBOOLE_1:1;
then f*<:F:> is PartFunc of X*, X by A2,RELSET_1:11;
then f*<:F:> in PFuncs(X*, X) by PARTFUN1:119;
then f*<:F:> in {g where g is Element of PFuncs(X*, X): g is homogeneous}
;
hence f*<:F:> in HFuncs X by Def8;
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;
coherence proof let f be Element of S; thus f is Element of P; end;
end;
definition
let f be homogeneous from-natural-fseqs Function;
cluster <*f*> -> with_the_same_arity;
coherence proof let h,g be Function such that
A1: h in rng <*f*> & g in rng <*f*>; rng <*f*> = {f} by FINSEQ_1:56;
then A2: h = f & g = f by A1,TARSKI:def 1;
hence h is empty implies g is empty or dom g = {{}};
assume h is non empty & g is non empty; take i = arity f,NAT;
thus dom h c= i-tuples_on NAT & dom g c= i-tuples_on NAT by A2,Th24;
end;
end;
theorem
for f being homogeneous to-naturals from-natural-fseqs Function
holds arity <*f*> = arity f
proof let f be homogeneous to-naturals from-natural-fseqs Function;
rng <*f*> = {f} by FINSEQ_1:55; then f in rng <*f*> by TARSKI:def 1;
hence arity <*f*> = arity f by Def7;
end;
theorem Th48:
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 such that
A1: g = f*<:F:>;
A2: dom g c= (arity F)-tuples_on NAT by A1,Th46;
consider x being set such that
A3: x in dom g by XBOOLE_0:def 1;
reconsider x as Element of (arity F)-tuples_on NAT by A2,A3;
len x = arity F by FINSEQ_2:109;
hence arity g = arity F by A3,Def5;
end;
theorem Th49:
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 & F is non empty and
A2: for h being Element of HFuncs X st h in rng F
holds h is quasi_total non empty;
A3: HFuncs X={h where h is Element of PFuncs(X*,X):h is homogeneous} by Def8;
set fF = f*<:F:>; set n = arity F;
A4: dom fF c= n-tuples_on X by Th46;
A5: n-tuples_on X c= dom fF proof let x be set; assume
A6: x in n-tuples_on X;
A7: n-tuples_on X c= dom <:F:> proof let x be set; assume
A8: x in n-tuples_on X;
A9: dom <:F:> = meet doms F by FUNCT_6:49
.= meet rng doms F by FUNCT_6:def 4;
dom F <> {} by A1,RELAT_1:64; then consider z being set such that
A10: z in dom F by XBOOLE_0:def 1;
F.z in rng F&rng F c=HFuncs X by A10,FINSEQ_1:def 4,FUNCT_1:12;
then A11: F.z is Element of HFuncs X;
A12: dom doms F = F"SubFuncs rng F by FUNCT_6:def 2;
then z in dom doms F by A10,A11,FUNCT_6:28;
then A13: rng doms F <> {} by RELAT_1:65;
now let y be set; assume y in rng doms F;
then consider w being set such that
A14: w in dom doms F & (doms F).w = y by FUNCT_1:def 5;
A15: w in dom F by A12,A14,FUNCT_6:28;
then reconsider Fw = F.w as Element of HFuncs X by FINSEQ_2:13;
A16: (doms F).w = proj1(F.w) by A12,A14,FUNCT_6:def 2
.= dom (Fw) by FUNCT_5:21;
A17: Fw in rng F by A15,FUNCT_1:12;
then Fw is non empty quasi_total by A2;
then dom (Fw) = (arity Fw)-tuples_on X by Th25;
hence x in y by A8,A14,A16,A17,Def7;
end; hence x in dom <:F:> by A9,A13,SETFAM_1:def 1;
end;
A18: dom f = (arity f)-tuples_on X by Th25;
A19: rng <:F:> c= product rngs F by FUNCT_6:49;
product rngs F c= (len F)-tuples_on X proof let p be set; assume
p in product rngs F; then consider g being Function such that
A20: p = g & dom g = dom rngs F and
A21: for x being set st x in dom rngs F holds g.x in (rngs F).x
by CARD_3:def 5;
A22: dom rngs F = F"SubFuncs rng F by FUNCT_6:def 3;
now let x be set;
hereby assume x in F"SubFuncs rng F;
then x in dom F & dom F = Seg len F by FINSEQ_1:def 3,FUNCT_6:28
;
hence x in Seg len F;
end; assume x in Seg len F;
then A23: x in dom F by FINSEQ_1:def 3;
then F.x in rng F & rng F c= HFuncs X by FINSEQ_1:def 4,FUNCT_1
:12;
then F.x is Element of HFuncs X;
hence x in F"SubFuncs rng F by A23,FUNCT_6:28;
end;
then A24: F"SubFuncs rng F = Seg len F by TARSKI:2;
then reconsider g as FinSequence by A20,A22,FINSEQ_1:def 2;
rng g c= X proof let x be set; assume
x in rng g; then consider d being set such that
A25: d in dom g & g.d = x by FUNCT_1:def 5;
A26: g.d in (rngs F).d by A20,A21,A25;
dom F = Seg len F by FINSEQ_1:def 3;
then reconsider Fd = F.d as Element of HFuncs X by A20,A22,A24,A25
,FINSEQ_2:13;
A27: (rngs F).d = proj2(F.d) by A20,A22,A25,FUNCT_6:def 3
.= rng Fd by FUNCT_5:21;
rng Fd c= X by RELSET_1:12;
hence x in X by A25,A26,A27;
end; then reconsider g as FinSequence of X by FINSEQ_1:def 4;
len g = len F by A20,A22,A24,FINSEQ_1:def 3;
then p is Element of (len F)-tuples_on X by A20,FINSEQ_2:110;
hence p in (len F)-tuples_on X;
end; then <:F:>.x in rng <:F:> & rng <:F:> c= (len F)-tuples_on X
by A6,A7,A19,FUNCT_1:12,XBOOLE_1:1;
hence x in dom fF by A1,A6,A7,A18,FUNCT_1:21;
end;
then A28: dom fF = n-tuples_on X by A4,XBOOLE_0:def 10;
(arity F)-tuples_on X c= X* by MSUALG_1:12;
then A29: dom fF c= X* by A4,XBOOLE_1:1;
rng fF c= X by Th46; then fF is Relation of X*, X by A29,RELSET_1:11;
then fF is Element of PFuncs(X*, X) by PARTFUN1:119;
then fF in HFuncs X by A3; then reconsider fF as Element of HFuncs X;
fF is quasi_total proof let x, y be FinSequence of X such that
A30: len x = len y & x in dom fF; len x = n by A4,A30,FINSEQ_2:109;
then y is Element of n-tuples_on X by A30,FINSEQ_2:110;
hence y in dom fF by A28;
end; hence f*<:F:> is non empty quasi_total Element of HFuncs X by A4,A5,
RELAT_1:60,XBOOLE_0:def 10;
thus dom (f*<:F:>) = (arity F)-tuples_on D by A4,A5,XBOOLE_0:def 10;
end;
theorem Th50:
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;
set fF = f*<:F:>;
reconsider g = {} as PartFunc of X*, X by PARTFUN1:56;
g in PFuncs(X*, X) by PARTFUN1:119;
then A3: g in {h where h is Element of PFuncs(X*, X): h is homogeneous};
A4: g is quasi_total proof let x, y be FinSequence of X;
assume len x = len y & x in dom g;
hence y in dom g by RELAT_1:60;
end;
then A5: g is quasi_total Element of HFuncs X by A3,Def8;
per cases;
suppose f = {}; hence thesis by RELAT_1:62;
suppose F = {}; then fF = f*{} by FUNCT_6:60; hence thesis by A3,A4,Def8;
suppose ex h being set st h in rng F & h = {}; then <:F:> = {} by Th10; hence
thesis by A5,RELAT_1:62;
suppose A6: 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 f*<:F:> is quasi_total Element of HFuncs X by A1,A6,Th49;
end;
theorem Th51:
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
A1: arity f = 0 & arity g = 0 & f.{} = g.{};
now thus dom f = 0-tuples_on X by A1,Th25 .= {<*>X} by FINSEQ_2:112;
thus dom g = 0-tuples_on X by A1,Th25 .= {<*>X} by FINSEQ_2:112;
let x be set; assume x in {<*>X}; then x = {} by TARSKI:def 1;
hence f.x = g.x by A1;
end; hence f = g by FUNCT_1:9;
end;
theorem Th52:
for f,g being non empty len-total homogeneous to-naturals
(from-natural-fseqs 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
(from-natural-fseqs Function); assume
A1: arity f = 0 & arity g = 0 & f.{} = g.{};
f is non empty quasi_total Element of HFuncs NAT &
g is non empty quasi_total Element of HFuncs NAT by Th32;
hence f = g by A1,Th51;
end;
begin :: Primitive recursiveness
reserve f1, f2 for non empty homogeneous to-naturals from-natural-fseqs
Function,
e1, e2 for homogeneous to-naturals from-natural-fseqs Function,
p for Element of (arity f1+1)-tuples_on NAT;
definition
let g, f1, f2 be homogeneous to-naturals from-natural-fseqs Function,
i be Nat;
pred g is_primitive-recursively_expressed_by f1,f2,i means:Def12:
ex n being Nat st dom g c= n-tuples_on NAT & i >= 1 & i <= n &
(arity f1)+1 = n & n+1 = arity f2 &
for p being FinSequence of NAT st len p = n
holds
(p+*(i,0) in dom g iff Del(p,i) in dom f1) &
(p+*(i,0) in dom g implies g.(p+*(i,0)) = f1.Del(p,i)) &
for n being Nat holds
(p+*(i,n+1) in dom g iff
p+*(i,n) in dom g & (p+*(i,n))^<*g.(p+*(i,n))*> in dom f2) &
(p+*(i,n+1) in dom g implies
g.(p+*(i,n+1)) = f2.((p+*(i,n))^<*g.(p+*(i,n))*>));
end;
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 from-natural-fseqs Function;
reconsider ff1 = f1, ff2 = f2 as Element of HFuncs NAT by Th31;
let i be Nat;
let p be FinSequence of NAT;
func primrec(f1,f2,i,p) -> Element of HFuncs NAT means:Def13:
ex F being Function of NAT, HFuncs NAT st it = F.(p/.i) &
(i in dom p & Del(p,i) in dom f1 implies
F.0 = {p+*(i,0)} --> (f1.Del(p,i))) &
(not i in dom p or not Del(p,i) in dom f1 implies F.0 = {}) &
for m being 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 set n = len p;
A1: HFuncs NAT = {f where f is Element of PFuncs(NAT*, NAT): f is homogeneous}
by Def8;
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:37;
Del(p,i) in dom f1 or not Del(p,i) in dom f1;
then ff1.Del(p,i) = ff1/.Del(p,i) or ff1.Del(p,i) = {}
by FINSEQ_4:def 4,FUNCT_1:def 4;
then reconsider z = ff1.Del(p,i) as Nat by CARD_1:51;
{} is PartFunc of NAT*, NAT &
Ap --> z is PartFunc of NAT*, NAT by PARTFUN1:56;
then Ap --> z = {p+*(i,0)} --> z & Ap --> z in PFuncs(NAT*, NAT) &
{} in PFuncs(NAT*, NAT) by PARTFUN1:119;
then Ap --> z in HFuncs NAT & {} in HFuncs NAT by A1;
then reconsider t = Ap --> z, e = {} as Element of HFuncs NAT;
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) &
(not i in dom p or not Del(p,i) in dom f1 implies A = e);
defpred A[Nat,Element of HFuncs NAT, Element of HFuncs NAT] means
Q[$1, $2, $3, p, i, ff2];
A3: 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;
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
A4: 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;
set f= x+*({p+*(i,m+1)} --> f2.((p+*(i,m))^<*x.(p+*(i,m))*>));
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:37;
(p+*(i,m))^<*x.(p+*(i,m))*> in dom f2 or
not (p+*(i,m))^<*x.(p+*(i,m))*> in dom f2;
then ff2.((p+*(i,m))^<*x.(p+*(i,m))*>) in rng ff2 & rng ff2 c= NAT or
ff2.((p+*(i,m))^<*x.(p+*(i,m))*>) = {}
by FUNCT_1:12,def 4,RELSET_1:12;
then reconsider z = ff2.((p+*(i,m))^<*x.(p+*(i,m))*>) as Nat by CARD_1:51;
dom p = dom (p+*(i,m+1)) by FUNCT_7:32;
then len (p+*(i,m+1)) = n by FINSEQ_3:31;
then p+*(i,m+1) is Element of n-tuples_on NAT by FINSEQ_2:110;
then A5: B c= n-tuples_on NAT by ZFMISC_1:37;
dom (B --> z) = B by FUNCOP_1:19;
then A6: f = x+*(B --> z) & dom f = dom x \/ B by FUNCT_4:def 1;
now assume
A7: p+*(i,m) in dom x;
dom x c= n-tuples_on NAT proof let a be set; assume
A8: a in dom x; then reconsider q = a as Element of NAT*;
A9: len q = len (p+*(i,m)) by A7,A8,Def4;
dom p = dom (p+*(i,m)) by FUNCT_7:32;
then len q = n by A9,FINSEQ_3:31;
then q is Element of n-tuples_on NAT by FINSEQ_2:110;
hence thesis;
end;
then f is PartFunc of NAT*, NAT & dom f c= n-tuples_on NAT
by A5,A6,FUNCT_4:41,XBOOLE_1:8;
then f in PFuncs(NAT*, NAT) & f is homogeneous by Th19,PARTFUN1:119;
hence f in HFuncs NAT by A1;
end; then reconsider y as Element of HFuncs NAT by A4;
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 A4;
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 A4;
end;
consider FF being Function of NAT, HFuncs NAT such that
A10: FF.0 = A and
A11: for m being Nat holds A[m,FF.m,FF.(m+1)] from RecExD(A3);
take FF.(p/.i), FF; thus thesis by A2,A10,A11;
end;
uniqueness proof let g1,g2 be Element of HFuncs NAT;
given F1 being Function of NAT, HFuncs NAT such that
A12: g1 = F1.(p/.i) and
A13: i in dom p & Del(p,i) in dom f1
implies F1.0 = {p+*(i,0)} --> (f1.Del(p,i)) and
A14: not i in dom p or not Del(p,i) in dom f1 implies F1.0 = {} and
A15: for m being Nat holds Q[m, F1.m, F1.(m+1), p, i , f2];
given F2 being Function of NAT, HFuncs NAT such that
A16: g2 = F2.(p/.i) and
A17: i in dom p & Del(p,i) in dom f1
implies F2.0 = {p+*(i,0)} --> (f1.Del(p,i)) and
A18: not i in dom p or not Del(p,i) in dom f1 implies F2.0 = {} and
A19: for m being Nat holds Q[m, F2.m, F2.(m+1), p, i , f2];
defpred p[Nat] means F1.$1 = F2.$1;
A20: p[0] by A13,A14,A17,A18;
A21: now let m be Nat; assume p[m];
then Q[m,F1.m,F1.(m+1),p,i,f2] & Q[m, F1.m, F2.(m+1), p, i , ff2] by A15,
A19;
hence p[m+1];
end; for m being Nat holds p[m] from Ind(A20,A21);
hence g1 = g2 by A12,A16;
end;
end;
theorem Th53:
for p, q being FinSequence of NAT
st q in dom primrec(e1,e2,i,p) ex k st q = p+*(i,k)
proof 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 Function of NAT, 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, F.(m+1), p, i, f2] by Def13;
defpred p[Nat] means q in dom (F.$1) implies ex k being Nat st q = p+*(i,k);
A6: p[0] proof assume
A7: 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,FUNCOP_1:19;
then p+*(i,0) = q by A7,TARSKI:def 1;
hence ex k being Nat st q = p+*(i,k);
suppose not i in dom p or not Del(p,i) in dom f1;
hence ex k being Nat st q = p+*(i,k) by A4,A7,RELAT_1:60;
end;
A8: for m be Nat st p[m] holds p[m+1] proof let m be Nat such that
A9: p[m] and
A10: 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 A11: dom (F.(m+1)) = dom (F.m) \/ {p+*(i,m+1)} by FUNCOP_1:19;
thus ex k being Nat st q = p+*(i,k) proof
per cases by A10,A11,XBOOLE_0:def 2;
suppose q in dom (F.m); hence ex k being Nat st q = p+*(i,k) by A9;
suppose q in {p+*(i,m+1)}; then q = p+*(i,m+1) by TARSKI:def 1;
hence ex k being Nat st q = p+*(i,k);
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 ex k being Nat st q = p+*(i,k) by A5,A9,A10;
end;
for n being Nat holds p[n] from Ind(A6,A8);
hence ex k being Nat st q = p+*(i,k) by A1,A2;
end;
theorem Th54:
for p being FinSequence of NAT st not i in dom p holds primrec(e1,e2,i,p) = {}
proof set f1 = e1, f2 = e2; let p be FinSequence of NAT; assume
A1: not i in dom p; consider F being Function of NAT, HFuncs NAT such that
A2: 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
A3: (not i in dom p or not Del(p,i) in dom f1 implies F.0 = {}) and
A4: for m being Nat holds Q[m, F.m, F.(m+1), p, i, f2] by Def13;
defpred p[Nat] means F.$1 = {};
A5: p[0] by A1,A3;
A6: for m be Nat st p[m] holds p[m+1] by A1,A4;
for m being Nat holds p[m] from Ind(A5, A6);
hence primrec(f1,f2,i,p) = {} by A2;
end;
theorem Th55:
for p, q being FinSequence of NAT holds
primrec(e1,e2,i,p) tolerates primrec(e1,e2,i,q)
proof 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 Th54;
hence thesis by PARTFUN1:141;
suppose A1: i in dom p1 & i in dom p2;
consider F1 being Function of NAT, HFuncs NAT such that
A2: primrec(f1,f2,i,p1) = F1.(p1/.i) and
A3: (i in dom p1 & Del(p1,i) in dom f1
implies F1.0 = {p1+*(i,0)} --> (f1.Del(p1,i))) and
A4: (not i in dom p1 or not Del(p1,i) in dom f1 implies F1.0 = {}) and
A5: for m being Nat holds Q[m, F1.m, F1.(m+1), p1, i, f2] by Def13;
consider F2 being Function of NAT, HFuncs NAT such that
A6: primrec(f1,f2,i,p2) = F2.(p2/.i) and
A7: (i in dom p2 & Del(p2,i) in dom f1
implies F2.0 = {p2+*(i,0)} --> (f1.Del(p2,i))) and
A8: (not i in dom p2 or not Del(p2,i) in dom f1 implies F2.0 = {}) and
A9: for m being Nat holds Q[m, F2.m, F2.(m+1), p2, i, f2] by Def13;
defpred p[Nat] means for x being set st x in dom (F1.$1)
ex n being Nat st x = p1+*(i,n) & n <= $1;
A10: p[0] proof let x be set such that
A11: x in dom (F1.0);
dom (F1.0) = {p1+*(i,0)} by A3,A4,A11,FUNCOP_1:19,RELAT_1:60;
then x = p1+*(i,0) by A11,TARSKI:def 1;
hence ex n being Nat st x = p1+*(i,n) & n <= 0;
end;
A12: now let m be Nat such that
A13: p[m];
thus p[m+1] proof
let x be set such that
A14: x in dom (F1.(m+1));
A15: m <= m+1 by NAT_1:29; set p1c = (p1+*(i,m))^<*(F1.m).(p1+*(i,m))*>;
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 A5;
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)} by FUNCOP_1:19;
then A16: x in dom (F1.m) or x in {p1+*(i,m+1)} by A14,XBOOLE_0:def 2;
thus ex n being Nat st x = p1+*(i,n) & n <= m+1 proof
per cases by A16,TARSKI:def 1;
suppose x in dom (F1.m); then consider n being Nat such that
A17: x = p1+*(i,n) & n <= m by A13; n <= m+1 by A15,A17,AXIOMS:22;
hence thesis by A17;
suppose x = p1+*(i,m+1); hence thesis;
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 A5;
then consider n being Nat such that
A18: x = p1+*(i,n) & n <= m by A13,A14; n <= m+1 by A15,A18,AXIOMS:22;
hence ex n being Nat st x = p1+*(i,n) & n <= m+1 by A18;
end;
end;
A19: for m being Nat holds p[m] from Ind(A10, A12);
defpred p[Nat] means for x being set st x in dom (F2.$1)
ex n being Nat st x = p2+*(i,n) & n <= $1;
A20: p[0] proof let x be set such that
A21: x in dom (F2.0);
dom (F2.0) = {p2+*(i,0)} by A7,A8,A21,FUNCOP_1:19,RELAT_1:60;
then x = p2+*(i,0) by A21,TARSKI:def 1;
hence ex n being Nat st x = p2+*(i,n) & n <= 0;
end;
A22: now let m be Nat such that
A23: p[m];
thus p[m+1]
proof let x be set such that
A24: x in dom (F2.(m+1));
A25: m <= m+1 by NAT_1:29; set p2c = (p2+*(i,m))^<*(F2.m).(p2+*(i,m))*>;
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 A9;
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)} by FUNCOP_1:19;
then A26: x in dom (F2.m) or x in {p2+*(i,m+1)} by A24,XBOOLE_0:def 2;
thus ex n being Nat st x = p2+*(i,n) & n <= m+1 proof
per cases by A26,TARSKI:def 1;
suppose x in dom (F2.m); then consider n being Nat such that
A27: x = p2+*(i,n) & n <= m by A23; n <= m+1 by A25,A27,AXIOMS:22;
hence thesis by A27;
suppose x = p2+*(i,m+1); hence thesis;
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 A9;
then consider n being Nat such that
A28: x = p2+*(i,n) & n <= m by A23,A24; n <= m+1 by A25,A28,AXIOMS:22;
hence ex n being Nat st x = p2+*(i,n) & n <= m+1 by A28;
end;
end;
A29: for m being Nat holds p[m] from Ind(A20, A22);
A30: for m being Nat holds F1.m = F2.m or dom (F1.m) /\ dom (F2.m) = {} proof
A31: now assume A32: p1+*(i,0) = p2+*(i,0);
defpred r[Nat] means F1.$1 = F2.$1;
A33: r[0] proof
per cases;
suppose i in dom p1 & Del(p1,i) in dom f1;
hence thesis by A1,A3,A7,A32,Th7;
suppose not i in dom p1 or not Del(p1, i) in dom f1;
hence thesis by A1,A4,A8,A32,Th7;
end;
A34: now let m be Nat such that
A35: r[m];
A36: p1+*(i,m) = p2+*(i,m) & p1+*(i,m+1) = p2+*(i,m+1) by A32,Th5;
A37: Q[m, F1.m, F1.(m+1), p1, i, f2] by A5;
Q[m, F2.m, F2.(m+1), p2, i, f2] by A9;
hence r[m+1] by A1,A35,A36,A37;
end;
thus for m being Nat holds r[m] from Ind(A33, A34);
end;
now assume A38: p1+*(i,0) <> p2+*(i,0);
let m be Nat; assume dom (F1.m) /\ dom (F2.m) <> {};
then consider x being set such that
A39: x in dom(F1.m) /\ dom(F2.m) by XBOOLE_0:def 1;
A40: x in dom(F1.m) & x in dom(F2.m) by A39,XBOOLE_0:def 3;
then consider n1 being Nat such that
A41: x = p1+*(i,n1) & n1 <= m by A19;
consider n2 being Nat such that
A42: x = p2+*(i,n2) & n2 <= m by A29,A40;
thus contradiction by A38,A41,A42,Th5;
end;
hence thesis by A31;
end;
A43: 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);
A44: r[0];
A45: now let n be Nat such that
A46: r[n]; set k = m+n;
F1.k qua set c= F1.(k+1) qua set proof let x be set such that
A47: x in F1.k; set p1c = (p1+*(i,k))^<*(F1.k).(p1+*(i,k))*>;
per cases;
suppose i in dom p1 & p1+*(i,k) in dom (F1.k) & p1c in dom f2;
then A48: F1.(k+1) = (F1.k)+*({p1+*(i,k+1)}--> f2.(p1c)) by A5;
dom (F1.k) misses dom ({p1+*(i,k+1)}--> f2.(p1c))
proof
assume not thesis; then consider x being set such that
A49: x in dom (F1.k) /\
dom({p1+*(i,k+1)}--> f2.(p1c)) by XBOOLE_0:4;
A50: x in dom (F1.k) & x in dom({p1+*(i,k+1)}--> f2.(p1c))
by A49,XBOOLE_0:def 3;
then x in dom (F1.k) & x in {p1+*(i,k+1)} by FUNCOP_1:19;
then A51: x in dom (F1.k) & x = p1+*(i,k+1) by TARSKI:def 1;
consider n1 being Nat such that
A52: x = p1+*(i,n1) & n1 <= k by A19,A50;
n1 = (p1+*(i,n1)).i & k+1 = (p1+*(i,k+1)).i by A1,FUNCT_7:33;
hence contradiction by A51,A52,NAT_1:38;
end; then F1.k c= F1.(k+1) by A48,FUNCT_4:33;
hence x in F1.(k+1) by A47;
suppose not i in dom p1 or not p1+*(i,k) in dom (F1.k)
or not p1c in dom f2;
hence x in F1.(k+1) by A5,A47;
end; then F1.m c= F1.((m+n)+1) by A46,XBOOLE_1:1;
hence r[n+1] by XCMPLX_1:1;
end; thus for n being Nat holds r[n] from Ind(A44, A45);
end;
A53: 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);
A54: r[0];
A55: now let n be Nat such that
A56: r[n]; set k = m+n;
F2.k c= F2.(k+1) proof let x be set such that
A57: x in F2.k; set p2c = (p2+*(i,k))^<*(F2.k).(p2+*(i,k))*>;
per cases;
suppose i in dom p2 & p2+*(i,k) in dom (F2.k) & p2c in dom f2;
then A58: F2.(k+1) = (F2.k)+*({p2+*(i,k+1)}--> f2.(p2c)) by A9;
dom (F2.k) misses dom ({p2+*(i,k+1)}--> f2.(p2c))
proof
assume not thesis; then consider x being set such that
A59: x in dom (F2.k) /\
dom({p2+*(i,k+1)}--> f2.(p2c)) by XBOOLE_0:4;
A60: x in dom (F2.k) & x in dom({p2+*(i,k+1)}--> f2.(p2c))
by A59,XBOOLE_0:def 3;
then x in dom (F2.k) & x in {p2+*(i,k+1)} by FUNCOP_1:19;
then A61: x in dom (F2.k) & x = p2+*(i,k+1) by TARSKI:def 1;
consider n2 being Nat such that
A62: x = p2+*(i,n2) & n2 <= k by A29,A60;
n2 = (p2+*(i,n2)).i & k+1 = (p2+*(i,k+1)).i by A1,FUNCT_7:33;
hence contradiction by A61,A62,NAT_1:38;
end; then F2.k c= F2.(k+1) by A58,FUNCT_4:33;
hence x in F2.(k+1) by A57;
suppose not i in dom p2 or not p2+*(i,k) in dom (F2.k)
or not p2c in dom f2;
hence x in F2.(k+1) by A9,A57;
end; then F2.m c= F2.((m+n)+1) by A56,XBOOLE_1:1;
hence r[n+1] by XCMPLX_1:1;
end; thus for n being Nat holds r[n] from Ind(A54, A55);
end;
reconsider m = p1/.i, n = p2/.i as Nat;
reconsider F1m = F1.m, F1n = F1.n, F2m = F2.m, F2n = F2.n
as Element of HFuncs NAT;
thus thesis proof
per cases;
suppose m <= n; then consider k being Nat such that
A63: n = m+k by NAT_1:28;
thus primrec(f1,f2,i,p1) tolerates primrec(f1,f2,i,p2) proof
per cases by A30;
suppose A64: F1n = F2n; F1m c= F1n by A43,A63;
hence thesis by A2,A6,A64,PARTFUN1:140;
suppose dom (F1n) /\ dom (F2n) = {};
then dom (F1n) misses dom (F2n) by XBOOLE_0:def 7;
then A65: F1n tolerates F2n by PARTFUN1:138; F1m c= F1n by A43,A63;
hence thesis by A2,A6,A65,PARTFUN1:140;
end;
suppose m >= n; then consider k being Nat such that
A66: m = n+k by NAT_1:28;
thus primrec(f1,f2,i,p1) tolerates primrec(f1,f2,i,p2) proof
per cases by A30;
suppose A67: F1m = F2m; F2n c= F2m by A53,A66;
hence thesis by A2,A6,A67,PARTFUN1:140;
suppose dom (F1m) /\ dom (F2m) = {};
then dom (F1m) misses dom (F2m) by XBOOLE_0:def 7;
then A68: F1m tolerates F2m by PARTFUN1:138; F2n c= F2m by A53,A66;
hence thesis by A2,A6,A68,PARTFUN1:140;
end;
end;
end;
theorem Th56:
for p being FinSequence of NAT
holds dom primrec(e1,e2,i,p) c= (1+arity e1)-tuples_on NAT
proof set f1 = e1, f2 = e2; let p be FinSequence of NAT;
per cases;
suppose A1: i in dom p;
consider F being Function of NAT, 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, F.(m+1), p, i, f2] by Def13;
defpred p[Nat] means dom (F.$1) c= (1+arity f1)-tuples_on NAT;
A6: p[0] proof
per cases;
suppose A7: Del(p,i) in dom f1;
then A8: dom (F.0) = {p+*(i,0)} by A1,A3,FUNCOP_1:19;
dom f1 c= (arity f1)-tuples_on NAT by Th24;
then A9: len Del(p,i) = arity f1 by A7,FINSEQ_2:109; p <> <*>NAT by A1,
RELAT_1:60;
then len p <> 0 by FINSEQ_1:32; then consider n being Nat such that
A10: len p = n+1 by NAT_1:22;
A11: len Del(p,i) = n by A1,A10,GOBOARD1:6;
dom p = dom (p+*(i,0)) by FUNCT_7:32;
then len (p+*(i,0)) = 1+arity f1 by A9,A10,A11,FINSEQ_3:31;
then (p+*(i,0)) is Element of (1+arity f1)-tuples_on NAT by FINSEQ_2:110;
hence dom (F.0) c= (1+arity f1)-tuples_on NAT by A8,ZFMISC_1:37;
suppose not Del(p,i) in dom f1;
hence dom (F.0) c= (1+arity f1)-tuples_on NAT by A4,RELAT_1:60,XBOOLE_1:2;
end;
A12: now let m be Nat such that
A13: p[m];
set pc = (p+*(i,m))^<*(F.m).(p+*(i,m))*>;
per cases;
suppose A14: p+*(i,m) in dom (F.m) & pc in dom f2;
then F.(m+1) = (F.m)+*({p+*(i,m+1)}--> f2.(pc)) by A1,A5;
then dom (F.(m+1)) = dom (F.m) \/ dom ({p+*(i,m+1)}--> f2.(pc))
by FUNCT_4:def 1;
then A15: dom (F.(m+1)) = dom (F.m) \/ {p+*(i,m+1)} by FUNCOP_1:19;
dom (p+*(i,m)) = dom p by FUNCT_7:32
.= dom (p+*(i,m+1)) by FUNCT_7:32;
then A16: len (p+*(i,m)) = len (p+*(i,m+1)) by FINSEQ_3:31;
len (p+*(i,m)) = 1+arity f1 by A13,A14,FINSEQ_2:109;
then p+*(i,m+1)is Element of (1+arity f1)-tuples_on NAT by A16,
FINSEQ_2:110;
then {p+*(i,m+1)} c= (1+arity f1)-tuples_on NAT by ZFMISC_1:37;
hence p[m+1] by A13,A15,XBOOLE_1:8;
suppose not p+*(i,m) in dom (F.m) or not pc in dom f2;
hence p[m+1] by A5,A13;
end;
for m being Nat holds p[m] from Ind(A6,A12);
hence thesis by A2;
suppose not i in dom p; then primrec(f1,f2,i,p) = {} by Th54;
hence thesis by RELAT_1:60,XBOOLE_1:2;
end;
theorem Th57:
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; assume
A1: f1 is empty; consider F be Function of NAT, 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))) &
(not i in dom p or not Del(p,i) in dom f1 implies F.0 = {}) and
A4: 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 Def13;
defpred p[Nat] means F.$1 = {};
A5: p[0] by A1,A3,RELAT_1:60;
A6: for k be Nat st p[k] holds p[k+1] by A4,RELAT_1:60;
for k being Nat holds p[k] from Ind(A5,A6);
hence primrec(f1,f2,i,p) is empty by A2;
end;
theorem Th58:
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 & i <= 1+arity f1;
A5: len p = 1+arity f1 by FINSEQ_2:109;
then A6: i in dom p by A4,FINSEQ_3:27;
then A7: p/.i = p.i by FINSEQ_4:def 4;
consider F being Function of NAT, HFuncs NAT such that
A8: primrec(f1,f2,i,p) = F.(p/.i) and
A9: (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
A10: 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 Def13;
defpred p[Nat] means (p+*(i,$1)) in dom (F.$1);
A11: now
A12: len Del(p,i) = arity f1 by A5,A6,GOBOARD1:6;
reconsider Dpi = Del(p,i) as FinSequence of NAT by MATRIX_2:9;
reconsider Dpi' = Dpi as Element of (len Dpi)-tuples_on NAT
by FINSEQ_2:110; dom f1 = (arity f1)-tuples_on NAT by A1,Th26;
then Dpi' in dom f1 by A12; then dom (F.0) = {p+*(i,0)} by A4,A5,A9,
FINSEQ_3:27,FUNCOP_1:19;
hence p[0] by TARSKI:def 1;
end;
A13: now let m be Nat such that
A14: p[m]; set pc = (p+*(i,m))^<*(F.m).(p+*(i,m))*>;
A15: dom f2 = (arity f2)-tuples_on NAT by A2,Th26;
F.m is Element of HFuncs NAT;
then A16: rng (F.m) c= NAT by RELSET_1:12;
(F.m).(p+*(i,m)) in rng (F.m) by A14,FUNCT_1:12;
then reconsider aa = (F.m).(p+*(i,m)) as Nat by A16;
reconsider p2 = <*aa*> as FinSequence of NAT;
reconsider p1 = (p+*(i,m))^p2 as FinSequence of NAT;
len (p+*(i,m))=1+arity f1 & len p2 = 1 by FINSEQ_2:109;
then len p1 = arity f1+1+1 by FINSEQ_1:35
.= arity f1+(1+1) by XCMPLX_1:1 .= arity f2 by A3;
then p1 is Element of (arity f2)-tuples_on NAT by FINSEQ_2:110;
then F.(m+1) = (F.m)+*({p+*(i,m+1)}--> f2.(pc)) by A6,A10,A14,A15;
then A17: dom(F.(m+1))=dom (F.m) \/
dom ({p+*(i,m+1)}--> f2.(pc))by FUNCT_4:def 1;
p+*(i,m+1) in {p+*(i,m+1)} by TARSKI:def 1;
then p+*(i,m+1) in dom ({p+*(i,m+1)}--> f2.(pc)) by FUNCOP_1:19;
hence p[m+1] by A17,XBOOLE_0:def 2;
end;
A18: for m being Nat holds p[m] from Ind(A11, A13);
(p+*(i,p.i)) = p by FUNCT_7:37;
hence p in dom primrec(f1,f2,i,p) by A7,A8,A18;
end;
definition
let f1,f2 be homogeneous to-naturals from-natural-fseqs Function;
let i be Nat;
reconsider ff1 = f1, ff2 = f2 as Element of HFuncs NAT by Th31;
func primrec(f1,f2,i) -> Element of HFuncs NAT means:Def14:
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 set n = arity f1+1;
deffunc f(FinSequence of NAT) = primrec(f1,f2,i,$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 LambdaD;
A2: dom G = n-tuples_on NAT & rng G c= HFuncs NAT by FUNCT_2:def 1,RELSET_1:12;
consider np being Element of n-tuples_on NAT;
G.np in rng G by A2,FUNCT_1:12;
then reconsider Y = rng G as non empty Subset of HFuncs NAT by RELSET_1:12;
Y is PartFunc-set of NAT*, NAT
proof let f be Element of Y; thus f is PartFunc of NAT*, NAT; end;
then reconsider Y as PFUNC_DOMAIN of NAT*, NAT;
A3: Y is compatible proof let f,g be Function; assume f in Y;
then consider x being set such that
A4: x in dom G & f = G.x by FUNCT_1:def 5; assume g in Y;
then consider y being set such that
A5: y in dom G & g = G.y by FUNCT_1:def 5;
reconsider x,y as Element of n-tuples_on NAT by A4,A5;
f = primrec(ff1,ff2,i,x) & g = primrec(ff1,ff2,i,y) by A1,A4,A5;
hence thesis by Th55;
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 Th56;
end; then consider g being Element of HFuncs NAT such that
A6: g = Union G & dom g c= n-tuples_on NAT by A3,Th43;
take g, G; thus thesis by A1,A6;
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
A7: g1 = Union G1 and
A8: 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
A9: g2 = Union G2 and
A10: 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 A8 .= G2.p by A10;
end;
hence thesis by A7,A9,FUNCT_2:113;
end;
end;
theorem Th59:
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 Def14;
A4: dom G = (arity f1+1)-tuples_on NAT by FUNCT_2:def 1;
now let y be set;
hereby assume y in rng G; then consider x being set such that
A5: x in dom G & G.x = y by FUNCT_1:def 5;
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,Th57;
hence y in {{}} by A5,TARSKI:def 1;
end; assume y in {{}};
then A6: y = {} by TARSKI:def 1;
consider p being Element of (arity f1+1)-tuples_on NAT; G.p = primrec
(
f1,f2,i,p) by A3
.= {} by A1,Th57;
hence y in rng G by A4,A6,FUNCT_1:12;
end;
then A7: rng G = {{}} by TARSKI:2;
Union G = union rng G by PROB_1:def 3 .= {} by A7,ZFMISC_1:31;
hence primrec(f1,f2,i) is empty by A2;
end;
theorem Th60:
dom primrec(f1,f2,i) c= (arity f1+1)-tuples_on NAT
proof let x be set 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 Def14;
A4: rng G is compatible proof let f,g being Function such that
A5: f in rng G & g in rng G; consider fx being set such that
A6: fx in dom G & f = G.fx by A5,FUNCT_1:def 5;
consider gx being set such that
A7: gx in dom G & g = G.gx by A5,FUNCT_1:def 5;
reconsider fx as Element of (arity f1+1)-tuples_on NAT by A6;
reconsider gx as Element of (arity f1+1)-tuples_on NAT by A7;
G.fx = primrec(f1,f2,i,fx) & G.gx = primrec(f1,f2,i,gx) by A3;
hence f tolerates g by A6,A7,Th55;
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 Th56;
end; then consider F being Element of HFuncs NAT such that
A8: F = Union G & dom F c= (arity f1+1)-tuples_on NAT by A4,Th43;
thus x in (arity f1+1)-tuples_on NAT by A1,A2,A8;
end;
theorem Th61:
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 & i <= 1+arity f1;
A5: dom primrec(f1,f2,i) c= (arity f1+1)-tuples_on NAT by Th60;
set n = arity f1+1;
n-tuples_on NAT c= dom primrec(f1,f2,i) proof let x be set such that
A6: x in n-tuples_on NAT;
reconsider x' = x as Element of n-tuples_on NAT by A6;
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 Def14;
A9: G.x' = primrec(f1,f2,i,x') by A8;
A10: x' in dom primrec(f1,f2,i,x') by A1,A2,A3,A4,Th58;
dom G = n-tuples_on NAT by FUNCT_2:def 1;
then A11: G.x' in rng G by FUNCT_1:12;
Union G = union rng G by PROB_1:def 3;
then reconsider rngG = rng G as non empty functional compatible set by A7,A11
,Th14
;
A12: dom union rngG =
union {dom f where f is Element of rngG: not contradiction} by Th15;
dom (G.x') in {dom f where f is Element of rngG:not contradiction} by A11
;
then x in dom union rngG by A9,A10,A12,TARSKI:def 4;
hence x in dom primrec(f1,f2,i) by A7,PROB_1:def 3;
end;
hence dom primrec(f1,f2,i) = (arity f1+1)-tuples_on NAT by A5,XBOOLE_0:def 10
;
hence arity primrec(f1,f2,i) = arity f1+1 by Th28;
end;
Lm2: now
let f1,f2 be non empty homogeneous to-naturals from-natural-fseqs Function;
let p be Element of (arity f1+1)-tuples_on NAT;
let i, m be Nat; set pm1 = p+*(i,m+1), pm = p+*(i,m);
let F1, F be Function of NAT, 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))) &
(not i in dom pm1 or not Del(pm1,i) in dom f1 implies F1.0 = {}) and
A2: for M being Nat holds Q[M, F1.M, F1.(M+1), pm1, i, f2] and
A3: (i in dom pm & Del(pm,i) in dom f1
implies F.0 = {pm+*(i,0)} --> (f1.Del(pm,i))) &
(not i in dom pm or not Del(pm,i) in dom f1 implies F.0 = {}) and
A4: for M being Nat holds Q[M, F.M, F.(M+1), pm, i, f2];
A5: dom p = dom pm & dom p = dom pm1 by FUNCT_7:32;
A6: pm+*(i,0) = p+*(i,0) by FUNCT_7:36 .= pm1+*(i,0) by FUNCT_7:36;
A7: Del(pm,i) = Del(p,i) by Th6 .= Del(pm1,i) by Th6;
for x being set st x in NAT holds F.x = F1.x proof
defpred p[Nat] means F.$1 = F1.$1;
A8: p[0] by A1,A3,A5,A6,A7;
A9: for k be Nat st p[k] holds p[k+1] proof let k be Nat such that
A10: p[k];
A11: pm+*(i,k) = p+*(i,k) by FUNCT_7:36 .= pm1+*(i,k) by FUNCT_7:36;
A12: pm+*(i,(k+1))=p+*(i,(k+1)) by FUNCT_7:36.=pm1+*(i,(k+1)) by FUNCT_7:36;
per cases;
suppose A13: 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 A4
.= F1.(k+1) by A2,A5,A10,A11,A12,A13;
suppose A14: 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 A4 .= F1.(k+1) by A2,A5,A10,A11,A14;
end;
A15: for k being Nat holds p[k] from Ind(A8, A9);
let x be set; assume x in NAT; hence thesis by A15;
end; hence F1 = F by FUNCT_2:18;
end;
Lm3: now
let f1,f2 be non empty homogeneous to-naturals from-natural-fseqs Function;
let p be Element of (arity f1+1)-tuples_on NAT;
let i, m be Nat such that
A1: i in dom p; set pm = p+*(i,m), pm1 = p+*(i,(m+1));
let F be Function of NAT, 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))) &
(not i in dom pm1 or not Del(pm1,i) in dom f1 implies F.0 = {}) and
A3: for M being Nat holds Q[M, F.M, F.(M+1), pm1, i, f2];
thus F.(m+1).pm = F.m.pm proof
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 A4: F.(m+1) =
(F.m)+*({pm1+*(i,m+1)}--> f2.((pm1+*(i,m))^<*(F.m).(pm1+*(i,m))*>)) by A3;
pm.i = m & pm1.i = m+1 by A1,FUNCT_7:33;
then pm <> pm1 & pm1 = pm1+*(i,m+1) by FUNCT_7:36,NAT_1:38;
then not pm in {pm1+*(i,m+1)} by TARSKI:def 1;
then not pm in dom
({pm1+*(i,m+1)}--> f2.((pm1+*(i,m))^<*(F.m).(pm1+*(i,m))*>)) by FUNCOP_1:19;
hence F.(m+1).pm = F.m.pm by A4,FUNCT_4:12;
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 F.(m+1).pm = F.m.pm by A3;
end;
A5: 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;
A6: p[0] proof let k be Nat such that
A7: 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,FUNCOP_1:19;
then A8:(p+*(i,k)) = (pm1+*(i,0)) by A7,TARSKI:def 1 .= p+*(i,0) by FUNCT_7
:36;
k = (p+*(i,k)).i by A1,FUNCT_7:33 .= 0 by A1,A8,FUNCT_7:33;
hence k <= 0;
suppose not i in dom pm1 or not Del(pm1,i) in dom f1;
hence k <= 0 by A2,A7,RELAT_1:60;
end;
A9: for m be Nat st p[m] holds p[m+1]
proof let m be Nat such that
A10: p[m];
let k be Nat such that
A11: 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 A3;
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 A12: dom (F.(m+1)) = dom (F.m) \/ {pm1+*(i,m+1)} by FUNCOP_1:19;
thus k <= (m+1) proof
per cases by A11,A12,XBOOLE_0:def 2;
suppose p+*(i,k) in dom (F.m); then k <= m & m <= m+1 by A10,NAT_1:29;
hence k <= (m+1) by AXIOMS:22;
suppose p+*(i,k) in {pm1+*(i,m+1)};
then A13: p+*(i,k)= pm1+*(i,m+1) by TARSKI:def 1 .=p+*(i,m+1) by
FUNCT_7:36;
k = (p+*(i,k)).i by A1,FUNCT_7:33 .= m+1 by A1,A13,FUNCT_7:33;
hence k <= (m+1);
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 A3;
then k <= m & m <= m+1 by A10,A11,NAT_1:29;
hence k <= (m+1) by AXIOMS:22;
end; thus for n be Nat holds p[n] from Ind(A6, A9);
end;
thus not pm1 in dom (F.m) proof assume not thesis; then m+1 <= m by A5;
hence contradiction by NAT_1:38;
end;
end;
Lm4: now
let f1,f2 be non empty homogeneous to-naturals from-natural-fseqs Function;
let p be Element of (arity f1+1)-tuples_on NAT;
let i, m be 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: p[0];
A4: now let n be Nat such that
A5: p[n];
set pkn = p+*(i,(k+n)); set pkn1 = p+*(i,((k+n)+1)); set m = k+n;
consider F being Function of NAT, 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))) &
(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, F.(M+1), pkn, i, f2] by Def13;
consider F1 being Function of NAT, HFuncs NAT such that
A9: primrec(f1,f2,i,pkn1)= F1.(pkn1/.i) and
A10: (i in dom pkn1 & Del(pkn1,i) in dom f1
implies F1.0 = {pkn1+*(i,0)} --> (f1.Del(pkn1,i))) &
(not i in dom pkn1 or not Del(pkn1,i) in dom f1 implies F1.0 = {}) and
A11: for M being Nat holds Q[M, F1.M, F1.(M+1), pkn1, i, f2] by Def13;
A12: F1 = F by A7,A8,A10,A11,Lm2;
A13: dom p = dom pk & dom p = dom pkn1 & dom p = dom pkn by FUNCT_7:32;
then A14: pkn1/.i = pkn1.i by A1,FINSEQ_4:def 4 .= m+1 by A1,FUNCT_7:33;
A15: pkn/.i = pkn.i by A1,A13,FINSEQ_4:def 4 .= m by A1,FUNCT_7:33;
k+n+1 = k+(n+1) by XCMPLX_1:1;
then A16: G.(p+*(i,(k+(n+1)))) = F.(m+1) by A2,A9,A12,A14;
A17: G.(p+*(i,(k+n))) = F.m by A2,A6,A15;
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 A5,A16,A17,XBOOLE_1:1;
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 A5,A8,A16,A17;
end;
thus for n being Nat holds p[n] from Ind(A3, A4);
end;
end;
Lm5: now
let f1,f2 be non empty homogeneous to-naturals from-natural-fseqs Function;
let p be Element of (arity f1+1)-tuples_on NAT;
let i, m be 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: p[0];
A4: for n be Nat st p[n] holds p[n+1] proof let n be Nat such that
A5: p[n] and
A6: not pk in dom (G.pk);
set pkn = p+*(i,(k+n)); set pkn1 = p+*(i,((k+n)+1)); set m = k+n;
consider F being Function of NAT, HFuncs NAT such that
A7: primrec(f1,f2,i,pkn)= F.(pkn/.i) and
A8: (i in dom pkn & Del(pkn,i) in dom f1
implies F.0 = {pkn+*(i,0)} --> (f1.Del(pkn,i))) &
(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, F.(M+1), pkn, i, f2] by Def13;
consider F1 being Function of NAT, 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))) &
(not i in dom pkn1 or not Del(pkn1,i) in dom f1 implies F1.0 = {}) and
A12: for M being Nat holds Q[M, F1.M, F1.(M+1), pkn1, i, f2] by Def13;
A13: F1 = F by A8,A9,A11,A12,Lm2;
A14: dom p = dom pk & dom p = dom pkn1 & dom p = dom pkn by FUNCT_7:32;
then A15: pkn1/.i = pkn1.i by A1,FINSEQ_4:def 4 .= m+1 by A1,FUNCT_7:33;
A16: pkn/.i = pkn.i by A1,A14,FINSEQ_4:def 4 .= m by A1,FUNCT_7:33;
A17: k+n+1 = k+(n+1) by XCMPLX_1:1;
A18: not pk in dom (F.m) by A2,A5,A6,A7,A16;
A19: G.(p+*(i,(k+(n+1)))) = F.(m+1) by A2,A10,A13,A15,A17;
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 A20: dom (F.(m+1)) = dom (F.m) \/ {pkn+*(i,m+1)} by FUNCOP_1:19;
k <= k+n by NAT_1:29;
then A21: k <> m+1 by NAT_1:38; pk.i = k & (pkn+*(i,m+1)).i = m+1 by A1,A14
,FUNCT_7:33; then not pk in {pkn+*(i,m+1)} by A21,TARSKI:def 1;
hence not pk in dom (G.(p+*(i,(k+(n+1))))) by A18,A19,A20,XBOOLE_0:def 2;
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 not pk in dom (G.(p+*(i,(k+(n+1))))) by A9,A18,A19;
end;
thus for n being Nat holds p[n] from Ind(A3, A4);
end;
end;
Lm6: 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 assume
A1: i in dom p;
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 Def14;
A4: Union G = union rng G by PROB_1:def 3;
then reconsider rngG = rng G as functional compatible set by A2,Th14;
A5: dom G = (arity f1+1)-tuples_on NAT by FUNCT_2:def 1;
A6: now let k be Nat such that
A7: p+*(i,k) in dom primrec(f1,f2,i) and
A8: not p+*(i,k) in dom (G.((p+*(i,k)))); set pk = p+*(i,k); union
rngG <> {} by A2,A7,PROB_1:def 3,RELAT_1:60;
then reconsider rngG = rng G as non empty functional compatible set by
ZFMISC_1:2;
dom union rngG = union {dom f where f is Element of rngG
: not contradiction} by Th15;
then consider X being set such that
A9: pk in X & X in {dom f where f is Element of rngG: not contradiction}
by A2,A4,A7,TARSKI:def 4;
consider f being Element of rngG such that
A10: X = dom f & not contradiction by A9; consider pp being set such that
A11: pp in dom G & f = G.pp by FUNCT_1:def 5;
reconsider pp as Element of (arity f1+1)-tuples_on NAT by A11;
G.pp = primrec(f1,f2,i,pp) by A3; then consider m being Nat such that
A12: pk = pp+*(i,m) by A9,A10,A11,Th53;
set ppi = pp.i;
A13: p+*(i,ppi) = pk+*(i,ppi) by FUNCT_7:36 .= pp+*(i,ppi) by A12,FUNCT_7:
36
.= pp by FUNCT_7:37;
per cases by AXIOMS:21;
suppose k = ppi; hence contradiction by A8,A9,A10,A11,A13;
suppose ppi < k; then consider m being Nat such that
A14: k = ppi+m by NAT_1:28; dom (G.pp) c= dom (G.pk) by A1,A3,A13,A14,
Lm4;
hence contradiction by A8,A9,A10,A11;
suppose ppi > k; then consider m being Nat such that
A15: ppi=k+m by NAT_1:28;
thus contradiction by A1,A3,A8,A9,A10,A11,A13,A15,Lm5;
end;
set p0 = p+*(i,0);
A16: dom p = dom p0 by FUNCT_7:32;
A17: now
A18: G.p0 = primrec(f1,f2,i,p0) by A3;
consider F being Function of NAT, HFuncs NAT such that
A19: primrec(f1,f2,i,p0)= F.(p0/.i) and
A20: (i in dom p0 & Del(p0,i) in dom f1
implies F.0 = {p0+*(i,0)} --> (f1.Del(p0,i)))and
A21: (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, F.(m+1), p0, i, f2] by Def13;
A22: p0/.i = p0.i by A1,A16,FINSEQ_4:def 4 .= 0 by A1,FUNCT_7:33;
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 A3,A19,A21,A22,Th6,RELAT_1:60;
assume Del(p,i) in dom f1;
then dom (F.0) = {p0+*(i,0)} by A1,A20,Th6,FUNCOP_1:19,FUNCT_7:32 .= {
p0} by FUNCT_7:36;
hence p0 in dom (G.p0) by A18,A19,A22,TARSKI:def 1;
end;
assume p0 in dom (G.p0);
then F.0 = {p0} --> (f1.Del(p0,i)) by A3,A19,A20,A21,A22,FUNCT_7:36,
RELAT_1:60;
then F.0 = {p0} --> (f1.Del(p,i)) & p0 in {p0} by Th6,TARSKI:def 1;
hence (G.p0).p0 = f1.Del(p,i) by A18,A19,A22,FUNCOP_1:13;
end;
A23: G.p0 in rng G by A5,FUNCT_1:def 5;
then reconsider rngG as non empty functional compatible set;
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 A6,A17;
assume A24: Del(p,i) in dom f1;
dom (G.p0) in {dom f where f is Element of rngG:not contradiction} by A23
;
then p0 in union {dom f where f is Element of rngG: not contradiction}
by A17,A24,TARSKI:def 4;
hence p+*(i,0) in dom primrec(f1,f2,i) by A2,A4,Th15;
end;
hereby assume A25: p+*(i,0) in dom primrec(f1,f2,i);
then p0 in dom (G.p0) by A6; then (union rngG).p0 = (G.p0).p0 by A23,Th16;
hence primrec(f1,f2,i).(p+*(i,0)) = f1.Del(p,i) by A2,A6,A17,A25,PROB_1:def 3
;
end;
set pm1 = p+*(i,m+1), pm = p+*(i,m), pc = <*(G.pm1).(pm1+*(i,m))*>;
A26: dom p = dom pm1 & dom p = dom pm by FUNCT_7:32;
A27: pm1+*(i,m) = pm & pm1+*(i,m+1) = pm1 by FUNCT_7:36;
A28: now
A29: G.pm1 = primrec(f1,f2,i,pm1) & G.pm = primrec(f1,f2,i,pm) by A3;
consider F1 being Function of NAT, HFuncs NAT such that
A30: primrec(f1,f2,i,pm1)= F1.(pm1/.i) and
A31: (i in dom pm1 & Del(pm1,i) in dom f1
implies F1.0 = {pm1+*(i,0)} --> (f1.Del(pm1,i))) &
(not i in dom pm1 or not Del(pm1,i) in dom f1 implies F1.0 = {}) and
A32: for M being Nat holds Q[M, F1.M, F1.(M+1), pm1, i, f2] by Def13;
consider F being Function of NAT, HFuncs NAT such that
A33: primrec(f1,f2,i,pm)= F.(pm/.i) and
A34: (i in dom pm & Del(pm,i) in dom f1
implies F.0 = {pm+*(i,0)} --> (f1.Del(pm,i))) &
(not i in dom pm or not Del(pm,i) in dom f1 implies F.0 = {}) and
A35: for M being Nat holds Q[M, F.M, F.(M+1), pm, i, f2] by Def13;
A36: pm1/.i = pm1.i by A1,A26,FINSEQ_4:def 4 .= m+1 by A1,FUNCT_7:33;
A37: pm/.i = pm.i by A1,A26,FINSEQ_4:def 4 .= m by A1,FUNCT_7:33;
A38: F1.m = F.m by A31,A32,A34,A35,Lm2;
A39: F1.(m+1).pm = F1.m.pm by A1,A31,A32,Lm3;
A40: not pm1 in dom (F1.m) by A1,A31,A32,Lm3;
thus
A41: pm1 in dom (G.pm1) iff pm in dom (G.pm) & pm^pc in dom f2 proof
hereby assume A42: pm1 in dom (G.pm1);
then A43: pm1 in dom (F1.(m+1)) by A3,A30,A36;
assume A44: not (pm in dom (G.pm) & pm^pc in dom f2);
per cases by A44;
suppose not pm in dom (G.pm);
then not pm in dom (F1.m) by A3,A33,A37,A38;
hence contradiction by A27,A32,A40,A43;
suppose not pm^pc in dom f2;
hence contradiction by A27,A29,A30,A32,A36,A39,A40,A42;
end;
assume pm in dom (G.pm) & pm^pc in dom f2;
then A45: F1.(m+1) = (F1.m)+*({pm1}--> f2.((pm)^<*(F1.m).pm*>))
by A1,A26,A27,A29,A30,A32,A33,A36,A37,A38,A39; pm1 in {pm1} by
TARSKI:def 1;
then pm1 in dom ({pm1}--> f2.((pm)^<*(F1.m).pm*>)) by FUNCOP_1:19;
then pm1 in dom (F1.m) \/ dom ({pm1}--> f2.((pm)^<*(F1.m).pm*>))
by XBOOLE_0:def 2
;
hence pm1 in dom (G.pm1) by A29,A30,A36,A45,FUNCT_4:def 1;
end;
assume A46: pm1 in dom (G.pm1);
then pm^<*(F1.m).pm*> in dom f2 by A27,A29,A30,A32,A36,A41;
then A47: F1.(m+1) = (F1.m)+*({pm1}--> f2.((pm)^<*(F1.m).pm*>))
by A1,A26,A27,A29,A32,A33,A37,A38,A41,A46;
A48: pm1 in {pm1} by TARSKI:def 1;
then pm1 in dom ({pm1}--> f2.((pm)^<*(F1.m).pm*>)) by FUNCOP_1:19;
hence G.(pm1).pm1 =
({pm1}-->f2.((pm)^<*(F1.m).pm*>)).pm1 by A29,A30,A36,A47,FUNCT_4:14
.= f2.(pm^pc) by A27,A29,A30,A36,A39,A48,FUNCOP_1:13;
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 A49: p+*(i,m+1) in dom primrec(f1,f2,i); G.pm in rng G by A5,
FUNCT_1:def 5;
then dom (G.pm) in {dom f where f is Element of rngG: not contradiction
};
then pm in union {dom f where f is Element of rngG: not contradiction}
by A6,A28,A49,TARSKI:def 4;
hence p+*(i,m) in dom primrec(f1,f2,i) by A2,A4,Th15;
A50: G.pm1 in rng G by A5,FUNCT_1:def 5; dom (G.pm) c= dom (G.pm1) by A1,A3
,Lm4
; then (union rngG).pm = (G.pm1).pm by A6,A28,A49,A50,Th16
;
hence (p+*(i,m))^<*primrec(f1,f2,i).(p+*(i,m))*> in dom f2 by A2,A6,A27,A28
,A49,PROB_1:def 3;
end;
assume A51: p+*(i,m) in dom primrec(f1,f2,i) &
(p+*(i,m))^<*primrec(f1,f2,i).(p+*(i,m))*> in dom f2;
then A52: pm in dom (G.pm) by A6;
A53: G.pm1 in rng G by A5,FUNCT_1:def 5; dom (G.pm) c= dom (G.pm1) by A1,A3
,Lm4; then A54: (union rngG).pm = (G.pm1).pm by A52,A53,Th16
;
G.pm1 in rng G by A5,FUNCT_1:def 5;
then dom (G.pm1)in {dom f where f is Element of rngG: not contradiction
};
then pm1 in union {dom f where f is Element of rngG: not contradiction}
by A2,A6,A27,A28,A51,A54,PROB_1:def 3,TARSKI:def 4;
hence p+*(i,m+1) in dom primrec(f1,f2,i) by A2,A4,Th15;
end;
assume A55: p+*(i,m+1) in dom primrec(f1,f2,i);
A56: G.pm1 in rng G by A5,FUNCT_1:def 5;
dom (G.pm) c= dom (G.pm1) by A1,A3,Lm4;
then (union rngG).pm = (G.pm1).pm & (union rngG).pm1 = (G.pm1).pm1
by A6,A28,A55,A56,Th16;
hence primrec(f1,f2,i).(p+*(i,m+1))
= f2.((p+*(i,m))^<*primrec(f1,f2,i).(p+*(i,m))*>) by A2,A4,A6,A28,A55,
FUNCT_7:36;
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 Th64:
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; len p = arity f1+1 by FINSEQ_2:109;
then A3: len Del(p,i) = arity f1 by A1,GOBOARD1:6;
A4: dom f1 = (arity f1)-tuples_on NAT by A2,Th26;
Del(p,i) is FinSequence of NAT by MATRIX_2:9;
then Del(p,i) is Element of (arity f1)-tuples_on NAT by A3,FINSEQ_2:110;
then p+*(i,0) in dom primrec(f1,f2,i) by A1,A4,Lm6;
hence primrec(f1,f2,i).(p+*(i,0)) = f1.Del(p,i) 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 Th67:
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 & i <= 1+arity f1; len p = arity f1 +1 by FINSEQ_2:109;
then A5: i in dom p by A4,FINSEQ_3:27;
(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,Th61;
hence primrec(f1,f2,i).(p+*(i,m+1))
= f2.((p+*(i,m))^<*primrec(f1,f2,i).(p+*(i,m))*>) by A5,Lm6;
end;
theorem Th68:
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 & i <= arity f1+1;
set g = primrec(f1,f2,i);
take n = arity f1+1; thus dom g c= n-tuples_on NAT by Th60;
thus i >= 1 & i <= n by A2; thus arity f1+1 = n;
thus n+1 = arity f1+(1+1) by XCMPLX_1:1 .= arity f2 by A1;
let p be FinSequence of NAT; assume
A3: len p = n;
then A4: p is Element of n-tuples_on NAT by FINSEQ_2:110;
A5: i in dom p by A2,A3,FINSEQ_3:27;
hence p+*(i,0) in dom g iff Del(p,i) in dom f1 by A4,Lm6;
thus p+*(i,0) in dom g implies g.(p+*(i,0)) = f1.Del(p,i) by A4,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 A4,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 A4,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
A1: i >= 1 & i <= arity f1+1; set n = arity f1+1, h = primrec(f1,f2,i);
let g be Element of HFuncs NAT; given n' being Nat such that
A2: dom g c= n'-tuples_on NAT & i >= 1 & i <= n' and
A3: (arity f1)+1 = n' & n'+1 = arity f2 and
A4: 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))*>));
A5: dom h c= n-tuples_on NAT by Th60;
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)));
A7: len p = n by FINSEQ_2:109;
then A8: i in dom p by A1,FINSEQ_3:27;
then A9: (p+*(i,0) in dom g iff Del(p,i) in dom f1) &
(p+*(i,0) in dom h iff Del(p,i) in dom f1) by A3,A4,A7,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 A3,A4,A7,A8,Lm6;
then A10: p[0] by A9;
set k = p/.i;
A11: p = p+*(i,k) by FUNCT_7:40;
A12: for m be Nat st p[m] holds p[m+1] proof let m such that
A13: p+*(i,m) in dom g iff p+*(i,m) in dom h and
A14: p+*(i,m) in dom g implies g.(p+*(i,m)) = h.(p+*(i,m));
A15: 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 A3,A4,A7;
A16: 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 A8,Lm6;
thus
p+*(i,m+1) in dom g iff p+*(i,m+1) in dom h by A8,A13,A14,A15,Lm6;
assume
A17: p+*(i,m+1) in dom g;
then g.(p+*(i,m+1)) = f2.((p+*(i,m))^<*g.(p+*(i,m))*>) &
g.(p+*(i,m)) = h.(p+*(i,m)) by A3,A4,A7,A14;
hence g.(p+*(i,m+1)) = h.(p+*(i,m+1)) by A3,A4,A7,A8,A13,A16,A17,Lm6;
end;
for m holds p[m] from Ind(A10,A12);
hence (p in dom g iff p in dom h) & (p in dom g implies g.p = h.p) by A11;
end;
then A18: dom g = dom h by A2,A3,A5,SUBSET_1:8;
then for x being set st x in dom h holds g.x = h.x by A5,A6;
hence thesis by A18,FUNCT_1:9;
end;
begin :: The set of primitive recursive functions
definition
let X be set;
attr X is composition_closed means:Def15:
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:Def16:
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:Def17:
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 Th70:
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 Th34,Th37,Th39;
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 Th46;
let g be Element of HFuncs NAT; thus thesis;
end;
definition
cluster primitive-recursively_closed non empty 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 Th70;
end;
end;
reserve P for primitive-recursively_closed non empty Subset of HFuncs NAT;
Lm7:
for X being non empty set, n,i be 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 Th71:
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 Nat such that
A2: dom g c= n-tuples_on NAT and
i >= 1 & i <= n and
(arity f1)+1 = n & 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))*>)) by Def12;
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 FINSEQ_2:109;
then A6: p[0] by A1,A3,RELAT_1:60;
A7: for k being Nat st p[k] holds p[k+1] by A3,A5;
thus for k being Nat holds p[k] from Ind(A6, A7);
end; assume g <> {}; then dom g <> {} by RELAT_1:64;
then consider x being set 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:37;
hence contradiction by A4,A8;
end;
theorem Th72:
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 Nat such that
A2: dom g c= n-tuples_on NAT and
A3: i >= 1 & i <= n and
A4: (arity f1)+1 = n & n+1 = arity f2 and
A5: 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))*>)) by Def12;
reconsider f2' = f2 as non empty quasi_total Element of HFuncs(NAT) by A4,
Th21;
per cases;
suppose f1 is empty;
hence thesis by A1,Th71;
suppose A6: f1 is non empty; consider pp being set such that
A7: pp in n-tuples_on NAT by XBOOLE_0:def 1;
pp is Element of n-tuples_on NAT by A7;
then reconsider p = pp as FinSequence of NAT;
A8: len p = n by A7,FINSEQ_2:109;
A9: dom f1 = (arity f1)-tuples_on NAT by A6,Th25;
A10: Del(p,i) in (arity f1)-tuples_on NAT by A3,A4,A7,Th12;
g is quasi_total proof let x, y be FinSequence of NAT such that
A11: len x = len y and
A12: x in dom g;
A13: len x = n by A2,A12,FINSEQ_2:109;
defpred p[Nat] means y+*(i,$1) in dom g;
y is Element of (len y)-tuples_on NAT by FINSEQ_2:110;
then Del(y,i) in (arity f1)-tuples_on NAT by A3,A4,A11,A13,Th12;
then A14: p[0] by A5,A9,A11,A13;
A15: now let k be Nat such that
A16: p[k];
A17: dom f2' = (arity f2)-tuples_on NAT by Th25;
A18: len ((y+*(i,k))^<*g.(y+*(i,k))*>)
= len (y+*(i,k)) + len <*g.(y+*(i,k))*> by FINSEQ_1:35
.= n+len <*g.(y+*(i,k))*> by A11,A13,JORDAN2B:12 .= n+1 by FINSEQ_1:56;
rng g c= NAT & g.(y+*(i,k)) in rng g by A16,FUNCT_1:12,RELSET_1:12;
then reconsider gyk = g.(y+*(i,k)) as Nat;
reconsider gyik = <*gyk*> as FinSequence of NAT;
(y+*(i,k))^gyik is FinSequence of NAT;
then (y+*(i,k))^<*g.(y+*(i,k))*> is Element of dom f2 by A4,A17,A18,
FINSEQ_2:110;
then (y+*(i,k))^<*g.(y+*(i,k))*> in dom f2';
hence p[k+1] by A5,A11,A13,A16;
end; for k being Nat holds p[k] from Ind(A14, A15);
then A19: y+*(i,y/.i) in dom g; i in dom y by A3,A11,A13,FINSEQ_3:27;
then y.i = y/.i by FINSEQ_4:def 4;
hence y in dom g by A19,FUNCT_7:37;
end; hence thesis by A5,A8,A9,A10,RELAT_1:60;
end;
theorem Th73:
n const c in P
proof
A1: P is composition_closed by Def17;
defpred p[Nat] means 0 const $1 in P;
A2: p[0] by Def17;
A3: for i be Nat st p[i] holds p[i+1] proof
let i be Nat; set F = <*0 const i*>;
reconsider 0consti = 0 const i as Element of HFuncs NAT by Th31;
<*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 A4: {0 const i} c= P & rng F = {0 const i} by FINSEQ_1:56,ZFMISC_1:37;
A5: (1 succ 1) in P by Def17;
A6: arity (1 succ 1) = 1 by Th38 .= len F by FINSEQ_1:56;
reconsider 1succ1 = 1 succ 1 as quasi_total Element of HFuncs NAT by Th32;
now let h be Element of HFuncs NAT; assume h in rng F;
then h = 0 const i by A4,TARSKI:def 1;
hence h is quasi_total by Th32;
end; then reconsider g = (1succ1)*<:F:>
as quasi_total Element of HFuncs NAT by A6,Th50;
A7: arity (0 const (i+1)) = 0 & arity (0 const i) = 0 by Th35;
A8: <*>NAT is Element of 0-tuples_on NAT by FINSEQ_2:114;
then A9: (0 const (i+1)).{} = i+1 & (0 const i).{} = i by Th36;
A10: dom <:<*0 const i*>:> = dom (0 const i) by FUNCT_6:61;
A11: dom (0 const i) = 0-tuples_on NAT by A7,Th26;
then A12: <:<*0 const i*>:>.{} = <*i*> by A8,A9,FUNCT_6:61;
dom (1 succ 1) = 1-tuples_on NAT by Def10;
then A13: {} in dom g by A8,A10,A11,A12,FUNCT_1:21; 0 const i in rng F
by A4,TARSKI:def 1;
then arity F = 0 by A7,Def7;
then A14: arity g = 0 by A13,Th48,RELAT_1:60; dom (0 const i) = 0-tuples_on
NAT by A7,Th26;
then g.{} = (1 succ 1).(<:F:>.{}) & <:F:>.{} = <*i*> &
<*i*> is Element of 1-tuples_on NAT by A8,A9,A10,FUNCT_1:23,FUNCT_6:61;
then g.{} = (<*i*>/.1)+1 by Def10 .= i+1 by FINSEQ_4:25;
then 0 const (i+1) = (1 succ 1)*<:<*0 const i*>:> by A7,A9,A13,A14,Th52,
RELAT_1:60;
hence 0 const (i+1) in P by A1,A4,A5,A6,Def15;
end;
A15: P is primitive-recursion_closed by Def17;
A16: for i being Nat holds p[i] from Ind(A2,A3);
defpred r[Nat] means for c being Nat holds $1 const c in P;
A17: r[0] by A16;
A18: now let n be Nat such that
A19: r[n];
thus r[n+1]
proof
let i be Nat; set g=(n+1) const i, f1=n const i,j=n+1,f2=(n+2) proj (n+2);
A20: arity g = j by Th35; g = ((n+1)-tuples_on NAT) --> i by Def9;
then A21: dom g = (n+1)-tuples_on NAT by FUNCOP_1:19;
A22: arity f1 = n by Th35; f1 = (n-tuples_on NAT) --> i by Def9;
then A23: dom f1 = n-tuples_on NAT by FUNCOP_1:19;
A24: dom f2 = (n+2)-tuples_on NAT by Th40;
A25: arity f2 = n+2 by Th41;
A26: n+(1+1) = j+1 by XCMPLX_1:1;
A27: g is_primitive-recursively_expressed_by f1,f2,n+1
proof take m = arity g;
thus dom g c= m-tuples_on NAT by Th24;
thus j >= 1 & j <= m by Th35,NAT_1:29;
thus (arity f1)+1 = m & m+1 = a