theorem :: ACKERMAN:56

for d being UnOp of NAT st ( for n being Nat holds d . n = Ackermann (n,n) ) holds
not dom2tuple d is primitive-recursive