:: COMPUT_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let X be non empty set ;
let n be Nat;
let p be Element of n -tuples_on X;
let i be Nat;
let x be Element of X;
:: original: +*
redefine func p +* i,x -> Element of n -tuples_on X;
coherence
p +* i,x is Element of n -tuples_on X
proof end;
end;

definition
let n be Nat;
let t be Element of n -tuples_on NAT ;
let i be Nat;
:: original: .
redefine func t . i -> Element of NAT ;
coherence
t . i is Element of NAT
proof end;
end;

theorem :: COMPUT_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPUT_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: COMPUT_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set holds
( <*x,y*> +* 1,z = <*z,y*> & <*x,y*> +* 2,z = <*x,z*> )
proof end;

theorem :: COMPUT_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th5: :: COMPUT_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, x, y, z being set
for f, g being Function st f +* a,x = g +* a,y holds
f +* a,z = g +* a,z
proof end;

theorem Th6: :: COMPUT_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for x being set
for p being FinSequence holds Del (p +* i,x),i = Del p,i
proof end;

theorem Th7: :: COMPUT_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for a being set
for p, q being FinSequence st p +* i,a = q +* i,a holds
Del p,i = Del q,i
proof end;

theorem Th8: :: COMPUT_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds 0 -tuples_on X = {{} }
proof end;

theorem :: COMPUT_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat st n <> 0 holds
n -tuples_on {} = {}
proof end;

theorem Th10: :: COMPUT_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function st {} in rng f holds
<:f:> = {}
proof end;

theorem Th11: :: COMPUT_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being Function st rng f = D holds
rng <:<*f*>:> = 1 -tuples_on D
proof end;

theorem Th12: :: COMPUT_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat
for D being non empty set st 1 <= i & i <= n + 1 holds
for p being Element of (n + 1) -tuples_on D holds Del p,i in n -tuples_on D
proof end;

theorem Th13: :: COMPUT_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for Y being FinSequenceSet of X holds Y c= X *
proof end;

definition
let X be set ;
attr X is compatible means :Def1: :: COMPUT_1:def 1
for f, g being Function st f in X & g in X holds
f tolerates g;
end;

:: deftheorem Def1 defines compatible COMPUT_1:def 1 :
for X being set holds
( X is compatible iff for f, g being Function st f in X & g in X holds
f tolerates g );

registration
cluster non empty functional compatible set ;
existence
ex b1 being set st
( not b1 is empty & b1 is functional & b1 is compatible )
proof end;
end;

registration
let X be functional compatible set ;
cluster union X -> Relation-like Function-like ;
coherence
( union X is Function-like & union X is Relation-like )
proof end;
end;

theorem Th14: :: COMPUT_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds
( ( X is functional & X is compatible ) iff union X is Function )
proof end;

registration
let X, Y be set ;
cluster compatible PartFunc-set of X,Y;
existence
ex b1 being PFUNC_DOMAIN of X,Y st
( not b1 is empty & b1 is compatible )
proof end;
end;

theorem Th15: :: COMPUT_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty functional compatible set holds dom (union X) = union { (dom f) where f is Element of X : verum }
proof end;

theorem Th16: :: COMPUT_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being functional compatible set
for f being Function st f in X holds
( dom f c= dom (union X) & ( for x being set st x in dom f holds
(union X) . x = f . x ) )
proof end;

theorem Th17: :: COMPUT_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty functional compatible set holds rng (union X) = union { (rng f) where f is Element of X : verum }
proof end;

registration
let X, Y be set ;
cluster -> functional PartFunc-set of X,Y;
coherence
for b1 being PFUNC_DOMAIN of X,Y holds b1 is functional
proof end;
end;

theorem Th18: :: COMPUT_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for P being compatible PFUNC_DOMAIN of X,Y holds union P is PartFunc of X,Y
proof end;

notation
let f be Relation;
synonym to-naturals f for natural-yielding f;
end;

definition
let f be Relation;
attr f is from-natural-fseqs means :Def2: :: COMPUT_1:def 2
dom f c= NAT * ;
end;

:: deftheorem Def2 defines from-natural-fseqs COMPUT_1:def 2 :
for f being Relation holds
( f is from-natural-fseqs iff dom f c= NAT * );

registration
cluster to-naturals from-natural-fseqs set ;
existence
ex b1 being Function st
( b1 is from-natural-fseqs & b1 is to-naturals )
proof end;
end;

definition
let f be from-natural-fseqs Relation;
attr f is len-total means :Def3: :: COMPUT_1:def 3
for x, y being FinSequence of NAT st len x = len y & x in dom f holds
y in dom f;
end;

:: deftheorem Def3 defines len-total COMPUT_1:def 3 :
for f being from-natural-fseqs Relation holds
( f is len-total iff for x, y being FinSequence of NAT st len x = len y & x in dom f holds
y in dom f );

definition
let f be Relation;
attr f is homogeneous means :Def4: :: COMPUT_1:def 4
for x, y being FinSequence st x in dom f & y in dom f holds
len x = len y;
end;

:: deftheorem Def4 defines homogeneous COMPUT_1:def 4 :
for f being Relation holds
( f is homogeneous iff for x, y being FinSequence st x in dom f & y in dom f holds
len x = len y );

theorem Th19: :: COMPUT_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for D being non empty set
for R being Relation st dom R c= n -tuples_on D holds
R is homogeneous
proof end;

registration
cluster {} -> homogeneous ;
coherence
{} is homogeneous
proof end;
end;

registration
let p be FinSequence;
let x be set ;
cluster K256({p},x) -> non empty homogeneous ;
coherence
( not {p} --> x is empty & {p} --> x is homogeneous )
proof end;
end;

registration
cluster non empty homogeneous set ;
existence
ex b1 being Function st
( not b1 is empty & b1 is homogeneous )
proof end;
end;

registration
let f be homogeneous Function;
let g be Function;
cluster f * g -> homogeneous ;
coherence
g * f is homogeneous
proof end;
end;

registration
let X, Y be set ;
cluster homogeneous Relation of X * ,Y;
existence
ex b1 being PartFunc of X * ,Y st b1 is homogeneous
proof end;
end;

registration
let X, Y be non empty set ;
cluster non empty homogeneous Relation of X * ,Y;
existence
ex b1 being PartFunc of X * ,Y st
( not b1 is empty & b1 is homogeneous )
proof end;
end;

registration
let X be non empty set ;
cluster non empty quasi_total homogeneous Relation of X * ,X;
existence
ex b1 being PartFunc of X * ,X st
( not b1 is empty & b1 is homogeneous & b1 is quasi_total )
proof end;
end;

registration
cluster non empty to-naturals from-natural-fseqs len-total homogeneous set ;
existence
ex b1 being from-natural-fseqs Function st
( not b1 is empty & b1 is homogeneous & b1 is to-naturals & b1 is len-total )
proof end;
end;

registration
cluster -> to-naturals from-natural-fseqs Relation of NAT * , NAT ;
coherence
for b1 being PartFunc of NAT * , NAT holds
( b1 is to-naturals & b1 is from-natural-fseqs )
proof end;
end;

registration
cluster quasi_total -> to-naturals from-natural-fseqs len-total Relation of NAT * , NAT ;
coherence
for b1 being PartFunc of NAT * , NAT st b1 is quasi_total holds
b1 is len-total
proof end;
end;

theorem Th20: :: COMPUT_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for g being to-naturals from-natural-fseqs len-total Function holds g is quasi_total PartFunc of NAT * , NAT
proof end;

