let i be Nat; for f1, f2 being non empty NAT * -defined to-naturals 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 )
let f1, f2 be non empty NAT * -defined to-naturals homogeneous Function; ( f1 is len-total & f2 is len-total & (arity f1) + 2 = arity f2 & 1 <= i & i <= 1 + (arity f1) implies ( dom (primrec (f1,f2,i)) = ((arity f1) + 1) -tuples_on NAT & arity (primrec (f1,f2,i)) = (arity f1) + 1 ) )
assume that
A1:
f1 is len-total
and
A2:
f2 is len-total
and
A3:
(arity f1) + 2 = arity f2
and
A4:
1 <= i
and
A5:
i <= 1 + (arity f1)
; ( dom (primrec (f1,f2,i)) = ((arity f1) + 1) -tuples_on NAT & arity (primrec (f1,f2,i)) = (arity f1) + 1 )
set n = (arity f1) + 1;
A6:
((arity f1) + 1) -tuples_on NAT c= dom (primrec (f1,f2,i))
proof
let x be
object ;
TARSKI:def 3 ( not x in ((arity f1) + 1) -tuples_on NAT or x in dom (primrec (f1,f2,i)) )
assume
x in ((arity f1) + 1) -tuples_on NAT
;
x in dom (primrec (f1,f2,i))
then reconsider x9 =
x as
Element of
((arity f1) + 1) -tuples_on NAT ;
consider G being
Function of
(((arity f1) + 1) -tuples_on NAT),
(HFuncs NAT) such that A7:
primrec (
f1,
f2,
i)
= Union G
and A8:
for
p being
Element of
((arity f1) + 1) -tuples_on NAT holds
G . p = primrec (
f1,
f2,
i,
p)
by Def11;
reconsider rngG =
rng G as non
empty functional compatible set by A7, Th10;
A9:
dom (union rngG) = union { (dom f) where f is Element of rngG : verum }
by Th11;
dom G = ((arity f1) + 1) -tuples_on NAT
by FUNCT_2:def 1;
then
G . x9 in rng G
by FUNCT_1:3;
then A10:
dom (G . x9) in { (dom f) where f is Element of rngG : verum }
;
A11:
x9 in dom (primrec (f1,f2,i,x9))
by A1, A2, A3, A4, A5, Th53;
G . x9 = primrec (
f1,
f2,
i,
x9)
by A8;
hence
x in dom (primrec (f1,f2,i))
by A7, A11, A9, A10, TARSKI:def 4;
verum
end;
dom (primrec (f1,f2,i)) c= ((arity f1) + 1) -tuples_on NAT
by Th55;
hence
dom (primrec (f1,f2,i)) = ((arity f1) + 1) -tuples_on NAT
by A6; arity (primrec (f1,f2,i)) = (arity f1) + 1
hence
arity (primrec (f1,f2,i)) = (arity f1) + 1
by Th24; verum