Require MinMJ_Exchange.

Lemma Hyps_ref_eq :
	(i,j:V)(P,Q:F)(h:Hyps)
	 i=j->
	  (In_Hyps i P h)->
	   (In_Hyps j Q h)->
	    P=Q.

(Induction i; Clear  i; Intros).
(Generalize H1 ; Clear  H1; Rewrite <- H; Clear  H j;
 Inversion_clear H0; Intros).
(Inversion_clear H1; Auto).

(Generalize H2 ; Clear  H2; Rewrite <- H0; Clear  H0 j;
 Inversion_clear H1; Intros).
Inversion_clear H2.
(Apply (H n P Q h0); Auto).
Save.

Lemma V_Exch_S_Bridge :
	(i,j:nat)
	 (V_Exchange (S i) (S j))=
	  (S (V_Exchange i j)).

(Intros; Unfold V_Exchange ).
(Rewrite -> nateqb_eq4; Rewrite -> nateqb_eq4).
(Case (nateqb i j); Auto; Case (nateqb (S i) j); Auto).
Save.

Lemma V_Exch_id :
	(i:nat)
	 (V_Exchange i i)=(S i).

(Intros; Simpl; Unfold V_Exchange ; Rewrite -> nateqb_is_eq1; Auto).
Save.

Lemma In_Exch1 :
	(h:Hyps)(i,j:nat)(P:F)
	 (lt i j)->
	  (In_Hyps i P h)->
	   (In_Hyps i P (Hyps_Exchange j h)).

(Induction h; Clear  h; Intros).
Inversion H0.

(Generalize H0 ; Clear  H0; Inversion_clear H1).
Intros.
(Generalize H ; Clear  H; Case l; Intros).
(Generalize H H0 ; Clear  H H0; Case j; Intros).
Inversion H0.

(Simpl; Auto).

(Generalize H0 ; Clear  H0; Case j; Intros).
Inversion H0.

(Rewrite -> Hyps_Exchange_eq4; Auto).

(Case j; Intros).
Inversion H1.

(Clear  j; Generalize H1 ; Clear  H1; Case n0; Intros).
(Inversion_clear H1; Inversion H2).

(Inversion_clear H1; Generalize H H0 ; Clear  H H0; Case l; Intros).
Inversion H0.

Rewrite -> Hyps_Exchange_eq4.
(Apply inhyps_rec; Apply H; Auto).
Save.

Lemma In_Exch2 :
	(h:Hyps)(i,j:nat)(P:F)
	 (lt (S j) i)->
	  (In_Hyps i P h)->
	   (In_Hyps i P (Hyps_Exchange j h)).

(Intros h; Case h; Clear  h).
Intros.
Inversion H0.

(Intros f h; Case h; Clear  h).
Intros.
(Generalize H ; Clear  H; Inversion_clear H0).
Intros.
Inversion_clear H.

Inversion H.

(Intros f0 h i j; Generalize f f0 h i ; Elim j; Clear  f f0 h i j).
(Intros f f0 h i P H; Inversion_clear H; Inversion_clear H0).
Simpl.
(Intros; Inversion_clear H; Inversion_clear H0; Auto).

Intros.
(Generalize H1 ; Case h; Clear  H1 h).
(Inversion_clear H0; Inversion_clear H1; Inversion_clear H0).
Simpl.
Intros.
(Inversion_clear H1; Inversion_clear H0; Inversion_clear H1).

Intros.
(Inversion_clear H0; Inversion_clear H2; Inversion_clear H0).

Inversion_clear H0.
Intros.
Inversion_clear H0.
(Rewrite -> Hyps_Exchange_eq4; Apply inhyps_rec).
(Apply H; Auto).
Save.

Lemma In_Exch :
	(i,j:nat)(h:Hyps)(P,Q,R:F)
	 (In_Hyps i P h)->
	  (In_Hyps j Q h)->
	   (In_Hyps (S j) R h)->
	    (In_Hyps (V_Exchange j i) P (Hyps_Exchange j h)).

(Intros i j; Unfold V_Exchange; Cut (nat_compare j i); Auto;
 Unfold nat_compare; Intros c; Case c; Clear  c; Intros H).
(Rewrite -> nateqb_is_eq1; Auto; Unfold Setifb).
(Rewrite -> H; Clear  H j; Intros h; Generalize i ; Elim h; Clear  i h).
Intros.
Inversion H.

