Require Export MinMJ_PermDef.
Require Export MinMJ_Normal_RhoBar.
Require Export MinMJ_Strength.
Require Export MinMJ_Bridge3.

Inductive
    L_Permn : L->L->Prop :=
	l_permn_base :
	    (l0,l1:L)
	       l0=l1->
	        (L_Permn l0 l1) |
	l_permn_rec :
	    (l0,l1,l2:L)
	     (L_Perm1 l0 l1)->
	      (L_Permn l1 l2)->
	       (L_Permn l0 l2).

Scheme L_Permn_ind1 := Induction for L_Permn Sort Prop.

Definition l_admis_perm1 :
	(l,l0:L)(L_Perm1 l l0)->Prop :=
	 [l,l0:L][d:(L_Perm1 l l0)]
	   (h:Hyps)(P:F)(L_Deriv h l P)->
	    (L_Deriv h l0 P).

Lemma L_admis_perm1 :
	(l,l0:L)(D:(L_Perm1 l l0))
	 (l_admis_perm1 l l0 D).

Lemma L_Admis_Perm1 :
	(l,l0:L)(h:Hyps)(P:F)
	 (L_Perm1 l l0)->
	  (L_Deriv h l P)->
	   (L_Deriv h l0 P).

Lemma L_Perm1n :
	(l,l0:L)
	 (L_Perm1 l l0)->
	  (L_Permn l l0).

Definition l_permnn : (l,l0:L)(L_Permn l l0)->Prop :=
	[l,l0:L][d:(L_Permn l l0)]
	 (l1:L)
	  (L_Permn l0 l1)->
	   (L_Permn l l1).

Lemma L_permnn :
	(l,l0:L)(d:(L_Permn l l0))
	 (l_permnn l l0 d).

Lemma L_Permnn :
	(l,l0,l1:L)
	 (L_Permn l l0)->
	  (L_Permn l0 l1)->
	   (L_Permn l l1).

Definition l_permn_app1 :
	(l,l0:L)(L_Permn l l0)->Prop :=
	 [l,l0:L][D:(L_Permn l l0)]
	  (x:V)(l1:L)
	   (L_Permn (app x l l1) (app x l0 l1)).

Lemma L_permn_app1 :
	(l,l0:L)(D:(L_Permn l l0))
	 (l_permn_app1 l l0 D).

Lemma L_Permn_app1 :
	(l,l0,l1:L)(x:V)
	 (L_Permn l l0)->
	  (L_Permn (app x l l1) (app x l0 l1)).

Definition l_permn_app2 :
	(l0,l1:L)(L_Permn l0 l1)->Prop :=
	 [l0,l1:L][D:(L_Permn l0 l1)]
	  (x:V)(l:L)
	   (L_Permn (app x l l0) (app x l l1)).

Lemma L_permn_app2 :
	(l0,l1:L)(D:(L_Permn l0 l1))
	 (l_permn_app2 l0 l1 D).

Lemma L_Permn_app2 :
	(l,l0,l1:L)(x:V)
	 (L_Permn l0 l1)->
	  (L_Permn (app x l l0) (app x l l1)).

Lemma L_Permn_app :
	(x:V)(l0,l1,l2,l3:L)
	 (L_Permn l0 l1)->
	   (L_Permn l2 l3)->
	    (L_Permn (app x l0 l2) (app x l1 l3)).

Definition l_permn_lm :
	(l0,l1:L)(L_Permn l0 l1)->Prop :=
	 [l0,l1:L][d:(L_Permn l0 l1)]
	    (L_Permn (lm l0) (lm l1)).

Lemma L_permn_lm :
	(l0,l1:L)(d:(L_Permn l0 l1))
	 (l_permn_lm l0 l1 d).

Lemma L_Permn_lm :
	(l,l0:L)
	 (L_Permn l l0)->
	  (L_Permn (lm l) (lm l0)).

Definition l_admis_permn :
	(l,l0:L)(L_Permn l l0)->Prop :=
	 [l,l0:L][d:(L_Permn l l0)]
	  (h:Hyps)(P:F)
	   (L_Deriv h l P)->
	    (L_Deriv h l0 P).

Lemma L_admis_permn :
	(l,l0:L)(d:(L_Permn l l0))
	 (l_admis_permn l l0 d).

Lemma L_Admis_Permn :
	(h:Hyps)(l0,l1:L)(P:F)
	 (L_Permn l0 l1)->
	  (L_Deriv h l0 P)->
	   (L_Deriv h l1 P).

