Require MinMJ_L_Admis_RhoBar.
Require MinMJ_NormL.

Definition noi_rhobar1 : M->Prop :=
	[m:M](i:nat)
	 ~(Occurs_In_L (S i)
	  (rhobar (lift_M i (lift_M i m)))).

Definition noi_rhobar2 : Ms->Prop :=
	[ms:Ms](i:nat)
	 ~(Occurs_In_L (S i)
	  (rhobar (sc O (lift_Ms i (lift_Ms i ms))))).

Lemma noi_rhobar :
	((m:M)(noi_rhobar1 m))/\
	 ((ms:Ms)(noi_rhobar2 ms)).

Apply M_Ms_Height_ind.
(Induction m; Clear  m).
(Intros x ms; Generalize x ; Elim ms; Clear  x ms; Unfold noi_rhobar1;
 Unfold noi_rhobar2; Intros).
(Simpl; Apply OIL1_is_OIL4; Rewrite -> Occurs_In_L1_eq1;
 Apply OIV1_is_OIV3; Apply NOI_Lift_V4; Auto).
Apply NOI_Lift_V.

(Rewrite -> LIFTM1; Rewrite -> LIFTM1; Case H0; Clear  H0; Intros;
 Rewrite -> LIFTM4; Rewrite -> LIFTM4).
(Rewrite -> RhoBar2; Apply OIL1_is_OIL4; Rewrite -> Occurs_In_L1_eq2;
 Apply ororb1; Split).
(Apply OIV1_is_OIV3; Apply NOI_Lift_V4; Auto; Apply NOI_Lift_V).

(Apply ororb1; Split; Apply OIL1_is_OIL3).
(Clear  H; Apply H0; Auto).
(Rewrite -> HTM1; Rewrite -> HTM4; Rewrite -> S_max_nat_bridge0;
 Apply ltS; Apply lt_max_nat2; Apply ltiSi; Auto).

Case i.
(Rewrite -> Lift_Lift_Ms_Bridge1; Auto).
(Rewrite -> (Lift_Lift_Ms_Bridge1 m0); Auto).
(Apply H1; Auto).
(Rewrite -> Height_Lift_Ms; Rewrite -> HTM1; Rewrite -> HTM4;
 Rewrite -> sym_max_nat; Rewrite -> S_max_nat_bridge0; Apply ltS;
 Apply lt_max_nat2; Apply ltiSi; Auto).

Intros.
(Rewrite -> Lift_Lift_Ms_Bridge; Auto;
 Rewrite -> (Lift_Lift_Ms_Bridge m0); Auto; Apply H1; Auto).
(Rewrite -> Height_Lift_Ms; Rewrite -> HTM1; Rewrite -> HTM4;
 Rewrite -> sym_max_nat; Rewrite -> S_max_nat_bridge0; Apply ltS;
 Apply lt_max_nat2; Apply ltiSi; Auto).

(Unfold noi_rhobar1; Unfold noi_rhobar2; Intros).
(Case H0; Clear  H H0; Intros).
(Rewrite -> LIFTM2; Rewrite -> LIFTM2; Rewrite -> RhoBar3;
 Apply OIL1_is_OIL4; Rewrite -> Occurs_In_L1_eq3; Apply OIL1_is_OIL3;
 Apply H; Auto).
(Rewrite -> HTM2; Apply ltiSi; Auto).

(Intros ms; Case ms; Clear  ms; Unfold noi_rhobar1; Unfold noi_rhobar2;
 Intros).
(Simpl; Apply OIL1_is_OIL4; Auto).

(Case H; Clear  H; Intros).
(Rewrite -> LIFTM4; Rewrite -> LIFTM4; Rewrite -> RhoBar2;
 Apply OIL1_is_OIL4; Rewrite -> Occurs_In_L1_eq2; Apply ororb1; 
 Split; Auto; Apply ororb1; Split; Apply OIL1_is_OIL3).
(Apply H0; Auto).
(Rewrite -> HTM4; Rewrite -> S_max_nat_bridge0; Apply lt_max_nat2;
 Apply ltiSi; Auto).

Case i.
(Rewrite -> Lift_Lift_Ms_Bridge1; Auto;
 Rewrite -> (Lift_Lift_Ms_Bridge1 m0); Auto; Apply H;
 Rewrite -> Height_Lift_Ms; Rewrite -> HTM4;
 Rewrite -> S_max_nat_bridge0; Rewrite -> sym_max_nat;
 Apply lt_max_nat2; Apply ltiSi; Auto).