(Intros f h H; Generalize f ; Elim h; Clear  H f h).
Intros.
(Inversion_clear H1; Inversion H2).

(Induction i; Clear  i; Intros).
Simpl.
(Inversion_clear H0; Auto).

Rewrite -> Hyps_Exchange_eq4.
Apply inhyps_rec.
(Apply (H a n P Q R); Auto).
(Inversion_clear H1; Auto).

(Inversion_clear H2; Auto).

(Inversion_clear H3; Auto).

(Rewrite -> nateqb_is_eq3; Auto; Unfold 1 Setifb;
 Cut (nat_compare (S j) i); Auto; Unfold nat_compare; Intros c; 
 Case c; Clear  c; Intros H0).
(Rewrite -> nateqb_is_eq1; Auto; Unfold Setifb).
(Rewrite <- H0; Intros h; Generalize j ; Clear  H H0 i j; Elim h;
 Clear  h).
(Intros; Inversion H).

(Intros f h H; Generalize f ; Elim h; Clear  H h f).
Intros.
(Inversion_clear H1; Inversion H2).

(Induction j; Clear  j; Intros).
Simpl.
(Inversion_clear H0; Inversion_clear H3; Auto).

Rewrite -> Hyps_Exchange_eq4.
(Inversion_clear H1; Inversion_clear H2; Inversion_clear H3;
 Apply inhyps_rec; Apply (H a n P Q R); Auto).

(Rewrite -> nateqb_is_eq3; Auto; Unfold Setifb).
(Cut (nat_compare2 i j); Auto; Unfold nat_compare2; Intros c; Case c;
 Clear  c; Intros H1).
Intros.
(Apply In_Exch1; Auto).

(Case H1; Clear  H1).
Intros.
Auto_Contra H.

Intros.
Cut (lt (S j) i).
Intros.
(Apply In_Exch2; Auto).

Clear  H2 H3 H4.
Clear  h P Q R.
Cut (S j)=i\/(lt (S j) i).
(Intros c; Case c; Clear  c; Intros).
Auto_Contra H0.

Auto.

(Apply lt_S_le; Auto).
Save.

Definition l_admis_exch1 :
	(h:Hyps)(l:L)(R:F)(L_Deriv h l R)->Prop :=
	 [h:Hyps][l:L][R:F][l0:(L_Deriv h l R)](j:nat)(P,Q:F)
	  (In_Hyps j P h)->
	   (In_Hyps (S j) Q h)->
	    (L_Deriv (Hyps_Exchange j h)
		     (L_Exchange j l)
		     R).

Lemma L_admis_exch : 
	(h:Hyps)(l:L)(R:F)(D:(L_Deriv h l R))
	 (l_admis_exch1 h l R D).

(Intros; Apply L_Deriv_ind1; Clear  D h l R; Unfold l_admis_exch1;
 Intros).
Simpl.
Apply L_Axiom.
(Apply In_Exch with Q:=P0 R:=Q; Auto).

(Simpl; Apply Implies_L with P:=P Q:=Q; Auto).
(Apply In_Exch with Q:=P0 R:=Q0; Auto).

(Apply (H j P0 Q0); Auto).

(Generalize i0 H H0 H1 H2 l l0 ; Case h; Clear  i0 H H0 H1 H2 l l0 h;
 Intros).
Inversion i0.

(Rewrite <- Hyps_Exchange_eq4; Apply H0 with P:=P0 Q0:=Q0; Auto).

(Simpl; Apply Implies_R; Auto).
(Generalize l0 H H0 H1 ; Case h; Clear  l0 H H0 H1 h; Intros).
Inversion H0.

(Rewrite <- Hyps_Exchange_eq4; Apply (H (S j) P0 Q0); Auto).
Save.

Lemma L_Admis_Exch :
	(h:Hyps)(l:L)(R:F)(j:nat)(P,Q:F)
	 (L_Deriv h l R)->
	  (In_Hyps j P h)->
	   (In_Hyps (S j) Q h)->
	    (L_Deriv (Hyps_Exchange j h)
		     (L_Exchange j l)
		     R).
	
Cut (h:Hyps)(l:L)(R:F)(D:(L_Deriv h l R))(l_admis_exch1 h l R D).
(Unfold l_admis_exch1; Intros).
Exact (H h l R H0 j P Q H1 H2).

