Require Export MinMJ_NormL.
Require Export MinMJ_PermDef.
Require Export MinMJ_HeightL.

Lemma perm_not_norm_l1 :
	(l0,l1,l2:L)(x:V)
	 (Occurs_In_L O l1)->
	  ~(Norm_L (app x l0 (app O l1 l2))).

(Unfold not ; Intros; Inversion_clear H0; Inversion_clear H2; Apply H4;
 Auto).
Save.

Lemma perm_not_norm_l2 :
	(l0,l1,l2:L)(x:V)
	 (Occurs_In_L (S O) l2)->
	  ~(Norm_L (app x l0 (app O l1 l2))).

(Unfold not ; Intros; Inversion_clear H0; Inversion_clear H2; Apply H5;
 Auto).
Save.

Lemma Norm'_Norm_L :
	(l:L)
	 (Norm'_L l)->
	  (Norm_L l).

(Induction l; Clear  l; Intros; Auto).
Inversion_clear H1.
(Apply norm_app; Auto).

Inversion H0.
Save.

Hint Norm'_Norm_L.

Lemma Perm_not_norm_l : 
	(l0,l1:L)
	 (L_Perm1 l0 l1)->
	  ~(Norm_L l0).

(Intro;
 Apply L_Height_ind with P:=[l0:L](l1:L)(L_Perm1 l0 l1)->~(Norm_L l0);
 Clear  l0; Induction l0; Clear  l0; Intros).
Inversion_clear H0.

Inversion_clear H2.
(Unfold not; Intros; Inversion_clear H2).
Cut (lt (Height_L l) (Height_L (app v l l0))).
Intros.
Apply (H1 l H2 l12 H3 H4).

(Simpl; Apply lt_max_nat1; Auto).

(Unfold not; Intros; Inversion_clear H2).
(Cut (Norm_L l0); Auto; Intros).
Cut (lt (Height_L l0) (Height_L (app v l l0))).
Intros.
Apply (H1 l0 H6 l22 H3 H2).

(Simpl; Rewrite -> sym_max_nat; Apply lt_max_nat1; Auto).

(Unfold not; Intros; Apply H3).
Inversion_clear H2.
(Inversion_clear H5; Auto).

(Unfold not; Intros; Inversion_clear H2).
Inversion_clear H6.

(Case H3; Clear  H3; Intros).
(Apply perm_not_norm_l1; Auto).

(Apply perm_not_norm_l2; Auto).

(Unfold not; Intros; Inversion_clear H2).
Inversion_clear H4.

Inversion_clear H1.
(Unfold not; Intros).
(Cut (lt (Height_L l) (Height_L (lm l))); Auto; Intros).
Inversion_clear H1.
Apply (H0 l H3 l2 H2 H4).

(Simpl; Auto).
Save.

Lemma Perm_Not_Norm_L :
	(l0,l1:L)
	 (L_Perm1 l0 l1)->
	  ~(Norm_L l0).

(Intros; Exact (Perm_not_norm_l l0 l1 H)).
Save.

Lemma Norm_Imperm_L :
	(l0,l1:L)
	 (Norm_L l0)->
	  ~(L_Perm1 l0 l1).

(Unfold not; Intros; Apply (Perm_not_norm_l l0 l1 H0 H)).
Save.