definition
let f be homogeneous Relation;
func arity f -> Nat means :Def5: :: COMPUT_1:def 5
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
( ( ex x being FinSequence st x in dom f implies ex b1 being Nat st
for x being FinSequence st x in dom f holds
b1 = len x ) & ( ( for x being FinSequence holds not x in dom f ) implies ex b1 being Nat st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Nat holds
( ( ex x being FinSequence st x in dom f & ( for x being FinSequence st x in dom f holds
b1 = len x ) & ( for x being FinSequence st x in dom f holds
b2 = len x ) implies b1 = b2 ) & ( ( for x being FinSequence holds not x in dom f ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being Nat holds verum
;
;
end;

:: deftheorem Def5 defines arity COMPUT_1:def 5 :
for f being homogeneous Relation
for b2 being Nat holds
( ( ex x being FinSequence st x in dom f implies ( b2 = arity f iff for x being FinSequence st x in dom f holds
b2 = len x ) ) & ( ( for x being FinSequence holds not x in dom f ) implies ( b2 = arity f iff b2 = 0 ) ) );

theorem Th21: :: COMPUT_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
arity {} = 0
proof end;

theorem Th22: :: COMPUT_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being homogeneous Relation st dom f = {{} } holds
arity f = 0
proof end;

theorem Th23: :: COMPUT_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for f being homogeneous PartFunc of X * ,Y holds dom f c= (arity f) -tuples_on X
proof end;

theorem Th24: :: COMPUT_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being from-natural-fseqs homogeneous Function holds dom f c= (arity f) -tuples_on NAT
proof end;

Lm1: for D being non empty set
for f being homogeneous PartFunc of D * ,D holds
( ( f is quasi_total & not f is empty ) iff dom f = (arity f) -tuples_on D )
proof end;

theorem Th25: :: COMPUT_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for f being homogeneous PartFunc of X * ,X holds
( ( f is quasi_total & not f is empty ) iff dom f = (arity f) -tuples_on X )
proof end;

theorem Th26: :: COMPUT_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being to-naturals from-natural-fseqs homogeneous Function holds
( ( f is len-total & not f is empty ) iff dom f = (arity f) -tuples_on NAT )
proof end;

theorem :: COMPUT_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being non empty homogeneous PartFunc of D * ,D
for n being Nat st dom f c= n -tuples_on D holds
arity f = n
proof end;

theorem Th28: :: COMPUT_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being homogeneous PartFunc of D * ,D
for n being Nat st dom f = n -tuples_on D holds
arity f = n
proof end;

definition
let R be Relation;
attr R is with_the_same_arity means :Def6: :: COMPUT_1:def 6
for f, g being Function st f in rng R & g in rng R holds
( ( not f is empty or g is empty or dom g = {{} } ) & ( not f is empty & not g is empty implies ex n being Nat ex X being non empty set st
( dom f c= n -tuples_on X & dom g c= n -tuples_on X ) ) );
end;

:: deftheorem Def6 defines with_the_same_arity COMPUT_1:def 6 :
for R being Relation holds
( R is with_the_same_arity iff for f, g being Function st f in rng R & g in rng R holds
( ( not f is empty or g is empty or dom g = {{} } ) & ( not f is empty & not g is empty implies ex n being Nat ex X being non empty set st
( dom f c= n -tuples_on X & dom g c= n -tuples_on X ) ) ) );

registration
cluster {} -> homogeneous with_the_same_arity ;
coherence
{} is with_the_same_arity
proof end;
end;

registration
cluster with_the_same_arity set ;
existence
ex b1 being FinSequence st b1 is with_the_same_arity
proof end;
let X be set ;
cluster with_the_same_arity FinSequence of X;
existence
ex b1 being FinSequence of X st b1 is with_the_same_arity
proof end;
cluster with_the_same_arity Element of X * ;
existence
ex b1 being Element of X * st b1 is with_the_same_arity
proof end;
end;

definition
let F be with_the_same_arity Relation;
func arity F -> Nat means :Def7: :: COMPUT_1:def 7
for f being homogeneous Function st f in rng F holds
it = arity f if ex f being homogeneous Function st f in rng F
otherwise it = 0;
existence
( ( ex f being homogeneous Function st f in rng F implies ex b1 being Nat st
for f being homogeneous Function st f in rng F holds
b1 = arity f ) & ( ( for f being homogeneous Function holds not f in rng F ) implies ex b1 being Nat st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Nat holds
( ( ex f being homogeneous Function st f in rng F & ( for f being homogeneous Function st f in rng F holds
b1 = arity f ) & ( for f being homogeneous Function st f in rng F holds
b2 = arity f ) implies b1 = b2 ) & ( ( for f being homogeneous Function holds not f in rng F ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being Nat holds verum
;
;
end;

:: deftheorem Def7 defines arity COMPUT_1:def 7 :
for F being with_the_same_arity Relation
for b2 being Nat holds
( ( ex f being homogeneous Function st f in rng F implies ( b2 = arity F iff for f being homogeneous Function st f in rng F holds
b2 = arity f ) ) & ( ( for f being homogeneous Function holds not f in rng F ) implies ( b2 = arity F iff b2 = 0 ) ) );

theorem :: COMPUT_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being with_the_same_arity FinSequence st len F = 0 holds
arity F = 0
proof end;

definition
let X be set ;
func HFuncs X -> PFUNC_DOMAIN of X * ,X equals :: COMPUT_1:def 8
{ f where f is Element of PFuncs (X * ),X : f is homogeneous } ;
coherence
{ f where f is Element of PFuncs (X * ),X : f is homogeneous } is PFUNC_DOMAIN of X * ,X
proof end;
end;

:: deftheorem defines HFuncs COMPUT_1:def 8 :
for X being set holds HFuncs X = { f where f is Element of PFuncs (X * ),X : f is homogeneous } ;

theorem Th30: :: COMPUT_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds {} in HFuncs X
proof end;

registration
let X be non empty set ;
cluster non empty quasi_total homogeneous Element of HFuncs X;
existence
ex b1 being Element of HFuncs X st
( not b1 is empty & b1 is homogeneous & b1 is quasi_total )
proof end;
end;

registration
let X be set ;
cluster -> homogeneous Element of HFuncs X;
coherence
for b1 being Element of HFuncs X holds b1 is homogeneous
proof end;
end;

registration
let X be non empty set ;
let S be non empty Subset of (HFuncs X);
cluster -> homogeneous Element of S;
coherence
for b1 being Element of S holds b1 is homogeneous
proof end;
end;

theorem Th31: :: COMPUT_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being to-naturals from-natural-fseqs homogeneous Function holds f is Element of HFuncs NAT
proof end;

theorem Th32: :: COMPUT_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being to-naturals from-natural-fseqs len-total homogeneous Function holds f is quasi_total Element of HFuncs NAT
proof end;

theorem Th33: :: COMPUT_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for F being Relation st rng F c= HFuncs X & ( for f, g being homogeneous Function st f in rng F & g in rng F holds
arity f = arity g ) holds
F is with_the_same_arity
proof end;

definition
let n, m be Nat;
func n const m -> to-naturals from-natural-fseqs homogeneous Function equals :: COMPUT_1:def 9
(n -tuples_on NAT ) --> m;
coherence
(n -tuples_on NAT ) --> m is to-naturals from-natural-fseqs homogeneous Function
proof end;
end;

:: deftheorem defines const COMPUT_1:def 9 :
for n, m being Nat holds n const m = (n -tuples_on NAT ) --> m;

theorem Th34: :: COMPUT_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat holds n const m in HFuncs NAT
proof end;

registration
let n, m be Nat;
cluster n const m -> non empty to-naturals from-natural-fseqs len-total homogeneous ;
coherence
( n const m is len-total & not n const m is empty )
proof end;
end;

theorem Th35: :: COMPUT_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat holds arity (n const m) = n
proof end;

theorem Th36: :: COMPUT_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat
for t being Element of n -tuples_on NAT holds (n const m) . t = m by FUNCOP_1:13;

definition
let n, i be Nat;
func n succ i -> to-naturals from-natural-fseqs homogeneous Function means :Def10: :: COMPUT_1:def 10
( dom it = n -tuples_on NAT & ( for p being Element of n -tuples_on NAT holds it . p = (p /. i) + 1 ) );
existence
ex b1 being to-naturals from-natural-fseqs homogeneous Function st
( dom b1 = n -tuples_on NAT & ( for p being Element of n -tuples_on NAT holds b1 . p = (p /. i) + 1 ) )
proof end;
uniqueness
for b1, b2 being to-naturals from-natural-fseqs homogeneous Function st dom b1 = n -tuples_on NAT & ( for p being Element of n -tuples_on NAT holds b1 . p = (p /. i) + 1 ) & dom b2 = n -tuples_on NAT & ( for p being Element of n -tuples_on NAT holds b2 . p = (p /. i) + 1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines succ COMPUT_1:def 10 :
for n, i being Nat
for b3 being to-naturals from-natural-fseqs homogeneous Function holds
( b3 = n succ i iff ( dom b3 = n -tuples_on NAT & ( for p being Element of n -tuples_on NAT holds b3 . p = (p /. i) + 1 ) ) );

theorem Th37: :: COMPUT_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat holds n succ i in HFuncs NAT
proof end;

registration
let n, i be Nat;
cluster n succ i -> non empty to-naturals from-natural-fseqs len-total homogeneous ;
coherence
( n succ i is len-total & not n succ i is empty )
proof end;
end;

theorem Th38: :: COMPUT_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat holds arity (n succ i) = n
proof end;

definition
let n, i be Nat;
func n proj i -> to-naturals from-natural-fseqs homogeneous Function equals :: COMPUT_1:def 11
proj (n |-> NAT ),i;
correctness
coherence
proj (n |-> NAT ),i is to-naturals from-natural-fseqs homogeneous Function
;
proof end;
end;

:: deftheorem defines proj COMPUT_1:def 11 :
for n, i being Nat holds n proj i = proj (n |-> NAT ),i;

theorem Th39: :: COMPUT_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat holds n proj i in HFuncs NAT
proof end;

theorem Th40: :: COMPUT_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat holds
( dom (n proj i) = n -tuples_on NAT & ( 1 <= i & i <= n implies rng (n proj i) = NAT ) )
proof end;

registration
let n, i be Nat;
cluster n proj i -> non empty to-naturals from-natural-fseqs len-total homogeneous ;
coherence
( n proj i is len-total & not n proj i is empty )
proof end;
end;

theorem Th41: :: COMPUT_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat holds arity (n proj i) = n
proof end;

theorem Th42: :: COMPUT_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat
for t being Element of n -tuples_on NAT holds (n proj i) . t = t . i
proof end;

registration
let X be set ;
cluster HFuncs X -> functional ;
coherence
HFuncs X is functional
;
end;

theorem Th43: :: COMPUT_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for D, E being non empty set
for F being Function of D, HFuncs E st rng F is compatible & ( for x being Element of D holds dom (F . x) c= n -tuples_on E ) holds
ex f being Element of HFuncs E st
( f = Union F & dom f c= n -tuples_on E )
proof end;

theorem :: COMPUT_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being Function of NAT , HFuncs D st ( for i being Nat holds F . i c= F . (i + 1) ) holds
Union F in HFuncs D
proof end;

theorem Th45: :: COMPUT_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being with_the_same_arity FinSequence of HFuncs D holds dom <:F:> c= (arity F) -tuples_on D
proof end;

registration
let X be non empty set ;
let F be with_the_same_arity FinSequence of HFuncs X;
cluster <:F:> -> homogeneous ;
coherence
<:F:> is homogeneous
proof end;
end;

theorem Th46: :: COMPUT_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being Element of HFuncs D
for F being with_the_same_arity FinSequence of HFuncs D holds
( dom (f * <:F:>) c= (arity F) -tuples_on D & rng (f * <:F:>) c= D & f * <:F:> in HFuncs D )
proof end;

definition
let X, Y be non empty set ;
let P be PFUNC_DOMAIN of X,Y;
let S be non empty Subset of P;
:: original: Element
redefine mode Element of S -> Element of P;
coherence
for b1 being Element of S holds b1 is Element of P
proof end;
end;

registration
let f be from-natural-fseqs homogeneous Function;
cluster <*f*> -> with_the_same_arity ;
coherence
<*f*> is with_the_same_arity
proof end;
end;

theorem :: COMPUT_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being to-naturals from-natural-fseqs homogeneous Function holds arity <*f*> = arity f
proof end;

theorem Th48: :: COMPUT_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being non empty Element of HFuncs NAT
for F being with_the_same_arity FinSequence of HFuncs NAT st g = f * <:F:> holds
arity g = arity F
proof end;

theorem Th49: :: COMPUT_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being non empty quasi_total Element of HFuncs D
for F being with_the_same_arity FinSequence of HFuncs D st arity f = len F & not F is empty & ( for h being Element of HFuncs D st h in rng F holds
( h is quasi_total & not h is empty ) ) holds
( f * <:F:> is non empty quasi_total Element of HFuncs D & dom (f * <:F:>) = (arity F) -tuples_on D )
proof end;

theorem Th50: :: COMPUT_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being quasi_total Element of HFuncs D
for F being with_the_same_arity FinSequence of HFuncs D st arity f = len F & ( for h being Element of HFuncs D st h in rng F holds
h is quasi_total ) holds
f * <:F:> is quasi_total Element of HFuncs D
proof end;

theorem Th51: :: COMPUT_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f, g being non empty quasi_total Element of HFuncs D st arity f = 0 & arity g = 0 & f . {} = g . {} holds
f = g
proof end;

theorem Th52: :: COMPUT_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being non empty to-naturals from-natural-fseqs len-total homogeneous Function st arity f = 0 & arity g = 0 & f . {} = g . {} holds
f = g
proof end;

definition
let g, f1, f2 be to-naturals from-natural-fseqs homogeneous Function;
let i be Nat;
pred g is_primitive-recursively_expressed_by f1,f2,i means :Def12: :: COMPUT_1:def 12
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 implies Del p,i in dom f1 ) & ( Del p,i in dom f1 implies p +* i,0 in dom g ) & ( p +* i,0 in dom g implies g . (p +* i,0) = f1 . (Del p,i) ) & ( for n being Nat holds
( ( p +* i,(n + 1) in dom g implies ( p +* i,n in dom g & (p +* i,n) ^ <*(g . (p +* i,n))*> in dom f2 ) ) & ( p +* i,n in dom g & (p +* i,n) ^ <*(g . (p +* i,n))*> in dom f2 implies p +* i,(n + 1) in dom g ) & ( p +* i,(n + 1) in dom g implies g . (p +* i,(n + 1)) = f2 . ((p +* i,n) ^ <*(g . (p +* i,n))*>) ) ) ) ) ) );
end;

:: deftheorem Def12 defines is_primitive-recursively_expressed_by COMPUT_1:def 12 :
for g, f1, f2 being to-naturals from-natural-fseqs homogeneous Function
for i being Nat holds
( g is_primitive-recursively_expressed_by f1,f2,i iff 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 implies Del p,i in dom f1 ) & ( Del p,i in dom f1 implies p +* i,0 in dom g ) & ( p +* i,0 in dom g implies g . (p +* i,0) = f1 . (Del p,i) ) & ( for n being Nat holds
( ( p +* i,(n + 1) in dom g implies ( p +* i,n in dom g & (p +* i,n) ^ <*(g . (p +* i,n))*> in dom f2 ) ) & ( p +* i,n in dom g & (p +* i,n) ^ <*(g . (p +* i,n))*> in dom f2 implies p +* i,(n + 1) in dom g ) & ( p +* i,(n + 1) in dom g implies g . (p +* i,(n + 1)) = f2 . ((p +* i,n) ^ <*(g . (p +* i,n))*>) ) ) ) ) ) ) );

defpred S1[ 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 to-naturals from-natural-fseqs homogeneous Function;
let i be Nat;
let p be FinSequence of NAT ;
func primrec f1,f2,i,p -> Element of HFuncs NAT means :Def13: :: COMPUT_1:def 13
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
ex b1 being Element of HFuncs NAT ex F being Function of NAT , HFuncs NAT st
( b1 = F . (p /. i) & ( i in dom p & Del p,i in dom f1 implies F . 0 = {(p +* i,0)} --> (f1 . (Del p,i)) ) & ( ( not i in dom p or not Del p,i in dom f1 ) implies F . 0 = {} ) & ( for m being 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 ) ) ) )
proof end;
uniqueness
for b1, b2 being Element of HFuncs NAT st ex F being Function of NAT , HFuncs NAT st
( b1 = F . (p /. i) & ( i in dom p & Del p,i in dom f1 implies F . 0 = {(p +* i,0)} --> (f1 . (Del p,i)) ) & ( ( not i in dom p or not Del p,i in dom f1 ) implies F . 0 = {} ) & ( for m being Nat holds
( ( i in dom p & p +* i,m in dom (F . m) & (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom f2 implies F . (m + 1) = (F . m) +* ({(p +* i,(m + 1))} --> (f2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>))) ) & ( ( not i in dom p or not p +* i,m in dom (F . m) or not (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom f2 ) implies F . (m + 1) = F . m ) ) ) ) & ex F being Function of NAT , HFuncs NAT st
( b2 = F . (p /. i) & ( i in dom p & Del p,i in dom f1 implies F . 0 = {(p +* i,0)} --> (f1 . (Del p,i)) ) & ( ( not i in dom p or not Del p,i in dom f1 ) implies F . 0 = {} ) & ( for m being Nat holds
( ( i in dom p & p +* i,m in dom (F . m) & (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom f2 implies F . (m + 1) = (F . m) +* ({(p +* i,(m + 1))} --> (f2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>))) ) & ( ( not i in dom p or not p +* i,m in dom (F . m) or not (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom f2 ) implies F . (m + 1) = F . m ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines primrec COMPUT_1:def 13 :
for f1, f2 being to-naturals from-natural-fseqs homogeneous Function
for i being Nat
for p being FinSequence of NAT
for b5 being Element of HFuncs NAT holds
( b5 = primrec f1,f2,i,p iff ex F being Function of NAT , HFuncs NAT st
( b5 = F . (p /. i) & ( i in dom p & Del p,i in dom f1 implies F . 0 = {(p +* i,0)} --> (f1 . (Del p,i)) ) & ( ( not i in dom p or not Del p,i in dom f1 ) implies F . 0 = {} ) & ( for m being Nat holds
( ( i in dom p & p +* i,m in dom (F . m) & (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom f2 implies F . (m + 1) = (F . m) +* ({(p +* i,(m + 1))} --> (f2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>))) ) & ( ( not i in dom p or not p +* i,m in dom (F . m) or not (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom f2 ) implies F . (m + 1) = F . m ) ) ) ) );

theorem Th53: :: COMPUT_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for e1, e2 being to-naturals from-natural-fseqs homogeneous Function
for p, q being FinSequence of NAT st q in dom (primrec e1,e2,i,p) holds
ex k being Nat st q = p +* i,k
proof end;

theorem Th54: :: COMPUT_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for e1, e2 being to-naturals from-natural-fseqs homogeneous Function
for p being FinSequence of NAT st not i in dom p holds
primrec e1,e2,i,p = {}
proof end;

theorem Th55: :: COMPUT_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for e1, e2 being to-naturals from-natural-fseqs homogeneous Function
for p, q being FinSequence of NAT holds primrec e1,e2,i,p tolerates primrec e1,e2,i,q
proof end;

theorem Th56: :: COMPUT_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for e1, e2 being to-naturals from-natural-fseqs homogeneous Function
for p being FinSequence of NAT holds dom (primrec e1,e2,i,p) c= (1 + (arity e1)) -tuples_on NAT
proof end;

theorem Th57: :: COMPUT_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for e1, e2 being to-naturals from-natural-fseqs homogeneous Function
for p being FinSequence of NAT st e1 is empty holds
primrec e1,e2,i,p is empty
proof end;

theorem Th58: :: COMPUT_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for f1, f2 being non empty to-naturals from-natural-fseqs homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st f1 is len-total & f2 is len-total & (arity f1) + 2 = arity f2 & 1 <= i & i <= 1 + (arity f1) holds
p in dom (primrec f1,f2,i,p)
proof end;

definition
let f1, f2 be to-naturals from-natural-fseqs homogeneous Function;
let i be Nat;
func primrec f1,f2,i -> Element of HFuncs NAT means :Def14: :: COMPUT_1:def 14
ex G being Function of ((arity f1) + 1) -tuples_on NAT , HFuncs NAT st
( it = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ) );
existence
ex b1 being Element of HFuncs NAT ex G being Function of ((arity f1) + 1) -tuples_on NAT , HFuncs NAT st
( b1 = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ) )
proof end;
uniqueness
for b1, b2 being Element of HFuncs NAT st ex G being Function of ((arity f1) + 1) -tuples_on NAT , HFuncs NAT st
( b1 = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ) ) & ex G being Function of ((arity f1) + 1) -tuples_on NAT , HFuncs NAT st
( b2 = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines primrec COMPUT_1:def 14 :
for f1, f2 being to-naturals from-natural-fseqs homogeneous Function
for i being Nat
for b4 being Element of HFuncs NAT holds
( b4 = primrec f1,f2,i iff ex G being Function of ((arity f1) + 1) -tuples_on NAT , HFuncs NAT st
( b4 = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ) ) );

theorem Th59: :: COMPUT_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for e1, e2 being to-naturals from-natural-fseqs homogeneous Function st e1 is empty holds
primrec e1,e2,i is empty
proof end;

theorem Th60: :: COMPUT_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for f1, f2 being non empty to-naturals from-natural-fseqs homogeneous Function holds dom (primrec f1,f2,i) c= ((arity f1) + 1) -tuples_on NAT
proof end;

theorem Th61: :: COMPUT_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for f1, f2 being non empty to-naturals from-natural-fseqs homogeneous Function st f1 is len-total & f2 is len-total & (arity f1) + 2 = arity f2 & 1 <= i & i <= 1 + (arity f1) holds
( dom (primrec f1,f2,i) = ((arity f1) + 1) -tuples_on NAT & arity (primrec f1,f2,i) = (arity f1) + 1 )
proof end;

Lm2: now
let f1, f2 be non empty to-naturals from-natural-fseqs homogeneous Function; :: thesis: for p being Element of ((arity f1) + 1) -tuples_on NAT
for i, m being Nat
for F1, F being Function of NAT , HFuncs NAT st ( i in dom (p +* i,(m + 1)) & Del (p +* i,(m + 1)),i in dom f1 implies F1 . 0 = {((p +* i,(m + 1)) +* i,0)} --> (f1 . (Del (p +* i,(m + 1)),i)) ) & ( ( not i in dom (p +* i,(m + 1)) or not Del (p +* i,(m + 1)),i in dom f1 ) implies F1 . 0 = {} ) & ( for M being Nat holds S1[M,F1 . M,F1 . (M + 1),p +* i,(m + 1),i,f2] ) & ( i in dom (p +* i,m) & Del (p +* i,m),i in dom f1 implies F . 0 = {((p +* i,m) +* i,0)} --> (f1 . (Del (p +* i,m),i)) ) & ( ( not i in dom (p +* i,m) or not Del (p +* i,m),i in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* i,m,i,f2] ) holds
F1 = F

let p be Element of ((arity f1) + 1) -tuples_on NAT ; :: thesis: for i, m being Nat
for F1, F being Function of NAT , HFuncs NAT st ( i in dom (p +* i,(m + 1)) & Del (p +* i,(m + 1)),i in dom f1 implies F1 . 0 = {((p +* i,(m + 1)) +* i,0)} --> (f1 . (Del (p +* i,(m + 1)),i)) ) & ( ( not i in dom (p +* i,(m + 1)) or not Del (p +* i,(m + 1)),i in dom f1 ) implies F1 . 0 = {} ) & ( for M being Nat holds S1[M,F1 . M,F1 . (M + 1),p +* i,(m + 1),i,f2] ) & ( i in dom (p +* i,m) & Del (p +* i,m),i in dom f1 implies F . 0 = {((p +* i,m) +* i,0)} --> (f1 . (Del (p +* i,m),i)) ) & ( ( not i in dom (p +* i,m) or not Del (p +* i,m),i in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* i,m,i,f2] ) holds
F1 = F

let i, m be Nat; :: thesis: for F1, F being Function of NAT , HFuncs NAT st ( i in dom (p +* i,(m + 1)) & Del (p +* i,(m + 1)),i in dom f1 implies F1 . 0 = {((p +* i,(m + 1)) +* i,0)} --> (f1 . (Del (p +* i,(m + 1)),i)) ) & ( ( not i in dom (p +* i,(m + 1)) or not Del (p +* i,(m + 1)),i in dom f1 ) implies F1 . 0 = {} ) & ( for M being Nat holds S1[M,F1 . M,F1 . (M + 1),p +* i,(m + 1),i,f2] ) & ( i in dom (p +* i,m) & Del (p +* i,m),i in dom f1 implies F . 0 = {((p +* i,m) +* i,0)} --> (f1 . (Del (p +* i,m),i)) ) & ( ( not i in dom (p +* i,m) or not Del (p +* i,m),i in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* i,m,i,f2] ) holds
F1 = F

set pm1 = p +* i,(m + 1);
set pm = p +* i,m;
let F1, F be Function of NAT , HFuncs NAT ; :: thesis: ( ( i in dom (p +* i,(m + 1)) & Del (p +* i,(m + 1)),i in dom f1 implies F1 . 0 = {((p +* i,(m + 1)) +* i,0)} --> (f1 . (Del (p +* i,(m + 1)),i)) ) & ( ( not i in dom (p +* i,(m + 1)) or not Del (p +* i,(m + 1)),i in dom f1 ) implies F1 . 0 = {} ) & ( for M being Nat holds S1[M,F1 . M,F1 . (M + 1),p +* i,(m + 1),i,f2] ) & ( i in dom (p +* i,m) & Del (p +* i,m),i in dom f1 implies F . 0 = {((p +* i,m) +* i,0)} --> (f1 . (Del (p +* i,m),i)) ) & ( ( not i in dom (p +* i,m) or not Del (p +* i,m),i in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* i,m,i,f2] ) implies F1 = F )
assume that
A1: ( ( i in dom (p +* i,(m + 1)) & Del (p +* i,(m + 1)),i in dom f1 implies F1 . 0 = {((p +* i,(m + 1)) +* i,0)} --> (f1 . (Del (p +* i,(m + 1)),i)) ) & ( ( not i in dom (p +* i,(m + 1)) or not Del (p +* i,(m + 1)),i in dom f1 ) implies F1 . 0 = {} ) ) and
A2: for M being Nat holds S1[M,F1 . M,F1 . (M + 1),p +* i,(m + 1),i,f2] and
A3: ( ( i in dom (p +* i,m) & Del (p +* i,m),i in dom f1 implies F . 0 = {((p +* i,m) +* i,0)} --> (f1 . (Del (p +* i,m),i)) ) & ( ( not i in dom (p +* i,m) or not Del (p +* i,m),i in dom f1 ) implies F . 0 = {} ) ) and
A4: for M being Nat holds S1[M,F . M,F . (M + 1),p +* i,m,i,f2] ; :: thesis: F1 = F
A5: ( dom p = dom (p +* i,m) & dom p = dom (p +* i,(m + 1)) ) by FUNCT_7:32;
A6: (p +* i,m) +* i,0 = p +* i,0 by FUNCT_7:36
.= (p +* i,(m + 1)) +* i,0 by FUNCT_7:36 ;
A7: Del (p +* i,m),i = Del p,i by Th6
.= Del (p +* i,(m + 1)),i by Th6 ;
for x being set st x in NAT holds
F . x = F1 . x
proof
defpred S2[ Nat] means F . $1 = F1 . $1;
A8: S2[0] by A1, A3, A5, A6, A7;
A9: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A10: S2[k] ; :: thesis: S2[k + 1]
A11: (p +* i,m) +* i,k = p +* i,k by FUNCT_7:36
.= (p +* i,(m + 1)) +* i,k by FUNCT_7:36 ;
A12: (p +* i,m) +* i,(k + 1) = p +* i,(k + 1) by FUNCT_7:36
.= (p +* i,(m + 1)) +* i,(k + 1) by FUNCT_7:36 ;
per cases ( ( i in dom (p +* i,m) & (p +* i,m) +* i,k in dom (F . k) & ((p +* i,m) +* i,k) ^ <*((F . k) . ((p +* i,m) +* i,k))*> in dom f2 ) or not i in dom (p +* i,m) or not (p +* i,m) +* i,k in dom (F . k) or not ((p +* i,m) +* i,k) ^ <*((F . k) . ((p +* i,m) +* i,k))*> in dom f2 ) ;
suppose A13: ( i in dom (p +* i,m) & (p +* i,m) +* i,k in dom (F . k) & ((p +* i,m) +* i,k) ^ <*((F . k) . ((p +* i,m) +* i,k))*> in dom f2 ) ; :: thesis: S2[k + 1]
hence F . (k + 1) = (F . k) +* ({((p +* i,m) +* i,(k + 1))} --> (f2 . (((p +* i,m) +* i,k) ^ <*((F . k) . ((p +* i,m) +* i,k))*>))) by A4
.= F1 . (k + 1) by A2, A5, A10, A11, A12, A13 ;
:: thesis: verum
end;
suppose A14: ( not i in dom (p +* i,m) or not (p +* i,m) +* i,k in dom (F . k) or not ((p +* i,m) +* i,k) ^ <*((F . k) . ((p +* i,m) +* i,k))*> in dom f2 ) ; :: thesis: S2[k + 1]
hence F . (k + 1) = F . k by A4
.= F1 . (k + 1) by A2, A5, A10, A11, A14 ;
:: thesis: verum
end;
end;
end;
A15: for k being Nat holds S2[k] from NAT_1:sch 1(, A8, A9);
let x be set ; :: thesis: ( x in NAT implies F . x = F1 . x )
assume x in NAT ; :: thesis: F . x = F1 . x
hence F . x = F1 . x by A15; :: thesis: verum
end;
hence F1 = F by FUNCT_2:18; :: thesis: verum
end;

Lm3: now
let f1, f2 be non empty to-naturals from-natural-fseqs homogeneous Function; :: thesis: for p being Element of ((arity f1) + 1) -tuples_on NAT
for i, m being Nat st i in dom p holds
for F being Function of NAT , HFuncs NAT st ( i in dom (p +* i,(m + 1)) & Del (p +* i,(m + 1)),i in dom f1 implies F . 0 = {((p +* i,(m + 1)) +* i,0)} --> (f1 . (Del (p +* i,(m + 1)),i)) ) & ( ( not i in dom (p +* i,(m + 1)) or not Del (p +* i,(m + 1)),i in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* i,(m + 1),i,f2] ) holds
( (F . (m + 1)) . (p +* i,m) = (F . m) . (p +* i,m) & not p +* i,(m + 1) in dom (F . m) )

let p be Element of ((arity f1) + 1) -tuples_on NAT ; :: thesis: for i, m being Nat st i in dom p holds
for F being Function of NAT , HFuncs NAT st ( i in dom (p +* i,(m + 1)) & Del (p +* i,(m + 1)),i in dom f1 implies F . 0 = {((p +* i,(m + 1)) +* i,0)} --> (f1 . (Del (p +* i,(m + 1)),i)) ) & ( ( not i in dom (p +* i,(m + 1)) or not Del (p +* i,(m + 1)),i in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* i,(m + 1),i,f2] ) holds
( (F . (m + 1)) . (p +* i,m) = (F . m) . (p +* i,m) & not p +* i,(m + 1) in dom (F . m) )

let i, m be Nat; :: thesis: ( i in dom p implies for F being Function of NAT , HFuncs NAT st ( i in dom (p +* i,(m + 1)) & Del (p +* i,(m + 1)),i in dom f1 implies F . 0 = {((p +* i,(m + 1)) +* i,0)} --> (f1 . (Del (p +* i,(m + 1)),i)) ) & ( ( not i in dom (p +* i,(m + 1)) or not Del (p +* i,(m + 1)),i in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* i,(m + 1),i,f2] ) holds
( (F . (m + 1)) . (p +* i,m) = (F . m) . (p +* i,m) & not p +* i,(m + 1) in dom (F . m) ) )

assume A1: i in dom p ; :: thesis: for F being Function of NAT , HFuncs NAT st ( i in dom (p +* i,(m + 1)) & Del (p +* i,(m + 1)),i in dom f1 implies F . 0 = {((p +* i,(m + 1)) +* i,0)} --> (f1 . (Del (p +* i,(m + 1)),i)) ) & ( ( not i in dom (p +* i,(m + 1)) or not Del (p +* i,(m + 1)),i in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* i,(m + 1),i,f2] ) holds
( (F . (m + 1)) . (p +* i,m) = (F . m) . (p +* i,m) & not p +* i,(m + 1) in dom (F . m) )

set pm = p +* i,m;
set pm1 = p +* i,(m + 1);
let F be Function of NAT , HFuncs NAT ; :: thesis: ( ( i in dom (p +* i,(m + 1)) & Del (p +* i,(m + 1)),i in dom f1 implies F . 0 = {((p +* i,(m + 1)) +* i,0)} --> (f1 . (Del (p +* i,(m + 1)),i)) ) & ( ( not i in dom (p +* i,(m + 1)) or not Del (p +* i,(m + 1)),i in dom f1 ) implies F . 0 = {} ) & ( for M being Nat holds S1[M,F . M,F . (M + 1),p +* i,(m + 1),i,f2] ) implies ( (F . (m + 1)) . (p +* i,m) = (F . m) . (p +* i,m) & not p +* i,(m + 1) in dom (F . m) ) )
assume that
A2: ( ( i in dom (p +* i,(m + 1)) & Del (p +* i,(m + 1)),i in dom f1 implies F . 0 = {((p +* i,(m + 1)) +* i,0)} --> (f1 . (Del (p +* i,(m + 1)),i)) ) & ( ( not i in dom (p +* i,(m + 1)) or not Del (p +* i,(m + 1)),i in dom f1 ) implies F . 0 = {} ) ) and
A3: for M being Nat holds S1[M,F . M,F . (M + 1),p +* i,(m + 1),i,f2] ; :: thesis: ( (F . (m + 1)) . (p +* i,m) = (F . m) . (p +* i,m) & not p +* i,(m + 1) in dom (F . m) )
thus (F . (m + 1)) . (p +* i,m) = (F . m) . (p +* i,m) :: thesis: not p +* i,(m + 1) in dom (F . m)
proof
per cases ( ( i in dom (p +* i,(m + 1)) & (p +* i,(m + 1)) +* i,m in dom (F . m) & ((p +* i,(m + 1)) +* i,m) ^ <*((F . m) . ((p +* i,(m + 1)) +* i,m))*> in dom f2 ) or not i in dom (p +* i,(m + 1)) or not (p +* i,(m + 1)) +* i,m in dom (F . m) or not ((p +* i,(m + 1)) +* i,m) ^ <*((F . m) . ((p +* i,(m + 1)) +* i,m))*> in dom f2 ) ;
suppose ( i in dom (p +* i,(m + 1)) & (p +* i,(m + 1)) +* i,m in dom (F . m) & ((p +* i,(m + 1)) +* i,m) ^ <*((F . m) . ((p +* i,(m + 1)) +* i,m))*> in dom f2 ) ; :: thesis: (F . (m + 1)) . (p +* i,m) = (F . m) . (p +* i,m)
then A4: F . (m + 1) = (F . m) +* ({((p +* i,(m + 1)) +* i,(m + 1))} --> (f2 . (((p +* i,(m + 1)) +* i,m) ^ <*((F . m) . ((p +* i,(m + 1)) +* i,m))*>))) by A3;
( (p +* i,m) . i = m & (p +* i,(m + 1)) . i = m + 1 ) by A1, FUNCT_7:33;
then ( p +* i,m <> p +* i,(m + 1) & p +* i,(m + 1) = (p +* i,(m + 1)) +* i,(m + 1) ) by FUNCT_7:36;
then not p +* i,m in {((p +* i,(m + 1)) +* i,(m + 1))} by TARSKI:def 1;
then not p +* i,m in dom ({((p +* i,(m + 1)) +* i,(m + 1))} --> (f2 . (((p +* i,(m + 1)) +* i,m) ^ <*((F . m) . ((p +* i,(m + 1)) +* i,m))*>))) by FUNCOP_1:19;
hence (F . (m + 1)) . (p +* i,m) = (F . m) . (p +* i,m) by A4, FUNCT_4:12; :: thesis: verum
end;
suppose ( not i in dom (p +* i,(m + 1)) or not (p +* i,(m + 1)) +* i,m in dom (F . m) or not ((p +* i,(m + 1)) +* i,m) ^ <*((F . m) . ((p +* i,(m + 1)) +* i,m))*> in dom f2 ) ; :: thesis: (F . (m + 1)) . (p +* i,m) = (F . m) . (p +* i,m)
hence (F . (m + 1)) . (p +* i,m) = (F . m) . (p +* i,m) by A3; :: thesis: verum
end;
end;
end;
A5: for m, k being Nat st p +* i,k in dom (F . m) holds
k <= m
proof
defpred S2[ Nat] means for k being Nat st p +* i,k in dom (F . $1) holds
k <= $1;
A6: S2[0]
proof
let k be Nat; :: thesis: ( p +* i,k in dom (F . 0) implies k <= 0 )
assume A7: p +* i,k in dom (F . 0) ; :: thesis: k <= 0
per cases ( ( i in dom (p +* i,(m + 1)) & Del (p +* i,(m + 1)),i in dom f1 ) or not i in dom (p +* i,(m + 1)) or not Del (p +* i,(m + 1)),i in dom f1 ) ;
suppose ( i in dom (p +* i,(m + 1)) & Del (p +* i,(m + 1)),i in dom f1 ) ; :: thesis: k <= 0
then dom (F . 0) = {((p +* i,(m + 1)) +* i,0)} by A2, FUNCOP_1:19;
then A8: p +* i,k = (p +* i,(m + 1)) +* 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 ; :: thesis: verum
end;
suppose ( not i in dom (p +* i,(m + 1)) or not Del (p +* i,(m + 1)),i in dom f1 ) ; :: thesis: k <= 0
hence k <= 0 by A2, A7, RELAT_1:60; :: thesis: verum
end;
end;
end;
A9: for m being Nat st S2[m] holds
S2[m + 1]
proof
let m be Nat; :: thesis: ( S2[m] implies S2[m + 1] )
assume A10: S2[m] ; :: thesis: S2[m + 1]
let k be Nat; :: thesis: ( p +* i,k in dom (F . (m + 1)) implies k <= m + 1 )
assume A11: p +* i,k in dom (F . (m + 1)) ; :: thesis: k <= m + 1
per cases ( ( i in dom (p +* i,(m + 1)) & (p +* i,(m + 1)) +* i,m in dom (F . m) & ((p +* i,(m + 1)) +* i,m) ^ <*((F . m) . ((p +* i,(m + 1)) +* i,m))*> in dom f2 ) or not i in dom (p +* i,(m + 1)) or not (p +* i,(m + 1)) +* i,m in dom (F . m) or not ((p +* i,(m + 1)) +* i,m) ^ <*((F . m) . ((p +* i,(m + 1)) +* i,m))*> in dom f2 ) ;
suppose ( i in dom (p +* i,(m + 1)) & (p +* i,(m + 1)) +* i,m in dom (F . m) & ((p +* i,(m + 1)) +* i,m) ^ <*((F . m) . ((p +* i,(m + 1)) +* i,m))*> in dom f2 ) ; :: thesis: k <= m + 1
then F . (m + 1) = (F . m) +* ({((p +* i,(m + 1)) +* i,(m + 1))} --> (f2 . (((p +* i,(m + 1)) +* i,m) ^ <*((F . m) . ((p +* i,(m + 1)) +* i,m))*>))) by A3;
then dom (F . (m + 1)) = (dom (F . m)) \/ (dom ({((p +* i,(m + 1)) +* i,(m + 1))} --> (f2 . (((p +* i,(m + 1)) +* i,m) ^ <*((F . m) . ((p +* i,(m + 1)) +* i,m))*>)))) by FUNCT_4:def 1;
then A12: dom (F . (m + 1)) = (dom (F . m)) \/ {((p +* i,(m + 1)) +* i,(m + 1))} by FUNCOP_1:19;
thus k <= m + 1 :: thesis: verum
proof
per cases ( p +* i,k in dom (F . m) or p +* i,k in {((p +* i,(m + 1)) +* i,(m + 1))} ) by A11, A12, XBOOLE_0:def 2;
suppose p +* i,k in dom (F . m) ; :: thesis: k <= m + 1
then ( k <= m & m <= m + 1 ) by A10, NAT_1:29;
hence k <= m + 1 by XREAL_1:2; :: thesis: verum
end;
suppose p +* i,k in {((p +* i,(m + 1)) +* i,(m + 1))} ; :: thesis: k <= m + 1
then A13: p +* i,k = (p +* i,(m + 1)) +* 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 ; :: thesis: verum
end;
end;
end;
end;
suppose ( not i in dom (p +* i,(m + 1)) or not (p +* i,(m + 1)) +* i,m in dom (F . m) or not ((p +* i,(m + 1)) +* i,m) ^ <*((F . m) . ((p +* i,(m + 1)) +* i,m))*> in dom f2 ) ; :: thesis: k <= m + 1
then F . (m + 1) = F . m by A3;
then ( k <= m & m <= m + 1 ) by A10, A11, NAT_1:29;
hence k <= m + 1 by XREAL_1:2; :: thesis: verum
end;
end;
end;
thus for n being Nat holds S2[n] from NAT_1:sch 1(, A6, A9); :: thesis: verum
end;
thus not p +* i,(m + 1) in dom (F . m) :: thesis: verum
proof
assume p +* i,(m + 1) in dom (F . m) ; :: thesis: contradiction
then m + 1 <= m by A5;
hence contradiction by NAT_1:38; :: thesis: verum
end;
end;

Lm4: now
let f1, f2 be non empty to-naturals from-natural-fseqs homogeneous Function; :: thesis: for p being Element of ((arity f1) + 1) -tuples_on NAT
for i, m being Nat st i in dom p holds
for G being Function of ((arity f1) + 1) -tuples_on NAT , HFuncs NAT st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ) holds
for k, n being Nat holds dom (G . (p +* i,k)) c= dom (G . (p +* i,(k + n)))

let p be Element of ((arity f1) + 1) -tuples_on NAT ; :: thesis: for i, m being Nat st i in dom p holds
for G being Function of ((arity f1) + 1) -tuples_on NAT , HFuncs NAT st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ) holds
for k, n being Nat holds dom (G . (p +* i,k)) c= dom (G . (p +* i,(k + n)))

let i, m be Nat; :: thesis: ( i in dom p implies for G being Function of ((arity f1) + 1) -tuples_on NAT , HFuncs NAT st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ) holds
for k, n being Nat holds dom (G . (p +* i,k)) c= dom (G . (p +* i,(k + n))) )

assume A1: i in dom p ; :: thesis: for G being Function of ((arity f1) + 1) -tuples_on NAT , HFuncs NAT st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ) holds
for k, n being Nat holds dom (G . (p +* i,k)) c= dom (G . (p +* i,(k + n)))

let G be Function of ((arity f1) + 1) -tuples_on NAT , HFuncs NAT ; :: thesis: ( ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ) implies for k, n being Nat holds dom (G . (p +* i,k)) c= dom (G . (p +* i,(k + n))) )
assume A2: for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ; :: thesis: for k, n being Nat holds dom (G . (p +* i,k)) c= dom (G . (p +* i,(k + n)))
thus for k, n being Nat holds dom (G . (p +* i,k)) c= dom (G . (p +* i,(k + n))) :: thesis: verum
proof
let k be Nat; :: thesis: for n being Nat holds dom (G . (p +* i,k)) c= dom (G . (p +* i,(k + n)))
set pk = p +* i,k;
defpred S2[ Nat] means dom (G . (p +* i,k)) c= dom (G . (p +* i,(k + $1)));
A3: S2[0] ;
A4: now
let n be Nat; :: thesis: ( S2[n] implies S2[b1 + 1] )
assume A5: S2[n] ; :: thesis: S2[b1 + 1]
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,(p +* i,(k + n)) = F . ((p +* i,(k + n)) /. i) and
A7: ( ( i in dom (p +* i,(k + n)) & Del (p +* i,(k + n)),i in dom f1 implies F . 0 = {((p +* i,(k + n)) +* i,0)} --> (f1 . (Del (p +* i,(k + n)),i)) ) & ( ( not i in dom (p +* i,(k + n)) or not Del (p +* i,(k + n)),i in dom f1 ) implies F . 0 = {} ) ) and
A8: for M being Nat holds S1[M,F . M,F . (M + 1),p +* i,(k + n),i,f2] by Def13;
consider F1 being Function of NAT , HFuncs NAT such that
A9: primrec f1,f2,i,(p +* i,((k + n) + 1)) = F1 . ((p +* i,((k + n) + 1)) /. i) and
A10: ( ( i in dom (p +* i,((k + n) + 1)) & Del (p +* i,((k + n) + 1)),i in dom f1 implies F1 . 0 = {((p +* i,((k + n) + 1)) +* i,0)} --> (f1 . (Del (p +* i,((k + n) + 1)),i)) ) & ( ( not i in dom (p +* i,((k + n) + 1)) or not Del (p +* i,((k + n) + 1)),i in dom f1 ) implies F1 . 0 = {} ) ) and
A11: for M being Nat holds S1[M,F1 . M,F1 . (M + 1),p +* i,((k + n) + 1),i,f2] by Def13;
A12: F1 = F by A7, A8, A10, A11, Lm2;
A13: ( dom p = dom (p +* i,k) & dom p = dom (p +* i,((k + n) + 1)) & dom p = dom (p +* i,(k + n)) ) by FUNCT_7:32;
then A14: (p +* i,((k + n) + 1)) /. i = (p +* i,((k + n) + 1)) . i by A1, FINSEQ_4:def 4
.= (k + n) + 1 by A1, FUNCT_7:33 ;
A15: (p +* i,(k + n)) /. i = (p +* i,(k + n)) . i by A1, A13, FINSEQ_4:def 4
.= k + n by A1, FUNCT_7:33 ;
A16: G . (p +* i,(k + (n + 1))) = F . ((k + n) + 1) by A2, A9, A12, A14;
A17: G . (p +* i,(k + n)) = F . (k + n) by A2, A6, A15;
per cases ( ( i in dom (p +* i,(k + n)) & (p +* i,(k + n)) +* i,(k + n) in dom (F . (k + n)) & ((p +* i,(k + n)) +* i,(k + n)) ^ <*((F . (k + n)) . ((p +* i,(k + n)) +* i,(k + n)))*> in dom f2 ) or not i in dom (p +* i,(k + n)) or not (p +* i,(k + n)) +* i,(k + n) in dom (F . (k + n)) or not ((p +* i,(k + n)) +* i,(k + n)) ^ <*((F . (k + n)) . ((p +* i,(k + n)) +* i,(k + n)))*> in dom f2 ) ;
suppose ( i in dom (p +* i,(k + n)) & (p +* i,(k + n)) +* i,(k + n) in dom (F . (k + n)) & ((p +* i,(k + n)) +* i,(k + n)) ^ <*((F . (k + n)) . ((p +* i,(k + n)) +* i,(k + n)))*> in dom f2 ) ; :: thesis: S2[b1 + 1]
then F . ((k + n) + 1) = (F . (k + n)) +* ({((p +* i,(k + n)) +* i,((k + n) + 1))} --> (f2 . (((p +* i,(k + n)) +* i,(k + n)) ^ <*((F . (k + n)) . ((p +* i,(k + n)) +* i,(k + n)))*>))) by A8;
then dom (F . ((k + n) + 1)) = (dom (F . (k + n))) \/ (dom ({((p +* i,(k + n)) +* i,((k + n) + 1))} --> (f2 . (((p +* i,(k + n)) +* i,(k + n)) ^ <*((F . (k + n)) . ((p +* i,(k + n)) +* i,(k + n)))*>)))) by FUNCT_4:def 1;
then dom (F . (k + n)) c= dom (F . ((k + n) + 1)) by XBOOLE_1:7;
hence S2[n + 1] by A5, A16, A17, XBOOLE_1:1; :: thesis: verum
end;
suppose ( not i in dom (p +* i,(k + n)) or not (p +* i,(k + n)) +* i,(k + n) in dom (F . (k + n)) or not ((p +* i,(k + n)) +* i,(k + n)) ^ <*((F . (k + n)) . ((p +* i,(k + n)) +* i,(k + n)))*> in dom f2 ) ; :: thesis: S2[b1 + 1]
hence S2[n + 1] by A5, A8, A16, A17; :: thesis: verum
end;
end;
end;
thus for n being Nat holds S2[n] from NAT_1:sch 1(, A3, A4); :: thesis: verum
end;
end;

Lm5: now
let f1, f2 be non empty to-naturals from-natural-fseqs homogeneous Function; :: thesis: for p being Element of ((arity f1) + 1) -tuples_on NAT
for i, m being Nat st i in dom p holds
for G being Function of ((arity f1) + 1) -tuples_on NAT , HFuncs NAT st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ) holds
for k, n being Nat st not p +* i,k in dom (G . (p +* i,k)) holds
not p +* i,k in dom (G . (p +* i,(k + n)))

