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

Absorbtion of contraction

Absorbtion of cut

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)

End K_absorb.