Require MinMJ_Lifts.
Require MinMJ_HeightM.

(* The Mapping RhoBar from MJ to LJ. *)
Fixpoint 
    rhobar [m:M] : L :=
	<L>Case m of
	    (* x;ms *)[x:V][ms:Ms]
		<L>Case ms of
		    (* mnil *)
			(vr x)
		    (* m::ms *)[m:M][ms:Ms]
			(app x (rhobar m) (rhobar' ms (S O)))
		end
	    (* \m *)[m:M]
		(lm (rhobar m))
	end
with
    rhobar' [ms:Ms] : nat->L :=
	[i:nat]
	<L>Case ms of
	    (* mnil *)
		(vr O)
	    (* m::ms *)[m:M][ms:Ms]
		(app O (lifts_L i O (rhobar m)) (rhobar' ms (S i)))
	end.

Recursive Definition rhobar1 : nat->Ms->L :=
i ms => (rhobar' ms i).

Recursive Definition rho : N->L :=
n => (rhobar (psi n)).

Lemma rhothetarhobar : (m:M)
	(rho (theta m))=(rhobar m).

(Intros; Rewrite -> rho_eq1; Rewrite -> psitheta; Auto).
Save.

Lemma Rhobar1 : (x:V)
	(rhobar (sc x mnil))=(vr x).

Auto.
Save.

Lemma Rhobar2 : (x:V)(m:M)
	(rhobar (sc x (mcons m mnil)))=
	 (app x (rhobar m) (vr O)).

Auto.
Save.

Lemma Rhobar3 : (x:V)(m:M)(ms:Ms)
	(rhobar (sc x (mcons m ms)))=
	 (app x (rhobar m) (rhobar1 (S O) ms)).

Auto.
Save.

Lemma Rhobar4 : (m:M)
	(rhobar (lambda m))=(lm (rhobar m)).

Auto.
Save.

Lemma Rhobar5 : (i:nat)
	(rhobar1 i mnil)=(vr O).

Auto.
Save.

Lemma Rhobar6 : (m:M)(ms:Ms)(i:nat)
	(rhobar1 i (mcons m ms))=
	 (app O
	      (lifts_L i O (rhobar m))
	      (rhobar1 (S i) ms)).

Auto.
Save.

Definition phibarrhobar1 : M->Prop :=
	[m:M]
	 (phibar (rhobar m))=m.

Definition phibarrhobar2 : Ms->Prop :=
	[ms:Ms]
	 (m:M)(i:nat)
	  ((m1:M)
	    (lt (Height_M m1) (Height_Ms (mcons m ms)))->
	     (phibar (rhobar m1))=m1)->
	   (phibar (rhobar1 i (mcons m ms)))=
	    (sc O (lifts_Ms i O (mcons m ms))).
	  

Lemma Phibarrhobar :
	((m:M)(phibarrhobar1 m))/\
	 ((ms:Ms)(phibarrhobar2 ms)).

(Apply M_Ms_Height_ind; Unfold phibarrhobar1; Unfold phibarrhobar2;
 Intros).
(Case H; Clear  H; Elim m; Clear  m).
(Intros x ms; Generalize x ; Elim ms; Clear  ms; Intros; Auto).
(Rewrite -> Rhobar3; Rewrite -> phibar_eq2).
(Clear  H; Rewrite -> H0; Auto; Clear  x).
(Generalize x0 m H0 H1 ; Elim m0; Clear  H0 H1 x0 m m0; Intros).
(Rewrite -> Rhobar5; Rewrite -> phibar_eq1; Rewrite -> MSVMV1).
(Rewrite -> nateqb_is_eq1; Auto; Unfold Setifb;
 Rewrite -> MSVMV3; Auto).

(Clear  H; Rewrite -> H1; Auto).
(Rewrite -> MSVMV1; Rewrite -> nateqb_is_eq1; 
 Auto; Unfold Setifb).
(Rewrite -> Lifts_Ms_rec1; Rewrite -> NOI_Mssub_Bridge).
(Rewrite -> Drop_Lift_Ms; Auto).
(Rewrite -> Lifts_Ms0; Auto).

Apply NOI_Lift_Ms.

(Rewrite -> HTM1; Apply ltS; Rewrite -> HTM4; Rewrite -> sym_max_nat;
 Apply ltS; Apply lt_max_nat2; Rewrite -> HTM4; Rewrite -> sym_max_nat;
 Apply lt_max_nat1; Auto).

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

(Rewrite -> HTM1; Apply ltS; Rewrite -> HTM4; Apply lt_max_nat1; Auto).

(Intros; Rewrite -> Rhobar4; Rewrite -> phibar_eq3; Rewrite -> H0; Auto).
(Rewrite -> HTM2; Apply ltiSi; Auto).

(Case H; Generalize m i H0 ; Elim ms; Clear  H H0 m i ms; Intros).
(Rewrite -> Rhobar6; Rewrite -> Rhobar5; Rewrite -> phibar_eq2;
 Rewrite -> phibar_eq1).
(Rewrite -> MSVMV1; Rewrite -> nateqb_is_eq1; 
 Auto; Unfold Setifb).
(Rewrite -> MSVMV3; Rewrite <- Lifts_PhiBar_Bridge; Rewrite -> LIFTSM4;
 Auto; Rewrite -> H0; Auto).
(Rewrite -> HTM4; Rewrite -> max_nat0; Apply ltiSi; Auto).

(Clear  H; Rewrite -> Rhobar6; Rewrite -> phibar_eq2; Rewrite -> H1;
 Auto).
(Rewrite -> Lifts_Ms_rec1; Rewrite -> MSVMV1;
 Rewrite -> nateqb_is_eq1; Auto; Unfold Setifb).
Rewrite -> NOI_Mssub_Bridge.
(Rewrite -> Drop_Lift_Ms; Auto).
(Rewrite <- Lifts_PhiBar_Bridge; Rewrite -> H0; Auto).
(Rewrite -> HTM4; Apply lt_max_nat1; Auto).

(Apply NOI_Lift_Ms; Auto).

(Rewrite -> HTM4; Rewrite -> sym_max_nat; Apply lt_max_nat1; Auto).
Save.

Lemma phibarrhobar :
	(m:M)(phibar (rhobar m))=m.

Cut ((m:M)(phibarrhobar1 m))/\
	 ((ms:Ms)(phibarrhobar2 ms)).
Intros c; Case c; Auto.
Exact Phibarrhobar.
Save.

Lemma phibarrhobar_ms :
	(i:nat)(m:M)(ms:Ms)
	 (phibar (rhobar1 i (mcons m ms)))=
	    (sc O (lifts_Ms i O (mcons m ms))).

Cut (and (m:M)(phibarrhobar1 m) (ms:Ms)(phibarrhobar2 ms)).
(Intros c; Case c; Unfold phibarrhobar2 ; Intros).
Apply H0.
Intros.
Apply phibarrhobar.

Exact Phibarrhobar.
Save.

Lemma phirho : (n:N)(phi (rho n))=n.

(Intros; Unfold rho; Rewrite <- (thetapsi (phi (rhobar (psi n))));
 Rewrite -> psiphiphibar; Rewrite -> phibarrhobar;
 Rewrite -> thetapsi; Auto).
Save.