let p be Element of ((arity f1) + 1) -tuples_on NAT ; :: thesis: for i, m being Nat st i in dom p holds
for G being Function of ((arity f1) + 1) -tuples_on NAT , HFuncs NAT st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ) holds
for k, n being Nat st not p +* i,k in dom (G . (p +* i,k)) holds
not p +* i,k in dom (G . (p +* i,(k + n)))

let i, m be Nat; :: thesis: ( i in dom p implies for G being Function of ((arity f1) + 1) -tuples_on NAT , HFuncs NAT st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ) holds
for k, n being Nat st not p +* i,k in dom (G . (p +* i,k)) holds
not p +* i,k in dom (G . (p +* i,(k + n))) )

assume A1: i in dom p ; :: thesis: for G being Function of ((arity f1) + 1) -tuples_on NAT , HFuncs NAT st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ) holds
for k, n being Nat st not p +* i,k in dom (G . (p +* i,k)) holds
not p +* i,k in dom (G . (p +* i,(k + n)))

let G be Function of ((arity f1) + 1) -tuples_on NAT , HFuncs NAT ; :: thesis: ( ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ) implies for k, n being Nat st not p +* i,k in dom (G . (p +* i,k)) holds
not p +* i,k in dom (G . (p +* i,(k + n))) )

assume A2: for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p ; :: thesis: for k, n being Nat st not p +* i,k in dom (G . (p +* i,k)) holds
not p +* i,k in dom (G . (p +* i,(k + n)))

