Require MinMJ_Exchange2.
Require MinMJ_Exchange3.
Require MinMJ_L_Admis_RhoBar.

Lemma Exchange_Lift_V :
	(v,x,y:V)
	 (x=y)->
	  (V_Exchange x (lift_V y v))=
	   (lift_V (S y) v).

Intros.
(Rewrite -> H; Clear  H x; Unfold lift_V).
(Cut (nat_compare2 v (S y));
 [ Destruct 1; [ Intro | Destruct 1; Intro ] | Auto ]).
(Cut (nat_compare v y); [ Destruct 1; Intro | Auto ]).
Rewrite -> ltb_is_lt3.
(Rewrite -> ltb_is_lt1; Auto; Unfold Setifb; Unfold V_Exchange).
Rewrite -> nateqb_is_eq3.
(Rewrite -> nateqb_is_eq1; Auto).

(Apply lt_not_eq1; Apply ltiSi; Auto).

(Apply notltii; Auto).

(Repeat Rewrite -> ltb_is_lt1; Unfold Setifb).
(Unfold V_Exchange; Repeat Rewrite -> nateqb_is_eq3; Auto).
(Apply sym_not_equal; Apply lt_not_eq1; Auto).

Auto.

(Apply ltS_neq_lt; Auto).

(Rewrite -> H1; Clear  H H0 H1 v).
(Repeat Rewrite -> ltb_is_lt3; Unfold Setifb; Unfold V_Exchange).
(Repeat Rewrite -> nateqb_is_eq3; Auto).

(Apply notltii; Auto).

(Apply ltnotlt; Apply ltiSi; Auto).

(Repeat Rewrite -> ltb_is_lt3; Unfold Setifb; Unfold V_Exchange).
(Repeat Rewrite -> nateqb_is_eq3; Auto).
(Apply lt_not_eq1; Apply ltS; Auto).

(Apply lt_not_eq1; Apply ltS; Apply Slt; Auto).

(Apply ltnotlt; Auto).

(Apply ltnotlt; Apply Slt; Auto).
Save.

Definition exchange_lift_m : M->Prop :=
	[m:M](x,y:V)
	 x=y->
	  (M_Exchange x (lift_M y m))=
	   (lift_M (S y) m).

Definition exchange_lift_ms : Ms->Prop :=
	[ms:Ms](x,y:V)
	 x=y->
	  (Ms_Exchange x (lift_Ms y ms))=
	   (lift_Ms (S y) ms).

Lemma Exchange_lift_m :
	((m:M)(exchange_lift_m m))/\
	 ((ms:Ms)(exchange_lift_ms ms)).

(Apply M_Ms_ind; Unfold exchange_lift_m; Unfold exchange_lift_ms;
 Intros; Auto).
(Rewrite -> LIFTM1; Rewrite -> MExch1; Rewrite -> H; Auto;
 Rewrite -> Exchange_Lift_V; Auto).

(Rewrite -> LIFTM2; Rewrite -> MExch2; Rewrite -> H; Auto).

(Rewrite -> LIFTM4; Rewrite -> MExch4; Rewrite -> H; Auto;
 Rewrite -> H0; Auto).
Save.

Lemma Exchange_Lift_M :
	(x,y:V)(m:M)
	 x=y->
	  (M_Exchange x (lift_M y m))=
	   (lift_M (S y) m).

Cut ((m:M)(exchange_lift_m m))/\
	 ((ms:Ms)(exchange_lift_ms ms)).
Intros c; Case c; Unfold exchange_lift_m; Auto.
Exact Exchange_lift_m.
Save.

Lemma Exchange_Lift_Ms :
	(x,y:V)(ms:Ms)
	 x=y->
	  (Ms_Exchange x (lift_Ms y ms))=
	   (lift_Ms (S y) ms).

Cut ((m:M)(exchange_lift_m m))/\
	 ((ms:Ms)(exchange_lift_ms ms)).
Intros c; Case c; Unfold exchange_lift_ms; Auto.
Exact Exchange_lift_m.
Save.

Lemma Lift_Exchange_V1 :
	(v,x,y:V)
	 (lt x (S y))->
	  (lift_V x (V_Exchange y v))=
	   (V_Exchange (S y) (lift_V x v)).

Intros.
Unfold 2 lift_V.
(Cut (nat_compare2 v x);
 [ Destruct 1; [ Intro | Destruct 1; Intro ] | Auto ]).
