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