thus for k, n being Nat st not p +* i,k in dom (G . (p +* i,k)) holds
not p +* i,k in dom (G . (p +* i,(k + n))) :: thesis: verum
proof
let k be Nat; :: thesis: for 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)))

set pk = p +* i,k;
defpred S2[ Nat] means ( not p +* i,k in dom (G . (p +* i,k)) implies not p +* i,k in dom (G . (p +* i,(k + $1))) );
A3: S2[0] ;
A4: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume that
A5: S2[n] and
A6: not p +* i,k in dom (G . (p +* i,k)) ; :: thesis: not p +* i,k in dom (G . (p +* i,(k + (n + 1))))
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,(p +* i,(k + n)) = F . ((p +* i,(k + n)) /. i) and
A8: ( ( i in dom (p +* i,(k + n)) & Del (p +* i,(k + n)),i in dom f1 implies F . 0 = {((p +* i,(k + n)) +* i,0)} --> (f1 . (Del (p +* i,(k + n)),i)) ) & ( ( not i in dom (p +* i,(k + n)) or not Del (p +* i,(k + n)),i in dom f1 ) implies F . 0 = {} ) ) and
A9: for M being Nat holds S1[M,F . M,F . (M + 1),p +* i,(k + n),i,f2] by Def13;
consider F1 being Function of NAT , HFuncs NAT such that
A10: primrec f1,f2,i,(p +* i,((k + n) + 1)) = F1 . ((p +* i,((k + n) + 1)) /. i) and
A11: ( ( i in dom (p +* i,((k + n) + 1)) & Del (p +* i,((k + n) + 1)),i in dom f1 implies F1 . 0 = {((p +* i,((k + n) + 1)) +* i,0)} --> (f1 . (Del (p +* i,((k + n) + 1)),i)) ) & ( ( not i in dom (p +* i,((k + n) + 1)) or not Del (p +* i,((k + n) + 1)),i in dom f1 ) implies F1 . 0 = {} ) ) and
A12: for M being Nat holds S1[M,F1 . M,F1 . (M + 1),p +* i,((k + n) + 1),i,f2] by Def13;
A13: F1 = F by A8, A9, A11, A12, Lm2;
A14: ( dom p = dom (p +* i,k) & dom p = dom (p +* i,((k + n) + 1)) & dom p = dom (p +* i,(k + n)) ) by FUNCT_7:32;
then A15: (p +* i,((k + n) + 1)) /. i = (p +* i,((k + n) + 1)) . i by A1, FINSEQ_4:def 4
.= (k + n) + 1 by A1, FUNCT_7:33 ;
(p +* i,(k + n)) /. i = (p +* i,(k + n)) . i by A1, A14, FINSEQ_4:def 4
.= k + n by A1, FUNCT_7:33 ;
then A16: not p +* i,k in dom (F . (k + n)) by A2, A5, A6, A7;
A17: G . (p +* i,(k + (n + 1))) = F . ((k + n) + 1) by A2, A10, A13, A15;
per cases ( ( i in dom (p +* i,(k + n)) & (p +* i,(k + n)) +* i,(k + n) in dom (F . (k + n)) & ((p +* i,(k + n)) +* i,(k + n)) ^ <*((F . (k + n)) . ((p +* i,(k + n)) +* i,(k + n)))*> in dom f2 ) or not i in dom (p +* i,(k + n)) or not (p +* i,(k + n)) +* i,(k + n) in dom (F . (k + n)) or not ((p +* i,(k + n)) +* i,(k + n)) ^ <*((F . (k + n)) . ((p +* i,(k + n)) +* i,(k + n)))*> in dom f2 ) ;
suppose ( i in dom (p +* i,(k + n)) & (p +* i,(k + n)) +* i,(k + n) in dom (F . (k + n)) & ((p +* i,(k + n)) +* i,(k + n)) ^ <*((F . (k + n)) . ((p +* i,(k + n)) +* i,(k + n)))*> in dom f2 ) ; :: thesis: not p +* i,k in dom (G . (p +* i,(k + (n + 1))))
then F . ((k + n) + 1) = (F . (k + n)) +* ({((p +* i,(k + n)) +* i,((k + n) + 1))} --> (f2 . (((p +* i,(k + n)) +* i,(k + n)) ^ <*((F . (k + n)) . ((p +* i,(k + n)) +* i,(k + n)))*>))) by A9;
then dom (F . ((k + n) + 1)) = (dom (F . (k + n))) \/ (dom ({((p +* i,(k + n)) +* i,((k + n) + 1))} --> (f2 . (((p +* i,(k + n)) +* i,(k + n)) ^ <*((F . (k + n)) . ((p +* i,(k + n)) +* i,(k + n)))*>)))) by FUNCT_4:def 1;
then A18: dom (F . ((k + n) + 1)) = (dom (F . (k + n))) \/ {((p +* i,(k + n)) +* i,((k + n) + 1))} by FUNCOP_1:19;
k <= k + n by NAT_1:29;
then A19: k <> (k + n) + 1 by NAT_1:38;
( (p +* i,k) . i = k & ((p +* i,(k + n)) +* i,((k + n) + 1)) . i = (k + n) + 1 ) by A1, A14, FUNCT_7:33;
then not p +* i,k in {((p +* i,(k + n)) +* i,((k + n) + 1))} by A19, TARSKI:def 1;
hence not p +* i,k in dom (G . (p +* i,(k + (n + 1)))) by A16, A17, A18, XBOOLE_0:def 2; :: thesis: verum
end;
suppose ( not i in dom (p +* i,(k + n)) or not (p +* i,(k + n)) +* i,(k + n) in dom (F . (k + n)) or not ((p +* i,(k + n)) +* i,(k + n)) ^ <*((F . (k + n)) . ((p +* i,(k + n)) +* i,(k + n)))*> in dom f2 ) ; :: thesis: not p +* i,k in dom (G . (p +* i,(k + (n + 1))))
hence not p +* i,k in dom (G . (p +* i,(k + (n + 1)))) by A9, A16, A17; :: thesis: verum
end;
end;
end;
thus for n being Nat holds S2[n] from NAT_1:sch 1(, A3, A4); :: thesis: verum
end;
end;