(Rewrite -> ltb_is_lt1; Auto; Unfold Setifb; Unfold V_Exchange).
Rewrite -> nateqb_is_eq3.
Rewrite -> nateqb_is_eq3.
Rewrite -> nateqb_is_eq3.
Simpl.
Unfold lift_V.
(Rewrite -> ltb_is_lt1; Auto).

Apply sym_not_equal.
(Apply lt_not_eq1; Apply lt_trans with j:=x; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Apply lt_trans with j:=x; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Apply lt_trans3 with j:=x; Auto).

Clear  H0 H1.
(Rewrite -> ltb_is_lt3; Auto).
(Simpl; Unfold V_Exchange).
Repeat Rewrite -> nateqb_eq4.
Cut (S x)=(S y)\/(lt (S x) (S y)).
(Intros c; Case c; Clear  c; Intros).
(Injection H0; Clear  H0; Intros).
(Rewrite -> H2; Rewrite -> nateqb_is_eq1; Auto).
(Unfold Setifb; Unfold lift_V).
(Rewrite -> ltb_is_lt3; Auto).

Inversion_clear H0.
(Rewrite -> H2; Rewrite -> nateqb_is_eq3).
(Rewrite -> nateqb_is_eq3; Unfold Setifb; Unfold lift_V).
(Rewrite -> ltb_is_lt3; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Auto).

Auto.

Clear  H0 H1.
(Rewrite -> ltb_is_lt3; Auto).
(Unfold Setifb; Unfold V_Exchange).
(Rewrite -> nateqb_eq4; Rewrite -> nateqb_eq4).
(Cut (nat_compare y v); [ Destruct 1; Intro | Auto ]).
(Rewrite -> nateqb_is_eq1; Auto; Unfold Setifb; Unfold lift_V).
(Rewrite -> ltb_is_lt3; Auto).

(Rewrite -> nateqb_is_eq3; Auto; Cut (nat_compare (S y) v);
 [ Destruct 1; Intro | Auto ]).
(Rewrite -> nateqb_is_eq1; Auto; Unfold Setifb; Unfold lift_V).
(Rewrite -> ltb_is_lt3; Auto).
(Apply ltS_not_lt; Auto).

(Rewrite -> nateqb_is_eq3; Auto; Unfold Setifb; Unfold lift_V).
(Rewrite -> ltb_is_lt3; Auto).
Save.

Definition lift_exchange_m1 : M->Prop :=
	[m:M](x,y:nat)
	 (lt x (S y))->
	  (lift_M x (M_Exchange y m))=
	   (M_Exchange (S y) (lift_M x m)).

Definition lift_exchange_ms1 : Ms->Prop :=
	[ms:Ms](x,y:nat)
	 (lt x (S y))->
	  (lift_Ms x (Ms_Exchange y ms))=
	   (Ms_Exchange (S y) (lift_Ms x ms)).

Lemma lift_exchange_M1 :
	((m:M)(lift_exchange_m1 m))/\
	 ((ms:Ms)(lift_exchange_ms1 ms)).

(Apply M_Ms_ind; Unfold lift_exchange_m1; Unfold lift_exchange_ms1;
 Auto; Intros).
(Rewrite -> LIFTM1; Rewrite -> MExch1; Rewrite -> MExch1;
 Rewrite -> LIFTM1).
(Rewrite -> H; Auto).
(Rewrite -> Lift_Exchange_V1; Auto).

(Rewrite -> MExch2; Rewrite -> LIFTM2; Rewrite -> H; Auto).

(Rewrite -> MExch4; Rewrite -> LIFTM4; Rewrite -> H; Auto;
 Rewrite -> H0; Auto).
Save.

Lemma Lift_Exchange_M1 :
	(m:M)(x,y:nat)
	 (lt x (S y))->
	  (lift_M x (M_Exchange y m))=
	   (M_Exchange (S y) (lift_M x m)).

Cut 	((m:M)(lift_exchange_m1 m))/\
	 ((ms:Ms)(lift_exchange_ms1 ms)).
Intros c; Case c; Auto.
Exact lift_exchange_M1.
Save.

Lemma Lift_Exchange_Ms1 :
	(ms:Ms)(x,y:nat)
	 (lt x (S y))->
	  (lift_Ms x (Ms_Exchange y ms))=
	   (Ms_Exchange (S y) (lift_Ms x ms)).

Cut 	((m:M)(lift_exchange_m1 m))/\
	 ((ms:Ms)(lift_exchange_ms1 ms)).
Intros c; Case c; Auto.
Exact lift_exchange_M1.
Save.

