(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

Require subst0_gen.
Require dnf_dec.
Require pr0_gen.
Require nf0_dec.
Require nf2_defs.

   Section nf2_dec. (********************************************************)

      Lemma nf2_dec: (c:?; t1:?) (nf2 c t1) \/
                     (EX t2 | (t1 = t2 -> (P:Prop) P) & (pr2 c t1 t2)).
      Proof.
      Unfold nf2; XElimUsing c_tail_ind c; Intros.
(* case 1: CSort *)
      XDecomPose '(nf0_dec t1).
(* case 1.1: t1 is normal *)
      Left; Intros; Pr2GenBase; XAuto.
(* case 1.2: t1 is not normal *)
      XDEAuto 4.
(* case 2: CHead *)
      XDecomPoseClear H '(H t1).
(* case 2.1: t1 is normal *)
      NewInduction k.
(* case 2.1.1: Bind *)
      NewInduction b.
(* case 2.1.1.1: Abbr *)
      XDecomPose '(dnf_dec t t1 (clen c)); Subst.
(* case 2.1.1.1.1: last variable free in t1 *)
      Clear H0; XDecomPose '(getl_ctail_clen Abbr t c).
      Right; EApply ex2_intro; [ Idtac | EApply pr2_delta; XDEAuto 2 ].
      Intros; Subst; Subst0Gen.
(* case 2.1.1.1.2: last variable bound in t1 *)
      Left; Intros; Pr2GenBase; XInv;
      Try (Pr0Gen; Subst; Subst0Gen); XAuto.
(* case 2.1.1.2: Abst *)
      Left; Intros; Pr2GenBase; XInv; XAuto.
(* case 2.1.1.3: Void *)
      Left; Intros; Pr2GenBase; XInv; XAuto.
(* case 2.1.2: Flat *)
      Left; Intros; Pr2GenBase; XInv; XAuto.
(* case 2.2: t1 is not normal *)
      XDEAuto 4.
      Qed.

   End nf2_dec.