let i be Element of NAT ; for f1, f2 being non empty NAT * -defined to-naturals 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
let f1, f2 be non empty NAT * -defined to-naturals homogeneous Function; ( (arity f1) + 2 = arity f2 & 1 <= i & i <= (arity f1) + 1 implies primrec (f1,f2,i) is_primitive-recursively_expressed_by f1,f2,i )
assume that
A1:
(arity f1) + 2 = arity f2
and
A2:
1 <= i
and
A3:
i <= (arity f1) + 1
; primrec (f1,f2,i) is_primitive-recursively_expressed_by f1,f2,i
take n = (arity f1) + 1; COMPUT_1:def 9 ( dom (primrec (f1,f2,i)) 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 (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)) ) & ( for n being Nat holds
( ( p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) implies ( p +* (i,n) in dom (primrec (f1,f2,i)) & (p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*> in dom f2 ) ) & ( p +* (i,n) in dom (primrec (f1,f2,i)) & (p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*> in dom f2 implies p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) ) & ( p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) implies (primrec (f1,f2,i)) . (p +* (i,(n + 1))) = f2 . ((p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*>) ) ) ) ) ) )
set g = primrec (f1,f2,i);
thus
dom (primrec (f1,f2,i)) c= n -tuples_on NAT
by Th55; ( 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 (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)) ) & ( for n being Nat holds
( ( p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) implies ( p +* (i,n) in dom (primrec (f1,f2,i)) & (p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*> in dom f2 ) ) & ( p +* (i,n) in dom (primrec (f1,f2,i)) & (p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*> in dom f2 implies p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) ) & ( p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) implies (primrec (f1,f2,i)) . (p +* (i,(n + 1))) = f2 . ((p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*>) ) ) ) ) ) )
thus
( i >= 1 & i <= n )
by A2, A3; ( (arity f1) + 1 = n & n + 1 = arity f2 & ( for p being FinSequence of NAT st len p = n 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)) ) & ( for n being Nat holds
( ( p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) implies ( p +* (i,n) in dom (primrec (f1,f2,i)) & (p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*> in dom f2 ) ) & ( p +* (i,n) in dom (primrec (f1,f2,i)) & (p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*> in dom f2 implies p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) ) & ( p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) implies (primrec (f1,f2,i)) . (p +* (i,(n + 1))) = f2 . ((p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*>) ) ) ) ) ) )
thus
(arity f1) + 1 = n
; ( n + 1 = arity f2 & ( for p being FinSequence of NAT st len p = n 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)) ) & ( for n being Nat holds
( ( p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) implies ( p +* (i,n) in dom (primrec (f1,f2,i)) & (p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*> in dom f2 ) ) & ( p +* (i,n) in dom (primrec (f1,f2,i)) & (p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*> in dom f2 implies p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) ) & ( p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) implies (primrec (f1,f2,i)) . (p +* (i,(n + 1))) = f2 . ((p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*>) ) ) ) ) ) )
thus
n + 1 = arity f2
by A1; for p being FinSequence of NAT st len p = n 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)) ) & ( for n being Nat holds
( ( p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) implies ( p +* (i,n) in dom (primrec (f1,f2,i)) & (p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*> in dom f2 ) ) & ( p +* (i,n) in dom (primrec (f1,f2,i)) & (p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*> in dom f2 implies p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) ) & ( p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) implies (primrec (f1,f2,i)) . (p +* (i,(n + 1))) = f2 . ((p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*>) ) ) ) )
let p be FinSequence of NAT ; ( len p = n implies ( ( 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)) ) & ( for n being Nat holds
( ( p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) implies ( p +* (i,n) in dom (primrec (f1,f2,i)) & (p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*> in dom f2 ) ) & ( p +* (i,n) in dom (primrec (f1,f2,i)) & (p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*> in dom f2 implies p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) ) & ( p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) implies (primrec (f1,f2,i)) . (p +* (i,(n + 1))) = f2 . ((p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*>) ) ) ) ) )
assume A4:
len p = n
; ( ( 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)) ) & ( for n being Nat holds
( ( p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) implies ( p +* (i,n) in dom (primrec (f1,f2,i)) & (p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*> in dom f2 ) ) & ( p +* (i,n) in dom (primrec (f1,f2,i)) & (p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*> in dom f2 implies p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) ) & ( p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) implies (primrec (f1,f2,i)) . (p +* (i,(n + 1))) = f2 . ((p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*>) ) ) ) )
then A5:
i in dom p
by A2, A3, FINSEQ_3:25;
A6:
p is Element of n -tuples_on NAT
by A4, FINSEQ_2:92;
hence
( p +* (i,0) in dom (primrec (f1,f2,i)) iff Del (p,i) in dom f1 )
by A5, Lm6; ( p +* (i,0) in dom (primrec (f1,f2,i)) iff (primrec (f1,f2,i)) . (p +* (i,0)) = f1 . (Del (p,i)) )
thus
( p +* (i,0) in dom (primrec (f1,f2,i)) implies (primrec (f1,f2,i)) . (p +* (i,0)) = f1 . (Del (p,i)) )
by A6, A5, Lm6; for n being Nat holds
( ( p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) implies ( p +* (i,n) in dom (primrec (f1,f2,i)) & (p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*> in dom f2 ) ) & ( p +* (i,n) in dom (primrec (f1,f2,i)) & (p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*> in dom f2 implies p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) ) & ( p +* (i,(n + 1)) in dom (primrec (f1,f2,i)) implies (primrec (f1,f2,i)) . (p +* (i,(n + 1))) = f2 . ((p +* (i,n)) ^ <*((primrec (f1,f2,i)) . (p +* (i,n)))*>) ) )
let m be Nat; ( ( 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)))*>) ) )
thus
( p +* (i,(m + 1)) in dom (primrec (f1,f2,i)) iff ( p +* (i,m) in dom (primrec (f1,f2,i)) & (p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*> in dom f2 ) )
by A6, A5, Lm6; ( 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)))*>) )
thus
( p +* (i,(m + 1)) in dom (primrec (f1,f2,i)) implies (primrec (f1,f2,i)) . (p +* (i,(m + 1))) = f2 . ((p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*>) )
by A6, A5, Lm6; verum