From Undecidability.L Require Import Datatypes.LNat Tactics.LTactics.
Import Ring.


Fixpoint ackermann n : :=
  match n with
    0 S
  | S n fix ackermann_Sn m : :=
            match m with
              0 ( _ ackermann n 1)
            | S m ( _ ackermann n (ackermann_Sn m))
            end true
  end.

Lemma term_ackermann : computable ackermann.
Proof.
  extract.
Qed.


Local Lemma Ack_pos n m : 0 < ackermann n m.
Proof.
  revert m.
  induction n as [n IHn] using lt_wf_ind. intros m.
  induction m as [m IHm] using lt_wf_ind.
  destruct n. all:destruct m.
  all:eauto.
  all:cbn in *. all:try .
  all:eauto.
Qed.


Import Ring Arith. Import .
Lemma termT_ackermann :
  computableTime' ackermann
                 ( x _
                    (14,
                      y _
                       (cnst("f",x,y),tt))).
Proof.
  extract.
  cbn. fold ackermann.
  repeat (cbn ;intros;intuition idtac;try destruct _).
  all:ring_simplify. all:try nia.
  all:repeat change (fix ackermann_Sn (m : ) : :=
    match m with
    | 0 _ ackermann 1
    | S _ ackermann (ackermann_Sn )
    end true) with (ackermann (S )). all: refine ( _:(_ _)).
Abort.