Require MinMJ_LJ.
Require MinMJ_MJ.
Require MinMJ_NJ.
Require MinMJ_Occurs_Lift.

Recursive Definition
    Strengthen_Hyps : nat->Hyps->Hyps :=
	n MT => MT |
	O (Add_Hyp Q h) => h |
	(S i) (Add_Hyp Q h) => (Add_Hyp Q (Strengthen_Hyps i h)).

Lemma Drop_S_Bridge_nat :
	(i,j:nat)
	 ~i=j->
	  (drop_V (S i) (S j))=
	   (S (drop_V i j)).

(Intros i j; Unfold drop_V ; Simpl).
(Elim j; Clear  j; Intros).
(Rewrite -> ltb_is_lt1; Auto).
(Generalize H ; Clear  H; Elim i; Auto).
Intros.
Cut False.
Contradiction.

(Apply H; Auto).

(Case (ltb (S n) i); Auto).
Save.

Lemma In_Strength :
	(h:Hyps)(i,j:nat)(P:F)
	 (In_Hyps i P h)->
	  ~i=j->
	   (In_Hyps (drop_V j i) P (Strengthen_Hyps j h)).

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

(Generalize H H1 ; Clear  H H1; Inversion_clear H0; Intros).
(Unfold drop_V; Generalize H1 ; Clear  H1; Elim j; Clear  j; Intros).
(Cut False; Intros).
Contradiction.

(Apply H1; Auto).

(Rewrite -> ltb_is_lt1; Auto; Unfold Setifb ; Simpl; Auto).

(Generalize H1 ; Clear  H1; Elim j; Clear  j; Intros).
Clear  H1.
Simpl.
Unfold drop_V .
Rewrite -> ltb_is_lt3.
Auto.

(Unfold not ; Intros c; Inversion c).

(Simpl; Rewrite -> Drop_S_Bridge_nat; Auto).
(Apply inhyps_rec; Apply H0; Auto).
(Unfold not ; Intros; Apply H2; Auto).

(Unfold not ; Intros; Apply H2; Auto).
Save.

Definition
    n_admis_strengthen : (h:Hyps)(n:N)(Q:F)(N_Deduc h n Q)->Prop :=
	[h:Hyps][n:N][Q:F][D:(N_Deduc h n Q)]
	 (i:nat)
	  ~(Occurs_In_N i n)->
	   (N_Deduc (Strengthen_Hyps i h) (drop_N i n) Q).

Definition
    a_admis_strengthen : (h:Hyps)(a:A)(Q:F)(A_Deduc h a Q)->Prop :=
	[h:Hyps][a:A][Q:F][D:(A_Deduc h a Q)]
	 (i:nat)
	  ~(Occurs_In_A i a)->
	   (A_Deduc (Strengthen_Hyps i h) (drop_A i a) Q).

Lemma N_admis_strengthen :
	((h:Hyps)(n:N)(Q:F)(n0:(N_Deduc h n Q))
	 (n_admis_strengthen h n Q n0))/\
	 ((h:Hyps)(a:A)(Q:F)(a0:(A_Deduc h a Q))
	  (a_admis_strengthen h a Q a0)).

(Apply N_A_Deduc_ind; Unfold n_admis_strengthen ; Unfold a_admis_strengthen ;
 Intros).
(Rewrite -> DROPN1; Apply Implies_I).
Rewrite <- Strengthen_Hyps_eq3.
(Apply H; Auto).
(Unfold not ; Intros; Apply H0; Auto).

(Rewrite -> DROPN2; Apply AN_Axiom; Apply H; Auto).
(Unfold not ; Intros; Apply H0; Auto).

(Rewrite -> DROPN3; Apply Implies_E with P:=P1 Q:=Q; Auto).
(Apply H; Auto).
(Unfold not ; Intros; Apply H1; Auto).

(Apply H0; Unfold not ; Intros; Apply H1; Auto).

(Rewrite -> DROPN4; Apply A_Axiom; Auto).
(Apply In_Strength; Auto).
(Unfold not ; Intros; Apply H; Auto).
Save.

Lemma N_Admis_Strengthen :
	(h:Hyps)(n:N)(Q:F)(i:nat)
	 (N_Deduc h n Q)->
	  ~(Occurs_In_N i n)->
	   (N_Deduc (Strengthen_Hyps i h) (drop_N i n) Q).

Cut (and
      (h:Hyps)(n:N)(Q:F)(n0:(N_Deduc h n Q))(n_admis_strengthen h n Q n0)
      (h:Hyps)(a:A)(Q:F)(a0:(A_Deduc h a Q))(a_admis_strengthen h a Q a0)).
Unfold n_admis_strengthen .
(Intros c; Case c; Clear  c; Intros).
Apply H; Auto.
Exact N_admis_strengthen.
Save.

Lemma A_Admis_Strengthen :
	(h:Hyps)(a:A)(Q:F)(i:nat)
	 (A_Deduc h a Q)->
	  ~(Occurs_In_A i a)->
	   (A_Deduc (Strengthen_Hyps i h) (drop_A i a) Q).

Cut (and
      (h:Hyps)(n:N)(Q:F)(n0:(N_Deduc h n Q))(n_admis_strengthen h n Q n0)
      (h:Hyps)(a:A)(Q:F)(a0:(A_Deduc h a Q))(a_admis_strengthen h a Q a0)).
Unfold a_admis_strengthen .
(Intros c; Case c; Clear  c; Intros).
(Apply H0; Auto).
Exact N_admis_strengthen.
Save.

Definition l_admis_strengthen : (h:Hyps)(l:L)(Q:F)(L_Deriv h l Q)->Prop :=
	[h:Hyps][l:L][Q:F][l0:(L_Deriv h l Q)]
	 (i:nat)
	   ~(Occurs_In_L i l)->
	    (L_Deriv (Strengthen_Hyps i h) (drop_L i l) Q).

Lemma L_admis_strengthen : (h:Hyps)(l:L)(Q:F)(l0:(L_Deriv h l Q))
			(l_admis_strengthen h l Q l0).

(Intros; Apply L_Deriv_ind1; Clear  l0 h l Q; Unfold l_admis_strengthen ;
 Intros).
(Simpl; Apply L_Axiom).
(Apply In_Strength; Auto).
(Unfold not ; Intros; Apply H; Auto).

Rewrite -> drop_L_eq2.
(Apply Implies_L with P:=P Q:=Q; Auto).
(Apply In_Strength; Auto).
(Unfold not ; Intros; Apply H1; Auto).

(Apply H; Auto).
(Unfold not ; Intros; Apply H1; Auto).

(Rewrite <- Strengthen_Hyps_eq3; Apply H0; Auto).
(Unfold not ; Intros; Apply H1; Auto).

(Rewrite -> drop_L_eq3; Apply Implies_R;
 Rewrite <- Strengthen_Hyps_eq3; Apply H; Auto; Unfold not ; Intros;
 Apply H0; Auto).

Save.

Lemma L_Admis_Strengthen :
	(h:Hyps)(l:L)(Q:F)(i:nat)
	 (L_Deriv h l Q)->
	   ~(Occurs_In_L i l)->
	    (L_Deriv (Strengthen_Hyps i h) (drop_L i l) Q).

Cut (h:Hyps)(l:L)(Q:F)(l0:(L_Deriv h l Q))(l_admis_strengthen h l Q l0).
Unfold l_admis_strengthen .
Intros.
(Apply H; Auto).

Exact L_admis_strengthen.
Save.