let d be UnOp of NAT; :: thesis: ( ( for n being Nat holds d . n = Ackermann (n,n) ) implies not dom2tuple d is primitive-recursive )
assume A1: for n being Nat holds d . n = Ackermann (n,n) ; :: thesis: not dom2tuple d is primitive-recursive
set g = dom2tuple d;
assume dom2tuple d is primitive-recursive ; :: thesis: contradiction
then dom2tuple d in PrimRec by COMPUT_1:def 16;
then dom2tuple d in majorizedBy AckermannFunction by Th53;
then consider h being NAT * -defined to-naturals homogeneous Function such that
A2: h = dom2tuple d and
A3: AckermannFunction majorizes h ;
consider N being Element of NAT such that
A4: for F being non empty FinSequence of NAT st F in dom h holds
for a being Element of NAT st a = max (rng F) holds
h . F < AckermannFunction . (N,a) by A3;
reconsider F = <*N*> as non empty FinSequence of NAT ;
A5: dom d = NAT by FUNCT_2:def 1;
then A6: dom (dom2tuple d) = 1 -tuples_on NAT by Def4;
rng F = {N} by FINSEQ_1:38;
then A7: max (rng F) = N by XXREAL_2:11;
(dom2tuple d) . F = d . N by A5, Def4
.= Ackermann (N,N) by A1 ;
hence contradiction by A2, A4, A6, A7, FINSEQ_2:98; :: thesis: verum