Lm6: for i, m being Nat
for f1, f2 being non empty to-naturals from-natural-fseqs homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p holds
( ( p +* i,0 in dom (primrec f1,f2,i) implies Del p,i in dom f1 ) & ( Del p,i in dom f1 implies p +* i,0 in dom (primrec f1,f2,i) ) & ( p +* i,0 in dom (primrec f1,f2,i) implies (primrec f1,f2,i) . (p +* i,0) = f1 . (Del p,i) ) & ( p +* i,(m + 1) in dom (primrec f1,f2,i) implies ( p +* i,m in dom (primrec f1,f2,i) & (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2 ) ) & ( p +* i,m in dom (primrec f1,f2,i) & (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2 implies p +* i,(m + 1) in dom (primrec f1,f2,i) ) & ( p +* i,(m + 1) in dom (primrec f1,f2,i) implies (primrec f1,f2,i) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*>) ) )
proof end;

theorem :: COMPUT_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for f1, f2 being non empty to-naturals from-natural-fseqs homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p holds
( p +* i,0 in dom (primrec f1,f2,i) iff Del p,i in dom f1 ) by Lm6;

theorem :: COMPUT_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for f1, f2 being non empty to-naturals from-natural-fseqs homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p & p +* i,0 in dom (primrec f1,f2,i) holds
(primrec f1,f2,i) . (p +* i,0) = f1 . (Del p,i) by Lm6;

theorem Th64: :: COMPUT_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for f1, f2 being non empty to-naturals from-natural-fseqs homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p & f1 is len-total holds
(primrec f1,f2,i) . (p +* i,0) = f1 . (Del p,i)
proof end;

theorem :: COMPUT_1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, m being Nat
for f1, f2 being non empty to-naturals from-natural-fseqs homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p holds
( p +* i,(m + 1) in dom (primrec f1,f2,i) iff ( p +* i,m in dom (primrec f1,f2,i) & (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2 ) ) by Lm6;

theorem :: COMPUT_1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, m being Nat
for f1, f2 being non empty to-naturals from-natural-fseqs homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p & p +* i,(m + 1) in dom (primrec f1,f2,i) holds
(primrec f1,f2,i) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*>) by Lm6;

theorem Th67: :: COMPUT_1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, m being Nat
for f1, f2 being non empty to-naturals from-natural-fseqs homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st f1 is len-total & f2 is len-total & (arity f1) + 2 = arity f2 & 1 <= i & i <= 1 + (arity f1) holds
(primrec f1,f2,i) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*>)
proof end;