Definition exchange_rhobar_bridge : M->Prop :=
	[m:M](x:V)
	 (L_Exchange x (rhobar m))=
	  (rhobar (M_Exchange x m)).

Definition exchange_rhobar1_bridge : Ms->Prop :=
	[ms:Ms](x,y:V)
	 (L_Exchange x (rhobar (sc y ms)))=
	  (rhobar (M_Exchange x (sc y ms))).

Lemma Exchange_rhobar_bridge :
	((m:M)(exchange_rhobar_bridge m))/\
	 ((ms:Ms)(exchange_rhobar1_bridge ms)).

Apply M_Ms_Height_ind.
(Destruct m; Clear  m).
(Intros x ms; Generalize x ; Clear  x; Case ms;
 Unfold exchange_rhobar_bridge; Unfold exchange_rhobar1_bridge; 
 Intros; Auto).
Rewrite -> RhoBar2.
Rewrite -> L_Exchange_eq2.
Rewrite -> MExch1.
Rewrite -> MExch4.
Rewrite -> RhoBar2.
(Case H; Clear  H; Intros).
(Rewrite -> H0; Auto).
(Rewrite -> H; Auto).
Rewrite -> MExch1.
Unfold 2 V_Exchange.
(Rewrite -> nateqb_is_eq3; Auto; Rewrite -> nateqb_is_eq3; Auto;
 Unfold Setifb).
(Rewrite -> Lift_Exchange_Ms1; Auto).

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

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

(Unfold exchange_rhobar_bridge; Intros).
(Case H; Clear  H; Intros).
Rewrite -> RhoBar3.
(Rewrite -> L_Exchange_eq3; Rewrite -> H; Auto).
(Rewrite -> HTM2; Apply ltiSi; Auto).

(Destruct ms; Unfold exchange_rhobar_bridge;
 Unfold exchange_rhobar1_bridge; Intros; Auto).
(Rewrite -> RhoBar2; Rewrite -> L_Exchange_eq2; Case H; Clear  H;
 Intros).
(Rewrite -> H; Auto).
Rewrite -> MExch1.
(Rewrite -> MExch1; Rewrite -> MExch4).
Rewrite -> RhoBar2.
(Rewrite -> H0; Auto).
(Rewrite -> Lift_Exchange_Ms1; Auto).

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

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

Lemma Exchange_RhoBar_Bridge :
	(x:nat)(m:M)
	 (L_Exchange x (rhobar m))=
	  (rhobar (M_Exchange x m)).

Cut 	((m:M)(exchange_rhobar_bridge m))/\
	 ((ms:Ms)(exchange_rhobar1_bridge ms)).
Intros c; Case c; Unfold exchange_rhobar_bridge; Auto.
Exact Exchange_rhobar_bridge.
Save.

Definition height_m_exchange : M->Prop :=
	[m:M](x:nat)
	 (Height_M (M_Exchange x m))=
	  (Height_M m).

Definition height_ms_exchange : Ms->Prop :=
	[ms:Ms](x:nat)
	 (Height_Ms (Ms_Exchange x ms))=
	  (Height_Ms ms).

Lemma Height_m_exchange :
	((m:M)(height_m_exchange m))/\
	 ((ms:Ms)(height_ms_exchange ms)).

(Apply M_Ms_ind; Unfold height_m_exchange; Unfold height_ms_exchange;
 Intros; Auto).
(Rewrite -> MExch1; Rewrite -> HTM1; Rewrite -> H; Auto).

(Rewrite -> MExch2; Rewrite -> HTM2; Rewrite -> H; Auto).

(Rewrite -> MExch4; Rewrite -> HTM4; Rewrite -> H; Rewrite -> H0;
 Auto).
Save.

Lemma Height_M_Exchange :
	(m:M)(x:nat)
	 (Height_M (M_Exchange x m))=
	  (Height_M m).

Cut ((m:M)(height_m_exchange m))/\
	 ((ms:Ms)(height_ms_exchange ms)).
Intros c; Case c; Unfold height_m_exchange; Auto.
Exact Height_m_exchange.
Save.

Lemma Height_Ms_Exchange :
	(ms:Ms)(x:nat)
	 (Height_Ms (Ms_Exchange x ms))=
	  (Height_Ms ms).

Cut ((m:M)(height_m_exchange m))/\
	 ((ms:Ms)(height_ms_exchange ms)).
Intros c; Case c; Unfold height_ms_exchange; Auto.
Exact Height_m_exchange.
Save.

Definition msub_exch_bridge1 : M->Prop :=
	[m:M](x,y:V)(m1:M)
	 (MsubstVMV x m1 y (M_Exchange y m))=
	  (MsubstVMV x m1 (S y) m).

