Cut elimination case a, part of 5.6.3
Require Export contraction factor_two_subst.
Section OSR_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_get_cut_rule :
∀(rules : set (sequent_rule V L))(n : nat)
(fsub : lambda_formula V L)
(rb_l rb_r : sequent_rule V L)(sigma_l sigma_r : lambda_subst V L)
(concl_l_subst concl_r_subst : sequent V L),
countably_infinite V →
one_step_rule_set rules →
absorbs_cut op_eq v_eq rules →
rules rb_l → rules rb_r →
rank_subst (S n) sigma_l → rank_subst (S n) sigma_r →
list_reorder (fsub :: concl_l_subst)
(subst_sequent sigma_l (conclusion rb_l)) →
list_reorder ((lf_neg fsub) :: concl_r_subst)
(subst_sequent sigma_r (conclusion rb_r))
→
∃(rsigma_l rsigma_r inj_sigma cut_sigma : lambda_subst V L)
(cut_r : sequent_rule V L)(concl_l concl_r : sequent V L),
renaming rsigma_l ∧ renaming rsigma_r ∧
renaming cut_sigma ∧ rank_subst (S n) inj_sigma ∧
injective inj_sigma ∧
rules cut_r ∧
rank_sequent 2 concl_l ∧ rank_sequent 2 concl_r ∧
concl_l_subst = subst_sequent inj_sigma concl_l ∧
concl_r_subst = subst_sequent inj_sigma concl_r ∧
map (subst_sequent sigma_l) (assumptions rb_l) =
map (subst_sequent (subst_compose inj_sigma rsigma_l))
(assumptions rb_l) ∧
map (subst_sequent sigma_r) (assumptions rb_r) =
map (subst_sequent (subst_compose inj_sigma rsigma_r))
(assumptions rb_r) ∧
multi_subset
(sequent_support op_eq v_eq
(subst_sequent cut_sigma (conclusion cut_r)))
(concl_l ++ concl_r) ∧
every_nth
(fun ass ⇒
provable (GC_n_set V L 1)
(reordered_sequent_list_set
((map (subst_sequent rsigma_l) (assumptions rb_l)) ++
(map (subst_sequent rsigma_r) (assumptions rb_r))))
(subst_sequent cut_sigma ass))
(assumptions cut_r).
Lemma syntactic_GR_n_prove_cut_absorb_assumptions :
∀(rules : set (sequent_rule V L))(n : nat)
(rb_l rb_r cut_r : sequent_rule V L)
(rsigma_l rsigma_r inj_sigma cut_sigma : lambda_subst V L),
countably_infinite V →
one_step_rule_set rules →
absorbs_congruence rules →
rules rb_l → rules rb_r →
renaming rsigma_l → renaming rsigma_r → renaming cut_sigma →
rank_subst (S n) inj_sigma →
every_nth (provable (GR_n_set rules (S n)) (empty_sequent_set V L))
(map (subst_sequent (subst_compose inj_sigma rsigma_l))
(assumptions rb_l)) →
every_nth (provable (GR_n_set rules (S n)) (empty_sequent_set V L))
(map (subst_sequent (subst_compose inj_sigma rsigma_r))
(assumptions rb_r)) →
every_nth
(fun(ass : sequent V L) ⇒
provable (GC_n_set V L 1)
(reordered_sequent_list_set
(map (subst_sequent rsigma_l) (assumptions rb_l) ++
map (subst_sequent rsigma_r) (assumptions rb_r)))
(subst_sequent cut_sigma ass))
(assumptions cut_r)
→
every_nth
(provable (GRC_n_set rules (S n)) (empty_sequent_set V L))
(map (subst_sequent (subst_compose inj_sigma cut_sigma))
(assumptions cut_r)).
Lemma syntactic_GR_n_prove_cut_absorb_conclusion :
∀(rules : set (sequent_rule V L))(n : nat)
(cut_r : sequent_rule V L)
(inj_sigma cut_sigma : lambda_subst V L),
one_step_rule_set rules →
rules cut_r →
renaming cut_sigma →
rank_subst (S n) inj_sigma →
every_nth (provable (GR_n_set rules (S n)) (empty_sequent_set V L))
(map (subst_sequent (subst_compose inj_sigma cut_sigma))
(assumptions cut_r))
→
provable (GR_n_set rules (2 + n)) (empty_sequent_set V L)
(subst_sequent (subst_compose inj_sigma cut_sigma)
(conclusion cut_r)).
Lemma syntactic_GR_n_cut_eli_two_osr_concl :
∀(rules : set (sequent_rule V L))(n : nat)(ssn_pos : 0 < 2 + n)
(f : lambda_formula V L)(q r : sequent V L)
(rb_l rb_r : sequent_rule V L)(sigma_l sigma_r : lambda_subst V L)
(delta_l delta_r concl_l_tl concl_r_tl : sequent V L),
countably_infinite V →
one_step_rule_set rules →
absorbs_congruence rules →
absorbs_cut op_eq v_eq rules →
(∀(s : sequent V L)(f : lambda_formula V L),
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))
→
(∀(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) →
rules rb_l → rules rb_r →
rank_subst (S n) sigma_l → rank_subst (S n) sigma_r →
rank_sequent (2 + n) delta_l → rank_sequent (2 + n) delta_r →
list_reorder (f :: q)
(subst_sequent sigma_l (conclusion rb_l) ++ delta_l) →
list_reorder (f :: concl_l_tl)
(subst_sequent sigma_l (conclusion rb_l)) →
list_reorder ((lf_neg f) :: r)
(subst_sequent sigma_r (conclusion rb_r) ++ delta_r) →
list_reorder ((lf_neg f) :: concl_r_tl)
(subst_sequent sigma_r (conclusion rb_r)) →
every_nth
(provable (GR_n_set rules (S n)) (empty_sequent_set V L))
(map (subst_sequent sigma_l) (assumptions rb_l)) →
every_nth
(provable (GR_n_set rules (S n)) (empty_sequent_set V L))
(map (subst_sequent sigma_r) (assumptions rb_r)) →
provable (G_n_set V L (2 + n))
(provable_subst_n_conclusions rules (2 + n) ssn_pos)
(q ++ r).
Lemma syntactic_GR_n_cut_eli_two_osr :
∀(rules : set (sequent_rule V L))(n : nat)(ssn_pos : 0 < 2 + n)
(f : lambda_formula V L)(r q : sequent V L),
countably_infinite V →
one_step_rule_set rules →
absorbs_cut op_eq v_eq rules →
absorbs_congruence rules →
(∀(s : sequent V L)(f : lambda_formula V L),
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))
→
(∀(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_subst_n_conclusions rules (2 + n) ssn_pos (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 OSR_cut.