Intros.
(Rewrite -> Lift_Lift_Ms_Bridge; Auto;
 Rewrite -> (Lift_Lift_Ms_Bridge m0); Auto; Apply H; Auto;
 Rewrite -> Height_Lift_Ms; Rewrite -> HTM4;
 Rewrite -> S_max_nat_bridge0; Rewrite -> sym_max_nat;
 Apply lt_max_nat2; Apply ltiSi; Auto).
Save.

Lemma NOI_RhoBar1 :
	(m:M)(i:nat)
	 ~(Occurs_In_L (S i)
	  (rhobar (lift_M i (lift_M i m)))).

Cut ((m:M)(noi_rhobar1 m))/\
	 ((ms:Ms)(noi_rhobar2 ms)).
Intros c; Case c; Auto.
Exact noi_rhobar.
Save.

Lemma NOI_RhoBar2 :
	(ms:Ms)(i:nat)
	 ~(Occurs_In_L (S i)
	  (rhobar (sc O (lift_Ms i (lift_Ms i ms))))).

Cut ((m:M)(noi_rhobar1 m))/\
	 ((ms:Ms)(noi_rhobar2 ms)).
Intros c; Case c; Auto.
Exact noi_rhobar.
Save.

Definition norm_l_rhobar_m : M->Prop :=
	[m:M](Norm_L (rhobar m)).

Definition norm_l_rhobar_ms : Ms->Prop :=
	[ms:Ms]
	  (Norm'_L (rhobar (sc O (lift_Ms O ms)))).

Lemma norm_l_rhobar :
	((m:M)(norm_l_rhobar_m m))/\
	 ((ms:Ms)(norm_l_rhobar_ms ms)).

Apply M_Ms_Height_ind.
(Induction m; Clear  m).
(Intros x ms; Generalize x ; Elim ms; Clear  x ms; Unfold norm_l_rhobar_m;
 Unfold norm_l_rhobar_ms; Intros; Auto).
(Simpl; Auto).

(Case H0; Clear  H0 H; Intros).
(Rewrite -> RhoBar2; Apply norm_app).
(Apply H; Auto).
(Rewrite -> HTM1; Rewrite -> HTM4; Rewrite -> S_max_nat_bridge0;
 Apply ltS; Apply lt_max_nat2; Apply ltiSi; Auto).

(Apply H0; Auto).
(Rewrite -> HTM1; Rewrite -> HTM4; Rewrite -> sym_max_nat;
 Rewrite -> S_max_nat_bridge0; Apply ltS; Apply lt_max_nat2;
 Apply ltiSi; Auto).

(Unfold norm_l_rhobar_m; Unfold norm_l_rhobar_ms; Intros).
Rewrite -> RhoBar3.
(Case H0; Clear  H H0; Intros).
(Apply norm_lm; Apply H; Rewrite -> HTM2; Apply ltiSi; Auto).

(Intros ms; Case ms; Clear  ms; Unfold norm_l_rhobar_m; Unfold norm_l_rhobar_ms;
 Intros).
(Simpl; Auto).

(Rewrite -> LIFTM4; Rewrite -> RhoBar2; Apply norm'_app; Case H;
 Clear  H; Intros).
(Apply H0; Rewrite -> Height_Lift_M; Rewrite -> HTM4;
 Rewrite -> S_max_nat_bridge0; Apply lt_max_nat2; Apply ltiSi; 
 Auto).

(Apply H; Auto).
(Rewrite -> Height_Lift_Ms; Rewrite -> HTM4; Rewrite -> sym_max_nat;
 Rewrite -> S_max_nat_bridge0; Apply lt_max_nat2; Apply ltiSi; 
 Auto).

(Rewrite <- Lift_RhoBar_Bridge; Apply NOI_Lift_L).
Apply NOI_RhoBar2.
Save.

Lemma Norm_L_RhoBar : (m:M)
	(Norm_L (rhobar m)).

Cut ((m:M)(norm_l_rhobar_m m))/\
	 ((ms:Ms)(norm_l_rhobar_ms ms)).
Intros c; Case c; Auto.
Exact norm_l_rhobar.
Save.

Lemma Norm'_L_RhoBar : (ms:Ms)
	(Norm'_L (rhobar (sc O (lift_Ms O ms)))).

Cut ((m:M)(norm_l_rhobar_m m))/\
	 ((ms:Ms)(norm_l_rhobar_ms ms)).
Intros c; Case c; Auto.
Exact norm_l_rhobar.
Save.