Require Export propositional_properties.

Section Mixed_cut.

  Variable V : Type.
  Variable L : modal_operators.

  Lemma mixed_cut_ax :
    ∀(rules : set (sequent_rule V L))(n : nat)(ssn_pos : 0 < 2 + n)
          (f : lambda_formula V L)(r q : sequent V L),
      not (neg_form_maybe prop_form f) →
      simple_tautology (f :: q) →
      rank_sequent (2 + n) (f :: q) →
      rank_sequent (2 + n) r →
        provable (G_n_set V L (2 + n))
          (provable_subst_n_conclusions rules (2 + n) ssn_pos)
          (q ++ r).

  Lemma mixed_cut_left_osr :
    ∀(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)
          (negf_rule : sequent_rule V L)
          (H : G_n_set V L (2 + n) negf_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)),
      one_step_rule_set rules →
      (∀(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 →
      1 + proof_depth (rule (G_n_set V L (2 + n))
                            (provable_subst_n_conclusions rules (2 + n) ssn_pos)
                            negf_rule H negf_sub)
         ≤ S sd →
      provable_subst_n_conclusions rules (2 + n) ssn_pos (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).

  Lemma mixed_cut_right_osr :
    ∀(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 : sequent_rule V L)
          (H : G_n_set V L (2 + n) f_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)),
      one_step_rule_set rules →
      (∀(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 H f_sub)
        + 1 ≤ S sd →
      conclusion f_rule = f :: q →
      provable_subst_n_conclusions rules (2 + n) ssn_pos ((lf_neg f) :: r) →
        provable (G_n_set V L (2 + n))
          (provable_subst_n_conclusions rules (2 + n) ssn_pos)
          (q ++ r).

End Mixed_cut.