Exact L_admis_exch.
Save.

Lemma Hyps_Exchange_Top :
	(P,Q:F)(h:Hyps)
	 (Hyps_Exchange O (Add_Hyp P (Add_Hyp Q h)))=
	  (Add_Hyp Q (Add_Hyp P h)).

Auto.
Save.

Lemma L_Admis_Exch_Top :
	(P,Q,R:F)(h:Hyps)(l:L)
	 (L_Deriv (Add_Hyp P (Add_Hyp Q h)) l R)->
	  (L_Deriv (Add_Hyp Q (Add_Hyp P h)) (L_Exchange O l) R).

Intros.
Rewrite <- Hyps_Exchange_Top.
(Apply L_Admis_Exch with P:=P Q:=Q; Auto).
Save.

Definition n_admis_exch :
	(h:Hyps)(n:N)(R:F)(N_Deduc h n R)->Prop :=
	 [h:Hyps][n:N][R:F][n0:(N_Deduc h n R)](j:nat)(P,Q:F)
	  (In_Hyps j P h)->
	   (In_Hyps (S j) Q h)->
	    (N_Deduc (Hyps_Exchange j h)
		     (N_Exchange j n)
		     R).

Definition a_admis_exch :
	(h:Hyps)(a:A)(R:F)(A_Deduc h a R)->Prop :=
	 [h:Hyps][a:A][R:F][a0:(A_Deduc h a R)](j:nat)(P,Q:F)
	  (In_Hyps j P h)->
	   (In_Hyps (S j) Q h)->
	    (A_Deduc (Hyps_Exchange j h)
		     (A_Exchange j a)
		     R).

Lemma N_admis_exch :
	((h:Hyps)(n:N)(R:F)(n0:(N_Deduc h n R))(n_admis_exch h n R n0))/\
	 ((h:Hyps)(a:A)(R:F)(a0:(A_Deduc h a R))(a_admis_exch h a R a0)).

(Apply N_A_Deduc_ind; Unfold n_admis_exch ; Unfold a_admis_exch ; Intros).
Simpl.
(Apply Implies_I; Auto).
(Generalize H H0 H1 n0 ; Case h; Clear  H H0 H1 n0 h; Intros).
Inversion H0.

Rewrite <- Hyps_Exchange_eq4.
(Apply H with P:=P Q0:=Q0; Auto).

Rewrite -> NExch2.
(Apply AN_Axiom; Auto).
(Apply (H j P Q); Auto).

(Rewrite -> NExch3; Apply Implies_E with P:=P1 Q:=Q; Auto).
(Apply (H j P Q0); Auto).

(Apply (H0 j P Q0); Auto).

(Rewrite -> NExch4; Apply A_Axiom).
(Apply In_Exch with Q:=P R:=Q; Auto).
Save.

Lemma N_Admis_Exch : (h:Hyps)(n:N)(R:F)(j:nat)(P,Q:F)
	(N_Deduc h n R)->
	 (In_Hyps j P h)->
	  (In_Hyps (S j) Q h)->
	   (N_Deduc (Hyps_Exchange j h)
		    (N_Exchange j n)
		    R).

Cut (and (h:Hyps)(n:N)(R:F)(n0:(N_Deduc h n R))(n_admis_exch h n R n0)
      (h:Hyps)(a:A)(R:F)(a0:(A_Deduc h a R))(a_admis_exch h a R a0)).
Unfold n_admis_exch .
(Intros c; Case c; Clear  c; Intros).
(Apply H with P:=P Q:=Q; Auto).

Exact N_admis_exch.
Save.

Lemma A_Admis_Exch : (h:Hyps)(a:A)(R:F)(j:nat)(P,Q:F)
	(A_Deduc h a R)->
	 (In_Hyps j P h)->
	  (In_Hyps (S j) Q h)->
	   (A_Deduc (Hyps_Exchange j h)
		    (A_Exchange j a)
		    R).

Cut ((h:Hyps)(n:N)(R:F)(n0:(N_Deduc h n R))(n_admis_exch h n R n0))/\
	 ((h:Hyps)(a:A)(R:F)(a0:(A_Deduc h a R))(a_admis_exch h a R a0)).
Unfold a_admis_exch.
Intros c; Case c; Clear c; Intros; Apply H0 with P:=P Q:=Q; Auto.
Exact N_admis_exch.
Save.