dom2tuple (AckermannFunction m) = AckermannSequence . m by Th39;
hence dom2tuple (AckermannFunction m) is primitive-recursive ; :: thesis: verum