(*
Definition hv_rhobar_m : M->Prop :=
	[m:M](x:V)(l1,l2:L)
	(rhobar m)=(app x l1 l2)->
	 (HV_L l2)=O.

Definition hv_rhobar_ms : Ms->Prop :=
	[ms:Ms]
	 (HV_L (rhobar (sc O ms)))=O.

Lemma HV_rhobar_m :
	((m:M)(hv_rhobar_m m))/\
	 ((ms:Ms)(hv_rhobar_ms ms)).

Apply M_Ms_Height_ind.
(Destruct m; Clear  m).
(Intros x ms; Generalize x ; Case ms; Clear  x ms; Unfold hv_rhobar_m;
 Unfold hv_rhobar_ms; Intros).
(Case H; Clear  H; Intros).
(Simpl in H0; Discriminate H0).

(Generalize H0 ; Clear  H0; Rewrite -> RhoBar2; Intros;
 Injection H0; Clear  H0; Intros).
Rewrite <- H0.
(Case H; Clear  H; Intros).
(Apply H3; Auto).
(Rewrite -> Height_Lift_Ms; Rewrite -> HTM1; Rewrite -> HTM4;
 Rewrite -> sym_max_nat; Apply ltS; Apply lt_max_nat1; Auto).

(Unfold hv_rhobar_m; Unfold hv_rhobar_ms; Intros).
(Simpl in H0; Discriminate H0).

(Destruct ms; Clear  ms; Unfold hv_rhobar_ms; Unfold hv_rhobar_m;
 Intros).
Auto.

Rewrite -> RhoBar2.
Rewrite -> HV_L_eq2.
(Case H; Clear  H; Intros).
(Rewrite -> H; Auto).
(Rewrite -> Height_Lift_Ms; Rewrite -> HTM4; Rewrite -> sym_max_nat;
 Apply lt_max_nat1; Auto).
Save.

Lemma HV_rhobar1 :
	(ms:Ms)
	 (HV_L (rhobar (sc O ms)))=O.

Cut ((m:M)(hv_rhobar_m m))/\((ms:Ms)(hv_rhobar_ms ms)).
(Intros c; Case c; Auto).

Exact HV_rhobar_m.
Save.

Lemma HV_rhobar :
	(m:M)(x:V)(l1,l2:L)
	(rhobar m)=(app x l1 l2)->
	 (HV_L l2)=O.

Cut ((m:M)(hv_rhobar_m m))/\((ms:Ms)(hv_rhobar_ms ms)).
(Intros c; Case c; Auto).

Exact HV_rhobar_m.
Save.
*)

Definition oi_rhobar_m : M->Prop :=
	[m:M](x:V)
	 (Occurs_In_M x m)->
	  (Occurs_In_L x (rhobar m)).

Definition oi_rhobar_ms : Ms->Prop :=
	[ms:Ms](x,y:V)
	 (Occurs_In_Ms x ms)->
	  (Occurs_In_L (S x) (rhobar (sc y (lift_Ms O ms)))).

Lemma oi_rhobar_M :
	((m:M)(oi_rhobar_m m))/\
	 ((ms:Ms)(oi_rhobar_ms ms)).

Lemma OI_RhoBar_M :
	(m:M)(x:V)
	 (Occurs_In_M x m)->
	  (Occurs_In_L x (rhobar m)).

Lemma OI_RhoBar_Ms :
	(ms:Ms)(x,y:V)
	 (Occurs_In_Ms x ms)->
	  (Occurs_In_L (S x) (rhobar (sc y (lift_Ms O ms)))).

Lemma NOI_RhoBar_M :
	(m:M)(x:V)
	 ~(Occurs_In_L x (rhobar m))->
	  ~(Occurs_In_M x m).

Lemma NOI_RhoBar_Ms :
	(ms:Ms)(x:V)
	 ~(Occurs_In_L (S x) (rhobar (sc O (lift_Ms O ms))))->
	  ~(Occurs_In_Ms x ms).

Definition oi_rhobar_m1 : M->Prop :=
	[m:M](x:V)
	 (Occurs_In_L x (rhobar m))->
	  (Occurs_In_M x m).

Definition oi_rhobar_ms1 : Ms->Prop :=
	[ms:Ms](x:V)
	 (Occurs_In_L (S x) (rhobar (sc O (lift_Ms O ms))))->
	  (Occurs_In_Ms x ms).

Lemma oi_rhobar_M1 :
	((m:M)(oi_rhobar_m1 m))/\
	 ((ms:Ms)(oi_rhobar_ms1 ms)).

Lemma OI_RhoBar_M1 :
	(x:V)(m:M)
	 (Occurs_In_L x (rhobar m))->
	  (Occurs_In_M x m).

Lemma OI_RhoBar_Ms1 :
	(x:V)(ms:Ms)
	 (Occurs_In_L (S x) (rhobar (sc O (lift_Ms O ms))))->
	  (Occurs_In_Ms x ms).

Lemma NOI_RhoBar_M1 :
	(x:V)(m:M)
	 ~(Occurs_In_M x m)->
	  ~(Occurs_In_L x (rhobar m)).

Lemma NOI_RhoBar_Ms1 :
	(x:V)(ms:Ms)
	 ~(Occurs_In_Ms x ms)->
	  ~(Occurs_In_L (S x) (rhobar (sc O (lift_Ms O ms)))).

Lemma Drop_RhoBar_Bridge :
	(x:V)(m:M)
	 ~(Occurs_In_M x m)->
	  (drop_L x (rhobar m))=
	   (rhobar (drop_M x m)).

Lemma Drop_Lift_M_Bridge1 :
	(m:M)(i,j:nat)
         ~(Occurs_In_M i m)->
          (lt j (S i))->
           (drop_M (S i) (lift_M j m))=(lift_M j (drop_M i m)).

Lemma Drop_Lift_Ms_Bridge1 :
	(ms:Ms)(i,j:nat)
	 ~(Occurs_In_Ms i ms)->
          (lt j (S i))->
           (drop_Ms (S i) (lift_Ms j ms))=(lift_Ms j (drop_Ms i ms)).

Definition app_red_m : M->Prop :=
	[m:M](x:V)(m1:M)
	  (L_Permn (app x (rhobar m1) (rhobar m))
		   (rhobar (MsubstVMV x m1 O m))).

Definition app_red_ms : Ms->Prop :=
	[ms:Ms](x,y:V)(m1:M)
	  (L_Permn (app x (rhobar m1) (rhobar (sc y ms)))
		   (app x (rhobar m1) (rhobar (sc y ms)))).

Lemma app_red :
	((m:M)(app_red_m m))/\
	 ((ms:Ms)(app_red_ms ms)).

Lemma App_Red_M :
	(x:V)(m1,m:M)
	 (L_Permn (app x (rhobar m1) (rhobar m))
		  (rhobar (MsubstVMV x m1 O m))).

Lemma Norm_Red :
	(l:L)(L_Permn l (rhobar (phibar l))).