Require Export MinMJ_Occurs.

Mutual Inductive
    Norm_L : L->Prop :=
	norm_vr : (x:V)(Norm_L (vr x)) |
	norm_app :
		(x:V)(l1,l2:L)
		 (Norm_L l1)->
		  (Norm'_L l2)->
		   (Norm_L (app x l1 l2)) |
	norm_lm :
		(l:L)
		 (Norm_L l)->
		  (Norm_L (lm l))
with
    Norm'_L : L->Prop :=
	norm'_vr : (Norm'_L (vr O)) |
	norm'_app :
		(l1,l2:L)
		 (Norm_L l1)->
		  (Norm'_L l2)->
		   ~(Occurs_In_L O l1)->
		    ~(Occurs_In_L (S O) l2)->
		     (Norm'_L (app O l1 l2)).

Scheme Norm_Norm'_L_ind1 := Induction for Norm_L Sort Prop
  with Norm'_Norm_L_ind1 := Induction for Norm'_L Sort Prop.

Lemma Norm_Norm'_L_ind :
	(P:(l:L)(Norm_L l)->Prop)
        (P0:(l:L)(Norm'_L l)->Prop)
         ((x:V)(P (vr x) (norm_vr x)))
          ->((x:V)
              (l1,l2:L)
               (n:(Norm_L l1))
                (P l1 n)
                 ->(n0:(Norm'_L l2))
                    (P0 l2 n0)
                     ->(P (app x l1 l2) (norm_app x l1 l2 n n0)))
             ->((l:L)(n:(Norm_L l))(P l n)->(P (lm l) (norm_lm l n)))
                ->(P0 (vr O) norm'_vr)
                   ->((l1,l2:L)
                       (n:(Norm_L l1))
                        (P l1 n)
                         ->(n0:(Norm'_L l2))
                            (P0 l2 n0)
                             ->(n1:~(Occurs_In_L O l1))
                                (n2:~(Occurs_In_L (S O) l2))
                                 (P0 (app O l1 l2)
                                   (norm'_app l1 l2 n n0 n1 n2)))
                      ->((l:L)(n:(Norm_L l))(P l n))/\
			((l:L)(n:(Norm'_L l))(P0 l n)).

Fixpoint
    Norm_Lb [l:L] : bool :=
	<bool>Case l of
	    (* vr x *)[x:V]
		true
	    (* app x l0 l1 *)[x:V][l0,l1:L]
		(andb (Norm_Lb l0)
		      (Norm'_Lb l1))
	    (* .\ l *)[l:L]
		(Norm_Lb l)
	end with
    Norm'_Lb [l:L] : bool :=
	<bool>Case l of
	    (* vr x *)[x:V]
		(nateqb x O)
	    (* app x l0 l1 *)[x:V][l0,l1:L]
		(andb (nateqb x O)
		(andb (negb (Occurs_In_L1 O l0))
		(andb (negb (Occurs_In_L1 (S O) l1))
		(andb (Norm_Lb l0)
		      (Norm'_Lb l1)))))
	    (* .\ l *)[l:L]
		false
	end.

Lemma NMLB1 :
	(x:V)
	 (Norm_Lb (vr x))=true.

Lemma NMLB2 :
	(x:V)(l0,l1:L)
	 (Norm_Lb (app x l0 l1))=
	 (andb (Norm_Lb l0)
	       (Norm'_Lb l1)).

Lemma NMLB3 :
	(l:L)
	 (Norm_Lb (lm l))=
	  (Norm_Lb l).

Lemma NMLB4 :
	(x:V)
	 (Norm'_Lb (vr x))=
	  (nateqb x O).

Lemma NMLB5 :
	(x:V)(l0,l1:L)
	 (Norm'_Lb (app x l0 l1))=
	 (andb (nateqb x O)
	 (andb (negb (Occurs_In_L1 O l0))
	 (andb (negb (Occurs_In_L1 (S O) l1))
	 (andb (Norm_Lb l0)
	       (Norm'_Lb l1))))).

Lemma NMLB6 :
	(l:L)
	 (Norm'_Lb (lm l))=
	  false.

Lemma nmlb1_is_nmlb1 :
	(l:L)
	 ((Norm_L l)->
	  (Norm_Lb l)=true)/\
	 ((Norm'_L l)->
	  (Norm'_Lb l)=true).

Lemma NMLB1_is_NMLB1 :
	(l:L)
	 ((Norm_L l)->
	  (Norm_Lb l)=true).

Lemma NM'LB1_is_NM'LB1 :
	(l:L)
	 ((Norm'_L l)->
	  (Norm'_Lb l)=true).

Lemma nmlb1_is_nmlb2 :
	(l:L)
	 ((Norm_Lb l)=true->
	  (Norm_L l))/\
	 ((Norm'_Lb l)=true->
	  (Norm'_L l)).

Lemma NMLB1_is_NMLB2 :
	(l:L)
	 ((Norm_Lb l)=true->
	  (Norm_L l)).

Lemma NM'LB1_is_NM'LB2 :
	(l:L)
	 ((Norm'_Lb l)=true->
	  (Norm'_L l)).

Lemma NMLB1_is_NMLB3 :
	(l:L)
	 (~(Norm_L l)->
	  (Norm_Lb l)=false).

Lemma NM'LB1_is_NM'LB3 :
	(l:L)
	 (~(Norm'_L l)->
	  (Norm'_Lb l)=false).

Lemma NMLB1_is_NMLB4 :
	(l:L)
	 ((Norm_Lb l)=false->
	  ~(Norm_L l)).

Lemma NM'LB1_is_NM'LB4 :
	(l:L)
	 ((Norm'_Lb l)=false->
	  ~(Norm'_L l)).

Definition NML_compare : L->Prop :=
	[l:L]
	 ((Norm_L l)\/~(Norm_L l)).

Lemma NML_dec : (l:L)(NML_compare l).

Definition NM'L_compare : L->Prop :=
	[l:L]
	 ((Norm'_L l)\/~(Norm'_L l)).

Lemma NM'L_dec : (l:L)(NM'L_compare l).