Require MinMJ_rhobar.
Require MinMJ_Bridge2.

Definition lift_rhobar_bridge : M->Prop :=
	[m:M](i:nat)
	 (lift_L i (rhobar m))=
	  (rhobar (lift_M i m)).

Definition lift_rhobar1_bridge : Ms->Prop :=
	[ms:Ms](i,j:nat)(m:M)
	 (lt O i)->
	  ((m1:M)(k:nat)
	    (lt (Height_M m1) (Height_Ms (mcons m ms)))->
	     (lift_L k (rhobar m1))=
	      (rhobar (lift_M k m1)))->
	   (rhobar1 i (lift_Ms j (mcons m ms)))=
	    (lift_L (plus i j) (rhobar1 i (mcons m ms))).

Lemma lift_rhobar_Bridge :
	((m:M)(lift_rhobar_bridge m))/\
	 ((ms:Ms)(lift_rhobar1_bridge ms)).

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

(Intros m ms H; Generalize m ; Elim ms; Clear  H m ms;
 Unfold lift_rhobar_bridge; Unfold lift_rhobar1_bridge; Intros).
(Rewrite -> Rhobar2; Rewrite -> lift_L_eq2).
(Case H; Clear  H; Intros).
(Rewrite -> H; Auto).
(Rewrite -> HTM1; Rewrite -> HTM4; Rewrite -> HTM3;
 Rewrite -> max_nat0; Apply ltS; Apply ltiSi; Auto).

(Rewrite -> Rhobar3; Rewrite -> lift_L_eq2; Case H0; Clear  H H0;
 Intros).
(Pattern 3 i ; Rewrite <- (plus_right_id i); Rewrite -> sym_plus;
 Rewrite <- plus_eq2).
(Rewrite <- H0; Auto).
(Rewrite -> LIFTM1; Rewrite -> LIFTM4).
Rewrite -> LIFTM4.
Rewrite -> Rhobar3.
(Rewrite -> H; Auto).
(Rewrite -> HTM1; Apply ltS; Rewrite -> HTM4; Apply lt_max_nat1; Auto).