theorem Th68: :: COMPUT_1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for f1, f2 being non empty to-naturals from-natural-fseqs homogeneous Function st (arity f1) + 2 = arity f2 & 1 <= i & i <= (arity f1) + 1 holds
primrec f1,f2,i is_primitive-recursively_expressed_by f1,f2,i
proof end;

theorem :: COMPUT_1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for f1, f2 being non empty to-naturals from-natural-fseqs homogeneous Function st 1 <= i & i <= (arity f1) + 1 holds
for g being Element of HFuncs NAT st g is_primitive-recursively_expressed_by f1,f2,i holds
g = primrec f1,f2,i
proof end;

definition
let X be set ;
attr X is composition_closed means :Def15: :: COMPUT_1:def 15
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;
attr X is primitive-recursion_closed means :Def16: :: COMPUT_1:def 16
for g, f1, f2 being Element of HFuncs NAT
for i being Nat st g is_primitive-recursively_expressed_by f1,f2,i & f1 in X & f2 in X holds
g in X;
end;

:: deftheorem Def15 defines composition_closed COMPUT_1:def 15 :
for X being set holds
( X is composition_closed iff for f being Element of HFuncs NAT
for F being with_the_same_arity FinSequence of HFuncs NAT st f in X & arity f = len F & rng F c= X holds
f * <:F:> in X );

:: deftheorem Def16 defines primitive-recursion_closed COMPUT_1:def 16 :
for X being set holds
( X is primitive-recursion_closed iff for g, f1, f2 being Element of HFuncs NAT
for i being Nat st g is_primitive-recursively_expressed_by f1,f2,i & f1 in X & f2 in X holds
g in X );

