Cut elimination case c, part of 5.6.3

This module proves case c) in the syntactic cut-elimination proof. This is the case of a cut between two propositional rules. The proof reuses intermediate lemmas from the propositional cut elimination in module propositional_properties.

Require Export contraction.

Section Prop_cut.

  Variable V : Type.
  Variable L : modal_operators.

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

  Lemma syntactic_GR_n_cut_two_prop :
    ∀(rules : set (sequent_rule V L))(n m sd : nat)(ssn_pos : 0 < 2 + n)
          (f : lambda_formula V L)(r q : sequent V L)
          (f_rule negf_rule : sequent_rule V L)
          (Hf : G_n_set V L (2 + n) f_rule)
          (Hnf : G_n_set V L (2 + n) negf_rule)
          (f_sub :
             dep_list (sequent V L)
                      (proof (G_n_set V L (2 + n))
                          (provable_subst_n_conclusions rules (2 + n) ssn_pos))
                      (assumptions f_rule))
          (negf_sub :
             dep_list (sequent V L)
                      (proof (G_n_set V L (2 + n))
                          (provable_subst_n_conclusions rules (2 + n) ssn_pos))
                      (assumptions negf_rule)),
      countably_infinite V →
      absorbs_congruence rules →
      absorbs_contraction op_eq v_eq rules →
      one_step_rule_set 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) →
      (∀(f : lambda_formula V L)(r q : sequent V L),
         provable (G_n_set V L (2 + n))
                  (provable_subst_n_conclusions rules (2 + n) ssn_pos)
                  (f :: q) →
         provable (G_n_set V L (2 + n))
                  (provable_subst_n_conclusions rules (2 + n) ssn_pos)
                  (lf_neg f :: r) →
         formula_measure f < m →
           provable (G_n_set V L (2 + n))
                    (provable_subst_n_conclusions rules (2 + n) ssn_pos)
                    (q ++ r)) →
      (∀(f : lambda_formula V L)(r q : sequent V L)
             (p_fq : proof (G_n_set V L (2 + n))
                           (provable_subst_n_conclusions rules (2 + n) ssn_pos)
                           (f :: q))
             (p_nfr : proof (G_n_set V L (2 + n))
                            (provable_subst_n_conclusions rules (2 + n) ssn_pos)
                            (lf_neg f :: r)),
         proof_depth p_fq + proof_depth p_nfr ≤ sd →
         formula_measure f < S m →
           provable (G_n_set V L (2 + n))
                    (provable_subst_n_conclusions rules (2 + n) ssn_pos)
                    (q ++ r)) →
      formula_measure f < S m →
      proof_depth (rule (G_n_set V L (2 + n))
                        (provable_subst_n_conclusions rules (2 + n) ssn_pos)
                        f_rule Hf f_sub)
        + proof_depth (rule (G_n_set V L (2 + n))
                            (provable_subst_n_conclusions rules (2 + n) ssn_pos)
                            negf_rule Hnf negf_sub)
         ≤ S sd →
      conclusion f_rule = f :: q →
      conclusion negf_rule = lf_neg f :: r →
        provable (G_n_set V L (2 + n))
          (provable_subst_n_conclusions rules (2 + n) ssn_pos)
          (q ++ r).

End Prop_cut.