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)).



Hint norm_vr.
Hint norm_app.
Hint norm_lm.
Hint norm'_vr.
Hint norm'_app.


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)).


(Intros; Split).
Exact (Norm_Norm'_L_ind1 P P0 H H0 H1 H2 H3).

Exact (Norm'_Norm_L_ind1 P P0 H H0 H1 H2 H3).
Save.

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.

Auto.
Save.

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

Auto.
Save.

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

Auto.
Save.

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

Auto.
Save.

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))))).

Auto.
Save.

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

Auto.
Save.

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

(Induction l; Clear  l; Intros; Auto).
(Split; Intros; Auto).
(Inversion_clear H; Auto).

(Case H0; Clear  H0; Intros).
(Case H; Clear  H; Intros).
(Split; Intros).
Inversion_clear H3.
Rewrite -> NMLB2.
(Rewrite -> H; Auto).

(Inversion_clear H3; Rewrite -> NMLB5).
(Rewrite -> H; Auto).
(Rewrite -> nateqb_is_eq1; Auto).
(Rewrite -> OIL1_is_OIL3; Auto).
(Rewrite -> OIL1_is_OIL3; Auto).

(Split; Intros).
(Inversion_clear H0; Case H; Clear  H; Intros; Rewrite -> NMLB3).
(Apply H; Auto).

Inversion_clear H0.
Save.

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

(Intros;
 Cut (l:L)
      (and (Norm_L l)->(eq ? (Norm_Lb l) true)
        (Norm'_L l)->(eq ? (Norm'_Lb l) true))).
(Intros c; Case (c l); Auto).

Exact nmlb1_is_nmlb1.
Save.

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

(Intros;
 Cut (l:L)
      (and (Norm_L l)->(eq ? (Norm_Lb l) true)
        (Norm'_L l)->(eq ? (Norm'_Lb l) true))).
(Intros c; Case (c l); Auto).

Exact nmlb1_is_nmlb1.
Save.

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

(Induction l; Clear  l; Intros; Split; Intros; Auto).
Simpl in H.
(Rewrite -> (nateqb_is_eq2 v O); Auto).

(Case H; Clear  H; Intros; Case H0; Clear  H0; Intros).
(Generalize H1 ; Clear  H1; Rewrite -> NMLB2; Intros).
Apply norm_app.
Apply H.
(Generalize H1 ; Clear  H1; Case (Norm_Lb l); Auto).

(Apply H3; Generalize H1 ; Case (Norm'_Lb l0); Auto).
(Rewrite -> sym_andb; Auto).

(Case H; Clear  H; Intros; Case H0; Clear  H0; Intros).
(Generalize H1 ; Clear  H1; Rewrite -> NMLB5; Intros).
Rewrite -> (nateqb_is_eq2 v O).
Apply norm'_app.
(Apply H; Generalize H1 ; Clear  H1; Case (Norm_Lb l); Auto).
Simpl.
(Rewrite -> andbf; Rewrite -> andbf; Rewrite -> andbf; Auto).

(Apply H3; Generalize H1 ; Clear  H1; Case (Norm'_Lb l0); Auto).
(Rewrite -> andbf; Rewrite -> andbf; Rewrite -> andbf;
 Rewrite -> andbf; Auto).

(Apply OIL1_is_OIL4; Generalize H1 ; Clear  H1).
(Case (Occurs_In_L1 O l); Auto).
(Simpl; Rewrite -> andbf; Auto).

(Apply OIL1_is_OIL4; Generalize H1 ; Clear  H1;
 Case (Occurs_In_L1 (S O) l0); Auto; Simpl; Rewrite -> andbf;
 Rewrite -> andbf; Auto).

(Generalize H1 ; Clear  H1; Case (nateqb v O); Auto).

(Case H; Clear  H; Intros; Simpl in H0).
(Apply norm_lm; Apply H; Auto).

(Simpl in H0; Discriminate H0).
Save.

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

(Intros;
 Cut (l:L)
	 ((Norm_Lb l)=true->
	  (Norm_L l))/\
	 ((Norm'_Lb l)=true->
	  (Norm'_L l))).
(Intros c; Case (c l); Auto).

Exact nmlb1_is_nmlb2.
Save.

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

(Intros;
 Cut (l:L)
	 ((Norm_Lb l)=true->
	  (Norm_L l))/\
	 ((Norm'_Lb l)=true->
	  (Norm'_L l))).
(Intros c; Case (c l); Auto).

Exact nmlb1_is_nmlb2.
Save.

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

Unfold not .
Intros.
Apply bool_dec5.
Unfold not .
Intros.
Apply H.
(Apply NMLB1_is_NMLB2; Auto).
Save.

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

Unfold not .
Intros.
Apply bool_dec5.
Unfold not .
Intros.
Apply H.
(Apply NM'LB1_is_NM'LB2; Auto).
Save.

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

Intros.
Cut (not (eq ? (Norm_Lb l) true)).
(Unfold not ; Intros; Apply H0; Apply NMLB1_is_NMLB1; Auto).

(Apply bool_dec6; Auto).
Save.

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

Intros.
Cut (not (eq ? (Norm'_Lb l) true)).
(Unfold not ; Intros; Apply H0; Apply NM'LB1_is_NM'LB1; Auto).

(Apply bool_dec6; Auto).
Save.

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

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

(Unfold NML_compare ; Intros).
Cut (or (eq ? (Norm_Lb l) true) (eq ? (Norm_Lb l) false)).
(Intros c; Case c; Clear  c; Intros).
(Left; Apply NMLB1_is_NMLB2; Auto).

(Right; Apply NMLB1_is_NMLB4; Auto).

(Case (Norm_Lb l); Auto).
Save.

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

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

(Unfold NM'L_compare ; Intros).
Cut (or (eq ? (Norm'_Lb l) true) (eq ? (Norm'_Lb l) false)).
(Intros c; Case c; Clear  c; Intros).
(Left; Apply NM'LB1_is_NM'LB2; Auto).

(Right; Apply NM'LB1_is_NM'LB4; Auto).

(Case (Norm'_Lb l); Auto).
Save.

Hint NML_dec.
Hint NM'L_dec.
Hint norm_vr.
Hint norm_app.
Hint norm_lm.
Hint norm'_vr.
Hint norm'_app.