definition
let X be set ;
attr X is primitive-recursively_closed means :Def17: :: COMPUT_1:def 17
( 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;

:: deftheorem Def17 defines primitive-recursively_closed COMPUT_1:def 17 :
for X being set holds
( X is primitive-recursively_closed iff ( 0 const 0 in X & 1 succ 1 in X & ( for n, i being Nat st 1 <= i & i <= n holds
n proj i in X ) & X is composition_closed & X is primitive-recursion_closed ) );

theorem Th70: :: COMPUT_1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
HFuncs NAT is primitive-recursively_closed
proof end;

registration
cluster non empty primitive-recursively_closed Element of bool (HFuncs NAT );
existence
ex b1 being Subset of (HFuncs NAT ) st
( b1 is primitive-recursively_closed & not b1 is empty )
proof end;
end;

Lm7: for X being non empty set
for n, i being Nat st 1 <= i & i <= n holds
for x being Element of X
for p being Element of n -tuples_on X holds p +* i,x in n -tuples_on X
;

theorem Th71: :: COMPUT_1:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for e1, e2 being to-naturals from-natural-fseqs homogeneous Function
for g being Element of HFuncs NAT st e1 = {} & g is_primitive-recursively_expressed_by e1,e2,i holds
g = {}
proof end;

theorem Th72: :: COMPUT_1:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for g being Element of HFuncs NAT
for f1, f2 being quasi_total Element of HFuncs NAT
for i being Nat st g is_primitive-recursively_expressed_by f1,f2,i holds
( g is quasi_total & ( not f1 is empty implies not g is empty ) )
proof end;

theorem Th73: :: COMPUT_1:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, c being Nat
for P being non empty primitive-recursively_closed Subset of (HFuncs NAT ) holds n const c in P
proof end;

theorem Th74: :: COMPUT_1:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat
for P being non empty primitive-recursively_closed Subset of (HFuncs NAT ) st 1 <= i & i <= n holds
n succ i in P
proof end;

theorem Th75: :: COMPUT_1:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty primitive-recursively_closed Subset of (HFuncs NAT ) holds {} in P
proof end;

theorem Th76: :: COMPUT_1:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty primitive-recursively_closed Subset of (HFuncs NAT )
for f being Element of P
for F being with_the_same_arity FinSequence of P st arity f = len F holds
f * <:F:> in P
proof end;

theorem Th77: :: COMPUT_1:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty primitive-recursively_closed Subset of (HFuncs NAT )
for f1, f2 being Element of P st (arity f1) + 2 = arity f2 holds
for i being Nat st 1 <= i & i <= (arity f1) + 1 holds
primrec f1,f2,i in P
proof end;

definition
func PrimRec -> Subset of (HFuncs NAT ) equals :: COMPUT_1:def 18
meet { R where R is Subset of (HFuncs NAT ) : R is primitive-recursively_closed } ;
coherence
meet { R where R is Subset of (HFuncs NAT ) : R is primitive-recursively_closed } is Subset of (HFuncs NAT )
proof end;
end;

:: deftheorem defines PrimRec COMPUT_1:def 18 :
PrimRec = meet { R where R is Subset of (HFuncs NAT ) : R is primitive-recursively_closed } ;

theorem Th78: :: COMPUT_1:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of (HFuncs NAT ) st X is primitive-recursively_closed holds
PrimRec c= X
proof end;

registration
cluster PrimRec -> non empty primitive-recursively_closed ;
coherence
( not PrimRec is empty & PrimRec is primitive-recursively_closed )
proof end;
end;

registration
cluster -> homogeneous Element of PrimRec ;
coherence
for b1 being Element of PrimRec holds b1 is homogeneous
;
end;

definition
let x be set ;
attr x is primitive-recursive means :Def19: :: COMPUT_1:def 19
x in PrimRec ;
end;

:: deftheorem Def19 defines primitive-recursive COMPUT_1:def 19 :
for x being set holds
( x is primitive-recursive iff x in PrimRec );

registration
cluster primitive-recursive -> Relation-like Function-like set ;
coherence
for b1 being set st b1 is primitive-recursive holds
( b1 is Relation-like & b1 is Function-like )
proof end;
end;

registration
cluster primitive-recursive -> to-naturals from-natural-fseqs homogeneous set ;
coherence
for b1 being Relation st b1 is primitive-recursive holds
( b1 is homogeneous & b1 is to-naturals & b1 is from-natural-fseqs )
proof end;
end;

registration
cluster -> Relation-like Function-like to-naturals from-natural-fseqs homogeneous primitive-recursive Element of PrimRec ;
coherence
for b1 being Element of PrimRec holds b1 is primitive-recursive
by Def19;
end;

registration
cluster to-naturals from-natural-fseqs homogeneous primitive-recursive set ;
existence
ex b1 being Function st b1 is primitive-recursive
proof end;
cluster to-naturals from-natural-fseqs homogeneous primitive-recursive Element of HFuncs NAT ;
existence
ex b1 being Element of HFuncs NAT st b1 is primitive-recursive
proof end;
end;

definition
func initial-funcs -> Subset of (HFuncs NAT ) equals :: COMPUT_1:def 20
{(0 const 0),(1 succ 1)} \/ { (n proj i) where n, i is Nat : ( 1 <= i & i <= n ) } ;
coherence
{(0 const 0),(1 succ 1)} \/ { (n proj i) where n, i is Nat : ( 1 <= i & i <= n ) } is Subset of (HFuncs NAT )
proof end;
let Q be Subset of (HFuncs NAT );
func PR-closure Q -> Subset of (HFuncs NAT ) equals :: COMPUT_1:def 21
Q \/ { g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Nat st
( f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by f1,f2,i )
}
;
coherence
Q \/ { g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Nat st
( f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by f1,f2,i )
}
is Subset of (HFuncs NAT )
proof end;
func composition-closure Q -> Subset of (HFuncs NAT ) equals :: COMPUT_1:def 22
Q \/ { (f * <:F:>) where f is Element of HFuncs NAT , F is with_the_same_arity Element of (HFuncs NAT ) * : ( f in Q & arity f = len F & rng F c= Q ) } ;
coherence
Q \/ { (f * <:F:>) where f is Element of HFuncs NAT , F is with_the_same_arity Element of (HFuncs NAT ) * : ( f in Q & arity f = len F & rng F c= Q ) } is Subset of (HFuncs NAT )
proof end;
end;

:: deftheorem defines initial-funcs COMPUT_1:def 20 :
initial-funcs = {(0 const 0),(1 succ 1)} \/ { (n proj i) where n, i is Nat : ( 1 <= i & i <= n ) } ;

:: deftheorem defines PR-closure COMPUT_1:def 21 :
for Q being Subset of (HFuncs NAT ) holds PR-closure Q = Q \/ { g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Nat st
( f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by f1,f2,i )
}
;

:: deftheorem defines composition-closure COMPUT_1:def 22 :
for Q being Subset of (HFuncs NAT ) holds composition-closure Q = Q \/ { (f * <:F:>) where f is Element of HFuncs NAT , F is with_the_same_arity Element of (HFuncs NAT ) * : ( f in Q & arity f = len F & rng F c= Q ) } ;

definition
func PrimRec-Approximation -> Function of NAT , bool (HFuncs NAT ) means :Def23: :: COMPUT_1:def 23
( it . 0 = initial-funcs & ( for m being Nat holds it . (m + 1) = (PR-closure (it . m)) \/ (composition-closure (it . m)) ) );
existence
ex b1 being Function of NAT , bool (HFuncs NAT ) st
( b1 . 0 = initial-funcs & ( for m being Nat holds b1 . (m + 1) = (PR-closure (b1 . m)) \/ (composition-closure (b1 . m)) ) )
proof end;
uniqueness
for b1, b2 being Function of NAT , bool (HFuncs NAT ) st b1 . 0 = initial-funcs & ( for m being Nat holds b1 . (m + 1) = (PR-closure (b1 . m)) \/ (composition-closure (b1 . m)) ) & b2 . 0 = initial-funcs & ( for m being Nat holds b2 . (m + 1) = (PR-closure (b2 . m)) \/ (composition-closure (b2 . m)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def23 defines PrimRec-Approximation COMPUT_1:def 23 :
for b1 being Function of NAT , bool (HFuncs NAT ) holds
( b1 = PrimRec-Approximation iff ( b1 . 0 = initial-funcs & ( for m being Nat holds b1 . (m + 1) = (PR-closure (b1 . m)) \/ (composition-closure (b1 . m)) ) ) );

theorem Th79: :: COMPUT_1:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat st m <= n holds
PrimRec-Approximation . m c= PrimRec-Approximation . n
proof end;

theorem Th80: :: COMPUT_1:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Union PrimRec-Approximation is primitive-recursively_closed
proof end;

theorem Th81: :: COMPUT_1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
PrimRec = Union PrimRec-Approximation
proof end;

theorem Th82: :: COMPUT_1:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat
for f being Element of HFuncs NAT st f in PrimRec-Approximation . m holds
f is quasi_total
proof end;

registration
cluster -> Relation-like Function-like quasi_total to-naturals from-natural-fseqs homogeneous primitive-recursive Element of PrimRec ;
coherence
for b1 being Element of PrimRec holds
( b1 is quasi_total & b1 is homogeneous )
proof end;
end;

registration
cluster primitive-recursive -> quasi_total homogeneous Element of HFuncs NAT ;
coherence
for b1 being Element of HFuncs NAT st b1 is primitive-recursive holds
b1 is quasi_total
proof end;
end;

registration
cluster from-natural-fseqs primitive-recursive -> from-natural-fseqs len-total set ;
coherence
for b1 being from-natural-fseqs Function st b1 is primitive-recursive holds
b1 is len-total
proof end;
cluster non empty quasi_total to-naturals from-natural-fseqs len-total homogeneous primitive-recursive Element of PrimRec ;
existence
not for b1 being Element of PrimRec holds b1 is empty
proof end;
end;

definition
let f be homogeneous Relation;
attr f is nullary means :Def24: :: COMPUT_1:def 24
arity f = 0;
attr f is unary means :Def25: :: COMPUT_1:def 25
arity f = 1;
attr f is binary means :Def26: :: COMPUT_1:def 26
arity f = 2;
attr f is 3-ary means :Def27: :: COMPUT_1:def 27
arity f = 3;
end;

:: deftheorem Def24 defines nullary COMPUT_1:def 24 :
for f being homogeneous Relation holds
( f is nullary iff arity f = 0 );

:: deftheorem Def25 defines unary COMPUT_1:def 25 :
for f being homogeneous Relation holds
( f is unary iff arity f = 1 );

:: deftheorem Def26 defines binary COMPUT_1:def 26 :
for f being homogeneous Relation holds
( f is binary iff arity f = 2 );

:: deftheorem Def27 defines 3-ary COMPUT_1:def 27 :
for f being homogeneous Relation holds
( f is 3-ary iff arity f = 3 );

registration
cluster homogeneous unary -> non empty homogeneous set ;
coherence
for b1 being homogeneous Function st b1 is unary holds
not b1 is empty
proof end;
cluster homogeneous binary -> non empty homogeneous set ;
coherence
for b1 being homogeneous Function st b1 is binary holds
not b1 is empty
proof end;
cluster homogeneous 3-ary -> non empty homogeneous set ;
coherence
for b1 being homogeneous Function st b1 is 3-ary holds
not b1 is empty
proof end;
end;

registration
cluster 1 proj 1 -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive ;
coherence
1 proj 1 is primitive-recursive
proof end;
cluster 2 proj 1 -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive ;
coherence
2 proj 1 is primitive-recursive
proof end;
cluster 2 proj 2 -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive ;
coherence
2 proj 2 is primitive-recursive
proof end;
cluster 1 succ 1 -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive ;
coherence
1 succ 1 is primitive-recursive
proof end;
cluster 3 succ 3 -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive ;
coherence
3 succ 3 is primitive-recursive
proof end;
let i be Nat;
cluster 0 const i -> non empty to-naturals from-natural-fseqs len-total homogeneous nullary ;
coherence
0 const i is nullary
proof end;
cluster 1 const i -> non empty to-naturals from-natural-fseqs len-total homogeneous unary ;
coherence
1 const i is unary
proof end;
cluster 2 const i -> non empty to-naturals from-natural-fseqs len-total homogeneous binary ;
coherence
2 const i is binary
proof end;
cluster 3 const i -> non empty to-naturals from-natural-fseqs len-total homogeneous 3-ary ;
coherence
3 const i is 3-ary
proof end;
cluster 1 proj i -> non empty to-naturals from-natural-fseqs len-total homogeneous unary ;
coherence
1 proj i is unary
proof end;
cluster 2 proj i -> non empty to-naturals from-natural-fseqs len-total homogeneous binary ;
coherence
2 proj i is binary
proof end;
cluster 3 proj i -> non empty to-naturals from-natural-fseqs len-total homogeneous 3-ary ;
coherence
3 proj i is 3-ary
proof end;
cluster 1 succ i -> non empty to-naturals from-natural-fseqs len-total homogeneous unary ;
coherence
1 succ i is unary
proof end;
cluster 2 succ i -> non empty to-naturals from-natural-fseqs len-total homogeneous binary ;
coherence
2 succ i is binary
proof end;
cluster 3 succ i -> non empty to-naturals from-natural-fseqs len-total homogeneous 3-ary ;
coherence
3 succ i is 3-ary
proof end;
let j be Nat;
cluster i const j -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive ;
coherence
i const j is primitive-recursive
proof end;
end;

registration
cluster non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive nullary set ;
existence
ex b1 being homogeneous Function st
( b1 is nullary & b1 is primitive-recursive & not b1 is empty )
by Def17;
cluster non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive unary set ;
existence
ex b1 being homogeneous Function st
( b1 is unary & b1 is primitive-recursive )
by Def17;
cluster non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive binary set ;
existence
ex b1 being homogeneous Function st
( b1 is binary & b1 is primitive-recursive )
proof end;
cluster non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive 3-ary set ;
existence
ex b1 being homogeneous Function st
( b1 is 3-ary & b1 is primitive-recursive )
proof end;
end;

registration
cluster non empty to-naturals from-natural-fseqs len-total homogeneous nullary set ;
existence
ex b1 being from-natural-fseqs homogeneous Function st
( not b1 is empty & b1 is nullary & b1 is len-total & b1 is to-naturals )
proof end;
cluster non empty to-naturals from-natural-fseqs len-total homogeneous unary set ;
existence
ex b1 being from-natural-fseqs homogeneous Function st
( not b1 is empty & b1 is unary & b1 is len-total & b1 is to-naturals )
proof end;
cluster non empty to-naturals from-natural-fseqs len-total homogeneous binary set ;
existence
ex b1 being from-natural-fseqs homogeneous Function st
( not b1 is empty & b1 is binary & b1 is len-total & b1 is to-naturals )
proof end;
cluster non empty to-naturals from-natural-fseqs len-total homogeneous 3-ary set ;
existence
ex b1 being from-natural-fseqs homogeneous Function st
( not b1 is empty & b1 is 3-ary & b1 is len-total & b1 is to-naturals )
proof end;
end;

registration
let f be non empty primitive-recursive nullary Function;
let g be primitive-recursive binary Function;
cluster primrec f,g,1 -> non empty quasi_total to-naturals from-natural-fseqs len-total homogeneous primitive-recursive unary ;
coherence
( primrec f,g,1 is primitive-recursive & primrec f,g,1 is unary )
proof end;
end;

registration
let f be primitive-recursive unary Function;
let g be primitive-recursive 3-ary Function;
cluster primrec f,g,1 -> non empty quasi_total to-naturals from-natural-fseqs len-total homogeneous primitive-recursive binary ;
coherence
( primrec f,g,1 is primitive-recursive & primrec f,g,1 is binary )
proof end;
cluster primrec f,g,2 -> non empty quasi_total to-naturals from-natural-fseqs len-total homogeneous primitive-recursive binary ;
coherence
( primrec f,g,2 is primitive-recursive & primrec f,g,2 is binary )
proof end;
end;

theorem Th83: :: COMPUT_1:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for f1 being to-naturals from-natural-fseqs len-total homogeneous unary Function
for f2 being non empty to-naturals from-natural-fseqs homogeneous Function holds (primrec f1,f2,2) . <*i,0*> = f1 . <*i*>
proof end;

theorem Th84: :: COMPUT_1:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being non empty to-naturals from-natural-fseqs homogeneous Function st f1 is len-total & arity f1 = 0 holds
(primrec f1,f2,1) . <*0*> = f1 . {}
proof end;

theorem Th85: :: COMPUT_1:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat
for f1 being to-naturals from-natural-fseqs len-total homogeneous unary Function
for f2 being to-naturals from-natural-fseqs len-total homogeneous 3-ary Function holds (primrec f1,f2,2) . <*i,(j + 1)*> = f2 . <*i,j,((primrec f1,f2,2) . <*i,j*>)*>
proof end;

theorem Th86: :: COMPUT_1:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for f1, f2 being non empty to-naturals from-natural-fseqs homogeneous Function st f1 is len-total & f2 is len-total & arity f1 = 0 & arity f2 = 2 holds
(primrec f1,f2,1) . <*(i + 1)*> = f2 . <*i,((primrec f1,f2,1) . <*i*>)*>
proof end;

Lm8: now
let g be non empty quasi_total homogeneous PartFunc of NAT * , NAT ; :: thesis: ( arity g = 2 implies ( dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3)) & dom <:<*(3 proj 1),(3 proj 3)*>:> = 3 -tuples_on NAT & dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT & ex G being homogeneous PartFunc of NAT * , NAT st
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty ) ) )

assume A1: arity g = 2 ; :: thesis: ( dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3)) & dom <:<*(3 proj 1),(3 proj 3)*>:> = 3 -tuples_on NAT & dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT & ex G being homogeneous PartFunc of NAT * , NAT st
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty ) )

thus A2: dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3)) by FUNCT_6:62; :: thesis: ( dom <:<*(3 proj 1),(3 proj 3)*>:> = 3 -tuples_on NAT & dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT & ex G being homogeneous PartFunc of NAT * , NAT st
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty ) )

