K example, Absorption properties and syntactic cut elimination, 5.2, 5.4

This module proves absorbtion of congruence, contruction and cut for K and then derives the syntactic cut-elimination results.
Note again, that no assumptions remaind from the generic theorems.

Require Export k_syntax syntactic_cut.

Section K_absorb.

Absorbtion of congruence


  Lemma k_absorbs_congruence : absorbs_congruence k_rules.

Absorbtion of contraction


  Lemma prop_var_sequent_support : ∀(s : sequent KV KL),
    prop_sequent s →
    every_nth neg_form s →
      list_support kv_eq (prop_var_sequent s) =
        prop_var_sequent (sequent_support kop_eq kv_eq s).

  Lemma k_absorbs_contraction : absorbs_contraction kop_eq kv_eq k_rules.

Absorbtion of cut


  Lemma k_absorbs_cut : absorbs_cut kop_eq kv_eq k_rules.

Syntactic cut elimination for K


  Theorem k_syntactic_cut :
    admissible_rule_set (GR_set k_rules) (empty_sequent_set KV KL) is_cut_rule.

  Theorem k_syntactic_contraction :
    admissible_rule_set (GR_set k_rules) (empty_sequent_set KV KL)
                        is_contraction_rule.

End K_absorb.