Require Export absorb.

Section Contraction_ind.

  Variable V : Type.
  Variable L : modal_operators.

  Variable op_eq : eq_type (operator L).
  Variable v_eq : eq_type V.

  Lemma provable_assumptions_contraction_rule :
    ∀(rules : set (sequent_rule V L))(n : nat)
          (r cr : sequent_rule V L)
          (sigma inj_sigma rsigma rho : lambda_subst V L),
      countably_infinite V →
      one_step_rule_set rules →
      absorbs_congruence rules →
      rules r →
      rules cr →
      rank_subst (S n) inj_sigma →
      renaming rsigma →
      renaming rho →
      subst_eq_on_vars sigma (subst_compose inj_sigma rsigma)
                       (prop_var_sequent (conclusion r)) →
      (∀(s : sequent V L),
         provable (GRC_n_set rules (S n)) (empty_sequent_set V L) s →
           provable (GR_n_set rules (S n)) (empty_sequent_set V L) s) →
      every_nth
        (provable (GR_n_set rules (S n)) (empty_sequent_set V L))
        (map (subst_sequent sigma) (assumptions r)) →
      every_nth
        (fun ca : sequent V L ⇒
           provable (GC_n_set V L 1)
             (reordered_sequent_list_set
                        (map (subst_sequent rsigma) (assumptions r)))
             (subst_sequent rho ca))
        (assumptions cr)
      →
        every_nth (provable (GR_n_set rules (S n)) (empty_sequent_set V L))
          (map (subst_sequent (subst_compose inj_sigma rho)) (assumptions cr)).

  Lemma head_contraction_closed_provable_subst_n_conclusions_ind :
    ∀(rules : set (sequent_rule V L))(n : nat),
      countably_infinite V →
      one_step_rule_set rules →
      absorbs_congruence rules →
      absorbs_contraction op_eq v_eq rules →
      (∀(s : sequent V L),
              provable (GRC_n_set rules (S n)) (empty_sequent_set V L) s →
                provable (GR_n_set rules (S n)) (empty_sequent_set V L) s) →
        head_contraction_closed
          (provable_subst_n_conclusions rules (2 + n) (lt_0_Sn (S n))).

  Lemma syntactic_GR_n_contraction_ind :
    ∀(rules : set (sequent_rule V L))(n : nat)
          (s : sequent V L)(f : lambda_formula V L),
      countably_infinite V →
      one_step_rule_set rules →
      absorbs_congruence rules →
      absorbs_contraction op_eq v_eq rules →
      (∀(s : sequent V L),
         provable (GRC_n_set rules (S n)) (empty_sequent_set V L) s →
           provable (GR_n_set rules (S n)) (empty_sequent_set V L) s) →
      provable (GR_n_set rules (2 + n)) (empty_sequent_set V L)
               (f :: f :: s) →
        provable (GR_n_set rules (2 + n)) (empty_sequent_set V L) (f :: s).

  Lemma syntactic_support_contraction_ind :
    ∀(rules : set (sequent_rule V L))(n : nat)(s1 s2 : sequent V L),
      (∀(s : sequent V L)(f : lambda_formula V L),
         provable (GR_n_set rules n) (empty_sequent_set V L)
                  (f :: f :: s) →
           provable (GR_n_set rules n) (empty_sequent_set V L)
                    (f :: s)) →
      provable (GR_n_set rules n) (empty_sequent_set V L) (s1 ++ s2) →
      incl s1 s2 →
        provable (GR_n_set rules n) (empty_sequent_set V L) s2.

  Lemma syntactic_support_contraction :
    ∀(rules : set (sequent_rule V L))(n : nat)(s : sequent V L),
      (∀(s : sequent V L)(f : lambda_formula V L),
         provable (GR_n_set rules n) (empty_sequent_set V L)
                  (f :: f :: s) →
           provable (GR_n_set rules n) (empty_sequent_set V L)
                    (f :: s)) →
      provable (GR_n_set rules n) (empty_sequent_set V L) s →
        provable (GR_n_set rules n) (empty_sequent_set V L)
                 (sequent_support op_eq v_eq s).

End Contraction_ind.