Definition mssub_exch_bridge1 : Ms->Prop :=
	[ms:Ms](x,y:V)(m1:M)
	 (MssubstVMV x m1 y (Ms_Exchange y ms))=
	  (MssubstVMV x m1 (S y) ms).

Lemma Msub_exch_bridge1 :
	((m:M)(msub_exch_bridge1 m))/\
	 ((ms:Ms)(mssub_exch_bridge1 ms)).

(Apply M_Ms_ind; Unfold msub_exch_bridge1; Unfold mssub_exch_bridge1;
 Intros; Auto).
(Rewrite -> MExch1; Rewrite -> MSVMV1).
Rewrite -> MSVMV1.
Unfold V_Exchange.
(Cut (nat_compare2 y v);
 [ Destruct 1; [ Intro | Destruct 1; Intro ] | Auto ]).
Rewrite -> (nateqb_is_eq3 y v).
Unfold 2 4 6 Setifb.
(Cut (nat_compare (S y) v); [ Destruct 1; Intro | Auto ]).
(Rewrite -> (nateqb_is_eq1 (S y) v); Auto).
Unfold 2 3 4 5 Setifb.
(Rewrite -> nateqb_is_eq1; Auto).
Unfold Setifb.
(Rewrite <- H3; Rewrite -> H; Auto).

(Rewrite -> (nateqb_is_eq3 (S y) v); Auto).
Unfold 2 3 4 5 Setifb.
(Rewrite -> nateqb_is_eq3; Auto).
Unfold Setifb.
(Rewrite -> H; Auto).
Unfold drop_V.
Rewrite -> ltb_is_lt3.
(Rewrite -> ltb_is_lt3; Auto).
(Apply lt_not_ltS; Auto).

(Apply ltnotlt; Auto).

(Apply lt_not_eq1; Auto).

(Apply lt_not_eq1; Auto).

(Clear  H0 H1; Rewrite -> (nateqb_is_eq1 y v H2)).
Unfold 2 4 6 Setifb.
Rewrite -> (nateqb_is_eq3 y (S y)).
Unfold drop_V.
Unfold 1 Setifb.
Rewrite -> ltb_is_lt3.
Unfold 1 Setifb.
Unfold 1 pred.
Rewrite -> nateqb_is_eq3.
Unfold 1 Setifb.
Rewrite -> ltb_is_lt1.
Unfold Setifb.
(Rewrite -> H; Rewrite -> H2; Auto).

(Apply ltiSi; Auto).

(Rewrite -> H2; Apply sym_not_equal; Apply n_Sn).

(Apply ltnotlt; Apply ltiSi; Auto).

(Apply n_Sn; Auto).

Clear  H1 H0.
Rewrite -> (nateqb_is_eq3 y v).
Unfold 2 4 6 Setifb.
Rewrite -> (nateqb_is_eq3 (S y) v).
Unfold 2 3 4 5 Setifb.
Rewrite -> nateqb_is_eq3.
Unfold Setifb.
(Rewrite -> H; Auto).
Unfold drop_V.
(Rewrite -> ltb_is_lt1; Auto).
(Rewrite -> ltb_is_lt1; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Auto).

(Apply sym_not_equal; Apply lt_not_eq1; Auto).

(Simpl; Rewrite -> H; Auto).

(Rewrite -> MExch4; Repeat Rewrite -> MSVMV4; Rewrite -> H;
 Rewrite -> H0; Auto).
Save.

Lemma Msub_Exch_Bridge1 :
	 (m:M)(x,y:V)(m1:M)
	 (MsubstVMV x m1 y (M_Exchange y m))=
	  (MsubstVMV x m1 (S y) m).

Cut ((m:M)(msub_exch_bridge1 m))/\
	 ((ms:Ms)(mssub_exch_bridge1 ms)).
Intros c; Case c; Unfold msub_exch_bridge1; Auto.
Exact Msub_exch_bridge1.
Save.

Lemma Mssub_Exch_Bridge1 :
	(ms:Ms)(x,y:V)(m1:M)
	 (MssubstVMV x m1 y (Ms_Exchange y ms))=
	  (MssubstVMV x m1 (S y) ms).

Cut ((m:M)(msub_exch_bridge1 m))/\
	 ((ms:Ms)(mssub_exch_bridge1 ms)).
Intros c; Case c; Unfold mssub_exch_bridge1; Auto.
Exact Msub_exch_bridge1.
Save.