Require Import Arith.
Fixpoint A m := fix A_m n :=
  match m with
    | 0 => n + 1
    | S pm =>
      match n with
        | 0 => A pm 1
        | S pn => A pm (A_m pn)
      end
  end.