(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 H.
(Rewrite -> HTM1; Apply ltS; Rewrite -> HTM4; Apply ltS;
 Rewrite -> sym_max_nat; Apply lt_max_nat2; Auto).

(Unfold lift_rhobar_bridge; Intros).
(Case H0; Clear  H H0; Intros).
(Rewrite -> Rhobar4; Rewrite -> lift_L_eq3; Rewrite -> H; Auto).
(Rewrite -> HTM2; Apply ltiSi; Auto).

(Induction ms; Clear  ms).
(Unfold lift_rhobar_bridge; Unfold lift_rhobar1_bridge; Intros).
(Rewrite -> LIFTM4; Rewrite -> LIFTM3; Rewrite -> Rhobar6;
 Rewrite -> Rhobar5).
(Case H; Clear  H; Intros).
(Rewrite <- H1; Auto).
(Rewrite -> Rhobar6; Rewrite -> Rhobar5).
(Rewrite -> lift_L_eq2; Rewrite -> lift_L_eq1).
Unfold lift_V.
Rewrite -> ltb_is_lt1.
(Rewrite -> ltb_is_lt1; Auto).
Unfold Setifb.
Rewrite -> Lifts_Lift_L_Bridge3.
Auto.

(Unfold not; Intros c; Inversion c).

(Inversion_clear H0; Simpl; Auto).

(Rewrite -> HTM4; Rewrite -> HTM3; Rewrite -> max_nat0; Apply ltiSi;
 Auto).

(Unfold lift_rhobar_bridge; Unfold lift_rhobar1_bridge; Intros).
(Case H0; Clear  H H0; Intros).
Clear  H0.
(Rewrite -> LIFTM4; Rewrite -> Rhobar6).
(Rewrite <- H2; Auto).
Rewrite -> Lifts_Lift_L_Bridge3.
(Rewrite -> H; Auto).
Rewrite -> plus_eq2.
Rewrite -> (Rhobar6 m1).
Rewrite -> lift_L_eq2.
Unfold lift_V.
(Rewrite -> ltb_is_lt1; Unfold Setifb).
Auto.

(Inversion_clear H1; Simpl; Auto).

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

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

(Unfold not; Intros c; Inversion c).

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

Lemma Lift_RhoBar_Bridge :
	(m:M)(i:nat)
	 (lift_L i (rhobar m))=
	  (rhobar (lift_M i m)).

Cut ((m:M)(lift_rhobar_bridge m))/\
	 ((ms:Ms)(lift_rhobar1_bridge ms)).
Intros c; Case c; Auto.
Exact lift_rhobar_Bridge.
Save.

Lemma Lift_RhoBar1_Bridge :
	(ms:Ms)(i,j:nat)(m:M)
	 (lt O i)->
	  (rhobar1 i (lift_Ms j (mcons m ms)))=
	    (lift_L (plus i j) (rhobar1 i (mcons m ms))).

Cut (and (m:M)(lift_rhobar_bridge m) (ms:Ms)(lift_rhobar1_bridge ms)).
(Intros c; Case c; Clear  c; Unfold lift_rhobar_bridge ;
 Unfold lift_rhobar1_bridge ; Intros).
(Rewrite -> H0; Auto).

Exact lift_rhobar_Bridge.
Save.

Lemma Lifts_RhoBar_Bridge :
	(i,j:nat)(m:M)
	 (lifts_L i j (rhobar m))=
	  (rhobar (lifts_M i j m)).

(Induction i; Clear  i; Intros).
(Rewrite -> Lifts_L0; Rewrite -> Lifts_M0; Auto).

(Rewrite -> Lifts_L_rec1; Rewrite -> Lifts_M_rec1; Rewrite -> H;
 Rewrite -> Lift_RhoBar_Bridge; Auto).
Save.

Lemma Lift_RhoBar1_Bridge1 :
	(ms:Ms)(i,j:nat)
	 (lt O i)->
	  (rhobar1 i (lift_Ms j ms))=
	    (lift_L (plus i j) (rhobar1 i ms)).

(Induction ms; Clear  ms; Intros).
(Rewrite -> LIFTM3; Rewrite -> Rhobar5; Rewrite -> lift_L_eq1; Unfold lift_V).
(Rewrite -> ltb_is_lt1; Auto).
(Inversion_clear H; Simpl; Auto).

(Rewrite -> LIFTM4; Rewrite -> Rhobar6; Rewrite -> Rhobar6;
 Rewrite -> lift_L_eq2; Unfold lift_V).
Rewrite -> ltb_is_lt1.
(Unfold Setifb ; Rewrite <- Lift_RhoBar_Bridge;
 Rewrite -> Lifts_Lift_L_Bridge3).
(Rewrite <- plus_eq2; Rewrite <- H; Auto).

(Unfold not ; Intros c; Inversion c).

(Inversion_clear H0; Simpl; Auto).
Save.

Lemma RhoBar1_Lifts_Ms1 :
	(ms:Ms)(i,j:nat)
	 (rhobar1 j (lifts_Ms (S i) O ms))=
	  (rhobar1 (S j) (lifts_Ms i O ms)).

(Induction ms; Clear  ms; Intros; Auto).
(Rewrite -> LIFTSM4; Rewrite -> Rhobar6;
 Rewrite <- Lifts_RhoBar_Bridge; Rewrite -> Lifts_Lifts_L_Bridge0;
 Auto; Rewrite -> LIFTSM4; Rewrite -> Rhobar6;
 Rewrite <- Lifts_RhoBar_Bridge; Rewrite -> Lifts_Lifts_L_Bridge0; 
 Auto; Rewrite -> sym_plus; Rewrite -> plus_eq2; Rewrite -> sym_plus;
 Rewrite -> plus_eq2; Rewrite -> H; Auto).
Save.

Lemma RhoBar1_Lifts_Ms :
	(i,j:nat)(ms:Ms)
	 (rhobar1 j (lifts_Ms i O ms))=
	  (rhobar1 (plus j i) ms).

(Induction i; Clear  i; Intros).
(Rewrite -> Lifts_Ms0; Rewrite -> plus_right_id; Auto).

(Rewrite -> RhoBar1_Lifts_Ms1; Rewrite -> H; Rewrite -> plus_eq2;
 Rewrite -> sym_plus; Rewrite <- plus_eq2; Rewrite -> sym_plus; Auto).
Save.

Definition rhobar21 : M->Prop :=
	[m:M](x:V)(ms:Ms)
	 ((ms1:Ms)(i:nat)
	   (lt (Height_Ms ms1) (Height_Ms (mcons m ms)))->
	    (rhobar1 (S i) ms1)=
	     (rhobar (sc O (lifts_Ms (S i) O ms1))))->
	  (rhobar (sc x (mcons m ms)))=
	   (app x (rhobar m) (rhobar (sc O (lift_Ms O ms)))).

Definition rhobar22 : Ms->Prop :=
	[ms:Ms](i:nat)
	 (rhobar1 (S i) ms)=
	  (rhobar (sc O (lifts_Ms (S i) O ms))).

Lemma Rhobar21 :
	((m:M)(rhobar21 m))/\
	 ((ms:Ms)(rhobar22 ms)).

Apply M_Ms_Height_ind.
(Induction m; Clear  m).
(Intros x ms; Generalize x ; Elim ms; Clear  x ms).
(Unfold rhobar21; Unfold rhobar22; Intros).
(Case H; Clear  H; Intros).
Clear  H1.
Rewrite -> Rhobar3.
Rewrite -> Rhobar1.
(Rewrite -> H0; Auto).
(Rewrite -> Lifts_Ms_rec1; Rewrite -> Lifts_Ms0; Auto).

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

(Unfold rhobar21; Unfold rhobar22; Intros).
(Case H0; Clear  H H0; Intros).
(Rewrite -> Rhobar3; Rewrite -> Rhobar3).
(Rewrite -> H1; Auto).
(Rewrite -> Lifts_Ms_rec1; Rewrite -> Lifts_Ms0; Auto).
(Rewrite -> H1; Auto).
(Rewrite -> Lifts_Ms_rec1; Rewrite -> Lifts_Ms0; Auto).

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

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

(Unfold rhobar21; Unfold rhobar22; Intros).
Rewrite -> Rhobar3.
Rewrite -> Rhobar4.
(Case H0; Clear  H H0; Intros).
(Rewrite -> H1; Auto).
(Rewrite -> Lifts_Ms_rec1; Rewrite -> Lifts_Ms0; Auto).

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

(Induction ms; Clear  ms).
(Unfold rhobar22; Auto).

(Intros m ms; Generalize m ; Elim ms; Clear  m ms; Unfold rhobar21;
 Unfold rhobar22; Intros).
(Case H0; Clear  H H0; Intros).
(Rewrite -> Rhobar6; Rewrite -> Rhobar5).
(Rewrite -> LIFTSM4; Rewrite -> LIFTSM3; Rewrite -> Rhobar2).
Rewrite -> Lifts_RhoBar_Bridge.
Auto.

(Case H1; Clear  H0 H1; Intros; Clear  H).
(Rewrite -> Rhobar6; Rewrite -> LIFTSM4; Rewrite -> Rhobar3).
Rewrite -> Lifts_RhoBar_Bridge.
(Rewrite -> H0; Auto).
(Rewrite -> LIFTSM4; Rewrite -> LIFTSM4; Rewrite -> Rhobar6;
 Rewrite -> Rhobar3; Rewrite -> Lifts_RhoBar_Bridge).
(Rewrite -> (Lifts_M_rec1 m);
 Rewrite -> (Lifts_M_rec1 (lifts_M (S i) O m)); Rewrite -> Lifts_M0).
(Rewrite -> RhoBar1_Lifts_Ms; Rewrite -> RhoBar1_Lifts_Ms; Auto).

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

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

Auto.
Save.

Lemma RhoBar2 : (ms:Ms)(x:V)(m:M)
	(rhobar (sc x (mcons m ms)))=
	 (app x (rhobar m) (rhobar (sc O (lift_Ms O ms)))).

Cut ((m:M)(rhobar21 m))/\
	 ((ms:Ms)(rhobar22 ms)).
Intros c; Case c; Clear c; Unfold rhobar21; Unfold rhobar22; Intros.
Rewrite H; Auto.
Exact Rhobar21.
Save.

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

Auto.
Save.

Definition l_admis_rhobar_m : M->Prop :=
	[m:M](h:Hyps)(P:F)
	 (M_Deriv h m P)->
	  (L_Deriv h (rhobar m) P).

Definition l_admis_rhobar_ms : Ms->Prop :=
	[ms:Ms](h:Hyps)(P,Q:F)
	 ((m1:M)(h1:Hyps)(P1:F)
	   (lt (Height_M m1) (Height_Ms ms))->
	    (M_Deriv h1 m1 P1)->
	     (L_Deriv h1 (rhobar m1) P1))->
	  (Ms_Deriv (Add_Hyp Q h) Q ms P)->
	   (L_Deriv (Add_Hyp Q h) (rhobar (sc O ms)) P).

Lemma L_Admis_RhoBar1 :
	((m:M)(l_admis_rhobar_m m))/\
	 ((ms:Ms)(l_admis_rhobar_ms ms)).

Apply M_Ms_Height_ind.
(Induction m; Clear  m).
(Intros x ms; Generalize x ; Elim ms; Clear  x ms; Unfold l_admis_rhobar_m;
 Unfold l_admis_rhobar_ms; Intros).
Rewrite -> RhoBar1.
Inversion_clear H0.
(Generalize H1 ; Clear  H; Inversion_clear H2; Intros; Apply L_Axiom;
 Auto).

Rewrite -> RhoBar2.
(Case H0; Clear  H H0; Intros).
(Generalize H H0 ; Clear  H H0; Inversion_clear H1).
(Generalize H ; Clear  H; Inversion_clear H0; Intros).
(Apply Implies_L with P:=P1 Q:=Q; Auto).
(Apply H2; Auto).
(Rewrite -> HTM1; Rewrite -> HTM4; Apply ltS; Apply lt_max_nat1;
 Auto).

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

Intros.
(Apply H2; Auto).
(Generalize H4 ; Clear  H4; Rewrite -> Height_Lift_Ms; Intros).
(Rewrite -> HTM1; Rewrite -> HTM4).
(Apply ltS; Apply ltS; Rewrite -> sym_max_nat; Apply lt_max_nat2; Auto).

(Apply Ms_Admis_Weaken_Top; Auto).

(Unfold l_admis_rhobar_m; Unfold l_admis_rhobar_ms; Intros).
Simpl.
(Case H0; Clear  H H0; Inversion_clear H1; Intros).
(Apply Implies_R; Apply H0; Auto).
Simpl.
(Apply ltiSi; Auto).

(Induction ms; Clear  ms; Unfold l_admis_rhobar_m; Unfold l_admis_rhobar_ms; Intros).
Clear  H.
Simpl.
(Inversion_clear H1; Apply L_Axiom; Auto).

Rewrite -> RhoBar2.
(Case H0; Clear  H H0; Inversion_clear H2; Intros).
(Apply Implies_L with P:=P0 Q:=Q0; Auto).
(Apply H1; Auto).
Rewrite -> HTM4.
(Apply lt_max_nat1; Auto).

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

Intros.
(Apply H3; Auto).
(Generalize H4 ; Clear  H4; Rewrite -> Height_Lift_Ms; Intros;
 Rewrite -> HTM4; Apply ltS; Rewrite -> sym_max_nat;
 Apply lt_max_nat2; Auto).

(Apply Ms_Admis_Weaken_Top; Auto).
Save.

Lemma L_Admis_RhoBar : (h:Hyps)(m:M)(P:F)
	(M_Deriv h m P)->
	 (L_Deriv h (rhobar m) P).

Cut (and (m:M)(l_admis_rhobar_m m) (ms:Ms)(l_admis_rhobar_ms ms)).
(Intros c; Case c; Unfold l_admis_rhobar_m; Auto).

Exact L_Admis_RhoBar1.
Save.

Lemma L_Admis_Rho : (h:Hyps)(n:N)(P:F)
	(N_Deduc h n P)->
	 (L_Deriv h (rho n) P).

(Intros; Unfold rho ; Apply L_Admis_RhoBar; Apply M_Admis_Psi; Auto).
Save.