Require Export factor_subst propositional_properties backward_substitution
               cut_properties.

Section Absorbtion.

  Variable V : Type.
  Variable L : modal_operators.

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

  Lemma one_step_rule_simple_modal_conclusion_subst_reorder :
    ∀(rules : set (sequent_rule V L))(sigma : lambda_subst V L)
          (r : sequent_rule V L)(s : sequent V L),
      one_step_rule_set rules →
      rules r →
      renaming sigma →
      list_reorder s (subst_sequent sigma (conclusion r)) →
        simple_modal_sequent s.

  Lemma one_step_rule_propositional_subst_assumptions :
    ∀(rules : set (sequent_rule V L))(sigma : lambda_subst V L)
          (r : sequent_rule V L),
      one_step_rule_set rules →
      rules r →
      renaming sigma →
        every_nth propositional_sequent
          (map (subst_sequent sigma) (assumptions r)).

  Definition congruence_assumption_list(pv qv : list (lambda_formula V L))
                                          : list (list (lambda_formula V L)) :=
    let pqv := combine pv qv
    in
      (map (fun pq ⇒ [lf_neg (fst pq); snd pq]) pqv) ++
      (map (fun pq ⇒ [fst pq; lf_neg (snd pq)]) pqv).

  Definition congruence_assumptions(n : nat)
                              (pv qv : counted_list (lambda_formula V L) n)
                                                        : set (sequent V L) :=
    reordered_sequent_list_set
      (congruence_assumption_list (list_of_counted_list pv)
                                  (list_of_counted_list qv)).

  Lemma congruence_assumptions_char :
    ∀(n : nat)(args : counted_list (lambda_formula V L) n)
          (s : sequent V L),
      every_nth prop_form (list_of_counted_list args) →
      congruence_assumptions n args args s →
        (∃(v : V), s = [lf_neg (lf_prop v); lf_prop v] ∨
                        s = [lf_prop v; lf_neg (lf_prop v)]
        ) ∧ rank_sequent 1 s.

  Lemma rank_sequent_set_congruence_assumptions :
    ∀(n : nat)(args : counted_list (lambda_formula V L) n),
      every_nth prop_form (list_of_counted_list args) →
        rank_sequent_set 1 (congruence_assumptions n args args).

  Lemma congruence_assumptions_subset :
    ∀(n r : nat)(args : counted_list (lambda_formula V L) n)
          (sigma : lambda_subst V L),
      rank_subst (S r) sigma →
      every_nth prop_form (list_of_counted_list args) →
        subset (subst_sequent_set sigma (congruence_assumptions n args args))
               (subst_Ax_n_set sigma (2 + r)).

  Lemma congruence_assumptions_provable_with_ax :
    ∀(rules : set (sequent_rule V L))(n : nat)
          (args : counted_list (lambda_formula V L) n)
          (s : sequent V L),
      subset (rank_rules 1 is_ax_rule) rules →
      every_nth prop_form (list_of_counted_list args) →
        (provable rules (congruence_assumptions n args args) s ↔
         provable rules (empty_sequent_set V L) s).

  Definition absorbs_congruence(rules : set (sequent_rule V L)) : Prop :=
    ∀(op : operator L)
          (pv qv : counted_list (lambda_formula V L) (arity L op)),
      every_nth prop_form (list_of_counted_list pv) →
      every_nth prop_form (list_of_counted_list qv) →
        ∃(r : sequent_rule V L)(sigma : lambda_subst V L),
          rules r ∧
          rank_subst 1 sigma ∧
          multi_subset (subst_sequent sigma (conclusion r))
                       [lf_neg (lf_modal op pv); lf_modal op qv]
          ∧
          every_nth
            (fun(s : sequent V L) ⇒
               provable (GC_n_set V L 1)
                        (congruence_assumptions (arity L op) pv qv)
                 (subst_sequent sigma s))
            (assumptions r).

  Definition absorbs_contraction(rules : set (sequent_rule V L)) : Prop :=
    ∀(or : sequent_rule V L)(sigma : lambda_subst V L),
      rules or →
      renaming sigma →
        ∃(cr : sequent_rule V L)(rho : lambda_subst V L),
          rules cr ∧ renaming rho ∧
          multi_subset
            (subst_sequent rho (conclusion cr))
            (sequent_support op_eq v_eq (subst_sequent sigma (conclusion or)))
          ∧
          every_nth
            (fun ca ⇒
               provable (GC_n_set V L 1)
                        (reordered_sequent_list_set
                                 (map (subst_sequent sigma) (assumptions or)))
                 (subst_sequent rho ca))
            (assumptions cr).

  Lemma absorbs_contraction_head :
    ∀(rules : set (sequent_rule V L))(or : sequent_rule V L)
          (sigma : lambda_subst V L)(f : lambda_formula V L)(s : sequent V L),
      one_step_rule_set rules →
      absorbs_contraction rules →
      rules or →
      renaming sigma →
      list_reorder (f :: f :: s) (subst_sequent sigma (conclusion or)) →
        ∃(cr : sequent_rule V L)(rho : lambda_subst V L)
              (delta : sequent V L),
          rules cr ∧ renaming rho ∧ simple_modal_sequent delta ∧
          list_reorder (f :: s) ((subst_sequent rho (conclusion cr)) ++ delta)
          ∧
          every_nth
            (fun ca ⇒
               provable (GC_n_set V L 1)
                        (reordered_sequent_list_set
                                 (map (subst_sequent sigma) (assumptions or)))
                 (subst_sequent rho ca))
            (assumptions cr).

  Definition absorbs_cut(rules : set (sequent_rule V L)) : Prop :=
    ∀(rl rr : sequent_rule V L)(sl sr : lambda_subst V L)(nl nr : nat)
          (nl_less : nl < length (subst_sequent sl (conclusion rl)))
          (nr_less : nr < length (subst_sequent sr (conclusion rr))),
      rules rl → rules rr →
      renaming sl → renaming sr →
      lf_neg (nth (subst_sequent sl (conclusion rl)) nl nl_less) =
      nth (subst_sequent sr (conclusion rr)) nr nr_less →
        ∃(rb : sequent_rule V L)(sb : lambda_subst V L),
          rules rb ∧ renaming sb ∧
          multi_subset
            (sequent_support op_eq v_eq (subst_sequent sb (conclusion rb)))
            ((cutout_nth (subst_sequent sl (conclusion rl)) nl) ++
             (cutout_nth (subst_sequent sr (conclusion rr)) nr)) ∧
          every_nth
            (fun ba ⇒
               provable (GC_n_set V L 1)
                        (reordered_sequent_list_set
                           ((map (subst_sequent sl) (assumptions rl)) ++
                            (map (subst_sequent sr) (assumptions rr))))
                 (subst_sequent sb ba))
            (assumptions rb).

  Lemma GR_n_non_atomic_axiom_head :
    ∀(rules : set (sequent_rule V L))(n : nat)
          (s : sequent V L)(f : lambda_formula V L),
      countably_infinite V →
      one_step_rule_set rules →
      absorbs_congruence rules →
      rank_sequent (2 + n) s →
      rank_formula (2 + n) f →
      (∀ (s : sequent V L) (f : lambda_formula V L),
         rank_sequent (S n) s →
         rank_formula (S n) f →
           provable (GR_n_set rules (S n)) (empty_sequent_set V L)
                    (f :: lf_neg f :: s)) →
        provable (GR_n_set rules (2 + n)) (empty_sequent_set V L)
                 (f :: lf_neg f :: s).

  Lemma syntactic_GR_n_non_atomic_axioms :
    ∀(rules : set (sequent_rule V L))(n : nat)
          (s : sequent V L)(f : lambda_formula V L),
      countably_infinite V →
      one_step_rule_set rules →
      absorbs_congruence rules →
      rank_sequent n s →
      rank_formula n f →
        provable (GR_n_set rules n) (empty_sequent_set V L)
                 (f :: (lf_neg f) :: s).

  Lemma syntactic_GR_n_provable_subst_Ax :
    ∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))
          (sigma : lambda_subst V L)(n : nat)(s : sequent V L),
      countably_infinite V →
      one_step_rule_set rules →
      absorbs_congruence rules →
      rank_subst n sigma →
      subst_Ax_n_set sigma n s →
        provable (GR_n_set rules n) hyp s.

End Absorbtion.

Implicit Arguments absorbs_congruence [V L].
Implicit Arguments absorbs_contraction [V L].
Implicit Arguments absorbs_contraction_head [V L].
Implicit Arguments absorbs_cut [V L].