let i be Element of NAT ; :: thesis: 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; :: thesis: ( (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 & i <= (arity f1) + 1 ) ; :: thesis: primrec f1,f2,i is_primitive-recursively_expressed_by f1,f2,i
set g = primrec f1,f2,i;
take n = (arity f1) + 1; :: according to COMPUT_1:def 12 :: thesis: ( 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 Element of 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 dom (primrec f1,f2,i) c= n -tuples_on NAT by Th60; :: thesis: ( 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 Element of 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; :: thesis: ( (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 Element of 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 ; :: thesis: ( 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 Element of 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; :: thesis: 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 Element of 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 ; :: thesis: ( 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 Element of 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 A3: len p = n ; :: thesis: ( ( 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 Element of 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 A4: p is Element of n -tuples_on NAT by FINSEQ_2:110;
A5: i in dom p by A2, A3, FINSEQ_3:27;
hence ( p +* i,0 in dom (primrec f1,f2,i) iff Del p,i in dom f1 ) by A4, Lm6; :: thesis: ( 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 A4, A5, Lm6; :: thesis: for n being Element of 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 Element of NAT ; :: thesis: ( ( 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 A4, A5, Lm6; :: thesis: ( 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 A4, A5, Lm6; :: thesis: verum