hence A3: dom <:<*(3 proj 1),(3 proj 3)*>:> = (3 -tuples_on NAT ) /\ (dom (3 proj 3)) by Th40
.= (3 -tuples_on NAT ) /\ (3 -tuples_on NAT ) by Th40
.= 3 -tuples_on NAT ;
:: thesis: ( dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT & ex G being homogeneous PartFunc of NAT * , NAT st
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty ) )

reconsider z3 = <*0,0,0*> as FinSequence of NAT ;
len z3 = 3 by FINSEQ_1:62;
then A4: z3 is Element of 3 -tuples_on NAT by FINSEQ_2:110;
A5: dom g = 2 -tuples_on NAT by A1, Th25;
set G = g * <:<*(3 proj 1),(3 proj 3)*>:>;
now
let x be set ; :: thesis: ( ( x in rng <:<*(3 proj 1),(3 proj 3)*>:> implies x in dom g ) & ( x in dom g implies x in rng <:<*(3 proj 1),(3 proj 3)*>:> ) )
set f = <*(3 proj 1),(3 proj 3)*>;
set F = <:<*(3 proj 1),(3 proj 3)*>:>;
A6: product (rngs <*(3 proj 1),(3 proj 3)*>) = product <*(rng (3 proj 1)),(rng (3 proj 3))*> by FUNCT_6:34
.= product <*NAT ,(rng (3 proj 3))*> by Th40
.= product <*NAT ,NAT *> by Th40
.= 2 -tuples_on NAT by FUNCT_6:6 ;
hereby :: thesis: ( x in dom g implies x in rng <:<*(3 proj 1),(3 proj 3)*>:> )
assume A7: x in rng <:<*(3 proj 1),(3 proj 3)*>:> ; :: thesis: x in dom g
rng <:<*(3 proj 1),(3 proj 3)*>:> c= product (rngs <*(3 proj 1),(3 proj 3)*>) by FUNCT_6:49;
hence x in dom g by A5, A6, A7; :: thesis: verum
end;
assume x in dom g ; :: thesis: x in rng <:<*(3 proj 1),(3 proj 3)*>:>
then consider d1, d2 being Nat such that
A8: x = <*d1,d2*> by A5, FINSEQ_2:120;
reconsider x' = <*d1,0,d2*> as Element of 3 -tuples_on NAT by FINSEQ_2:124;
<:<*(3 proj 1),(3 proj 3)*>:> . x' = <*((3 proj 1) . x'),((3 proj 3) . x')*> by A2, A3, FUNCT_6:62
.= <*(x' . 1),((3 proj 3) . x')*> by Th42
.= <*(x' . 1),(x' . 3)*> by Th42
.= <*d1,(x' . 3)*> by FINSEQ_1:62
.= x by A8, FINSEQ_1:62 ;
hence x in rng <:<*(3 proj 1),(3 proj 3)*>:> by A3, FUNCT_1:def 5; :: thesis: verum
end;
then A9: rng <:<*(3 proj 1),(3 proj 3)*>:> = dom g by TARSKI:2;
hence A10: dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT by A3, RELAT_1:46; :: thesis: ex G being homogeneous PartFunc of NAT * , NAT st
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty )

then A11: dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) c= NAT * by MSUALG_1:12;
rng g c= NAT by RELSET_1:12;
then rng (g * <:<*(3 proj 1),(3 proj 3)*>:>) c= NAT by A9, RELAT_1:47;
then reconsider G = g * <:<*(3 proj 1),(3 proj 3)*>:> as PartFunc of NAT * , NAT by A11, RELSET_1:11;
now
let x, y be FinSequence; :: thesis: ( x in dom G & y in dom G implies len x = len y )
assume ( x in dom G & y in dom G ) ; :: thesis: len x = len y
then ( 3 = len x & 3 = len y ) by A10, FINSEQ_2:109;
hence len x = len y ; :: thesis: verum
end;
then reconsider G = G as homogeneous PartFunc of NAT * , NAT by Def4;
take G = G; :: thesis: ( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty )
thus G = g * <:<*(3 proj 1),(3 proj 3)*>:> ; :: thesis: ( G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty )
G is Element of PFuncs (NAT * ),NAT by PARTFUN1:119;
then G in HFuncs NAT ;
hence G is Element of HFuncs NAT ; :: thesis: ( arity G = 3 & G is quasi_total & not G is empty )
for x being FinSequence st x in dom G holds
3 = len x by A10, FINSEQ_2:109;
hence arity G = 3 by A4, A10, Def5; :: thesis: ( G is quasi_total & not G is empty )
hence ( G is quasi_total & not G is empty ) by A10, Th25; :: thesis: verum
end;

definition
let g be Function;
func (1,2)->(1,?,2) g -> Function equals :: COMPUT_1:def 28
g * <:<*(3 proj 1),(3 proj 3)*>:>;
coherence
g * <:<*(3 proj 1),(3 proj 3)*>:> is Function
;
end;

:: deftheorem defines (1,2)->(1,?,2) COMPUT_1:def 28 :
for g being Function holds (1,2)->(1,?,2) g = g * <:<*(3 proj 1),(3 proj 3)*>:>;

registration
let g be to-naturals from-natural-fseqs Function;
cluster (1,2)->(1,?,2) g -> to-naturals from-natural-fseqs ;
coherence
( (1,2)->(1,?,2) g is to-naturals & (1,2)->(1,?,2) g is from-natural-fseqs )
proof end;
end;

registration
let g be homogeneous Function;
cluster (1,2)->(1,?,2) g -> homogeneous ;
coherence
(1,2)->(1,?,2) g is homogeneous
proof end;
end;

registration
let g be to-naturals from-natural-fseqs len-total homogeneous binary Function;
cluster (1,2)->(1,?,2) g -> non empty to-naturals from-natural-fseqs len-total homogeneous 3-ary ;
coherence
( not (1,2)->(1,?,2) g is empty & (1,2)->(1,?,2) g is 3-ary & (1,2)->(1,?,2) g is len-total )
proof end;
end;

theorem Th87: :: COMPUT_1:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, k being Nat
for f being to-naturals from-natural-fseqs len-total homogeneous binary Function holds ((1,2)->(1,?,2) f) . <*i,j,k*> = f . <*i,k*>
proof end;

theorem Th88: :: COMPUT_1:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for g being primitive-recursive binary Function holds (1,2)->(1,?,2) g in PrimRec
proof end;

registration
let f be homogeneous primitive-recursive binary Function;
cluster (1,2)->(1,?,2) f -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive 3-ary ;
coherence
( (1,2)->(1,?,2) f is primitive-recursive & (1,2)->(1,?,2) f is 3-ary )
proof end;
end;

definition
func [+] -> primitive-recursive binary Function equals :: COMPUT_1:def 29
primrec (1 proj 1),(3 succ 3),2;
coherence
primrec (1 proj 1),(3 succ 3),2 is primitive-recursive binary Function
;
end;

:: deftheorem defines [+] COMPUT_1:def 29 :
[+] = primrec (1 proj 1),(3 succ 3),2;

theorem Th89: :: COMPUT_1:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat holds [+] . <*i,j*> = i + j
proof end;

definition
func [*] -> primitive-recursive binary Function equals :: COMPUT_1:def 30
primrec (1 const 0),((1,2)->(1,?,2) [+] ),2;
coherence
primrec (1 const 0),((1,2)->(1,?,2) [+] ),2 is primitive-recursive binary Function
;
end;

:: deftheorem defines [*] COMPUT_1:def 30 :
[*] = primrec (1 const 0),((1,2)->(1,?,2) [+] ),2;

theorem Th90: :: COMPUT_1:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat holds [*] . <*i,j*> = i * j
proof end;

registration
let g, h be homogeneous primitive-recursive binary Function;
cluster <*g,h*> -> with_the_same_arity ;
coherence
<*g,h*> is with_the_same_arity
proof end;
end;

registration
let f, g, h be primitive-recursive binary Function;
cluster <:<*g,h*>:> * f -> to-naturals from-natural-fseqs len-total homogeneous primitive-recursive ;
coherence
f * <:<*g,h*>:> is primitive-recursive
proof end;
end;

registration
let f, g, h be primitive-recursive binary Function;
cluster <:<*g,h*>:> * f -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive binary ;
coherence
f * <:<*g,h*>:> is binary
proof end;
end;

registration
let f be primitive-recursive unary Function;
let g be primitive-recursive Function;
cluster <:<*g*>:> * f -> to-naturals from-natural-fseqs len-total homogeneous primitive-recursive ;
coherence
f * <:<*g*>:> is primitive-recursive
proof end;
end;

registration
let f be primitive-recursive unary Function;
let g be primitive-recursive binary Function;
cluster <:<*g*>:> * f -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive binary ;
coherence
f * <:<*g*>:> is binary
proof end;
end;

definition
func [!] -> primitive-recursive unary Function equals :: COMPUT_1:def 31
primrec (0 const 1),([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>),1;
coherence
primrec (0 const 1),([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>),1 is primitive-recursive unary Function
;
end;

:: deftheorem defines [!] COMPUT_1:def 31 :
[!] = primrec (0 const 1),([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>),1;

scheme :: COMPUT_1:sch 1
Primrec1{ F1() -> to-naturals from-natural-fseqs len-total homogeneous unary Function, F2() -> to-naturals from-natural-fseqs len-total homogeneous binary Function, F3( set ) -> Nat, F4( set , set ) -> Nat } :
for i, j being Nat holds (F1() * <:<*F2()*>:>) . <*i,j*> = F3(F4(i,j))
provided
A1: for i being Nat holds F1() . <*i*> = F3(i) and
A2: for i, j being Nat holds F2() . <*i,j*> = F4(i,j)
proof end;

scheme :: COMPUT_1:sch 2
Primrec2{ F1() -> to-naturals from-natural-fseqs len-total homogeneous binary Function, F2() -> to-naturals from-natural-fseqs len-total homogeneous binary Function, F3() -> to-naturals from-natural-fseqs len-total homogeneous binary Function, F4( set , set ) -> Nat, F5( set , set ) -> Nat, F6( set , set ) -> Nat } :
for i, j being Nat holds (F1() * <:<*F2(),F3()*>:>) . <*i,j*> = F4(F5(i,j),F6(i,j))
provided
A1: for i, j being Nat holds F1() . <*i,j*> = F4(i,j) and
A2: for i, j being Nat holds F2() . <*i,j*> = F5(i,j) and
A3: for i, j being Nat holds F3() . <*i,j*> = F6(i,j)
proof end;

theorem :: COMPUT_1:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat holds [!] . <*i*> = i !
proof end;

definition
func [^] -> primitive-recursive binary Function equals :: COMPUT_1:def 32
primrec (1 const 1),((1,2)->(1,?,2) [*] ),2;
coherence
primrec (1 const 1),((1,2)->(1,?,2) [*] ),2 is primitive-recursive binary Function
;
end;

:: deftheorem defines [^] COMPUT_1:def 32 :
[^] = primrec (1 const 1),((1,2)->(1,?,2) [*] ),2;

theorem :: COMPUT_1:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat holds [^] . <*i,j*> = i |^ j
proof end;

definition
func [pred] -> primitive-recursive unary Function equals :: COMPUT_1:def 33
primrec (0 const 0),(2 proj 1),1;
coherence
primrec (0 const 0),(2 proj 1),1 is primitive-recursive unary Function
;
end;

:: deftheorem defines [pred] COMPUT_1:def 33 :
[pred] = primrec (0 const 0),(2 proj 1),1;

theorem Th93: :: COMPUT_1:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat holds
( [pred] . <*0*> = 0 & [pred] . <*(i + 1)*> = i )
proof end;

definition
func [-] -> primitive-recursive binary Function equals :: COMPUT_1:def 34
primrec (1 proj 1),((1,2)->(1,?,2) ([pred] * <:<*(2 proj 2)*>:>)),2;
coherence
primrec (1 proj 1),((1,2)->(1,?,2) ([pred] * <:<*(2 proj 2)*>:>)),2 is primitive-recursive binary Function
;
end;

:: deftheorem defines [-] COMPUT_1:def 34 :
[-] = primrec (1 proj 1),((1,2)->(1,?,2) ([pred] * <:<*(2 proj 2)*>:>)),2;

theorem :: COMPUT_1:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat holds [-] . <*i,j*> = i -' j
proof end;