Cut elimination case b, part of 5.6.3
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.