K example, equivalence with the (N), (D) rule set

This is work in progress to prove the equivalence of the K-rule set with the rules (N) and (D).

Require Export k_syntax.

Section K_nd.

(N), (D) rule set


  Definition k_n_rule(r : sequent_rule KV KL) : Prop :=
    assumptions r = [[lf_prop 0]] ∧ conclusion r = [box_v 0].

  Definition k_d_rule(r : sequent_rule KV KL) : Prop :=
    ∃(sa : sequent KV KL),
      assumptions r = [sa] ∧ list_reorder sa (k_assumption 2) ∧
      list_reorder (conclusion r) (k_conclusion 2).

  Definition k_nd_rules : set (sequent_rule KV KL) :=
    union k_n_rule k_d_rule.

  Lemma rule_multiset_k_nd : rule_multiset k_nd_rules.

  Lemma provable_k_nd_hyp_list_reorder :
    ∀(hyp : set (sequent KV KL))(s1 s2 : sequent KV KL),
      sequent_multiset hyp →
      list_reorder s1 s2 →
      provable k_nd_rules hyp s1 →
        provable k_nd_rules hyp s2.

Towards the equivalence of the rule sets


  Lemma k_nd_subset : subset k_nd_rules k_rules.

  Lemma k_n_rule_eq_1 : ∀(r : sequent_rule KV KL),
    k_n_rule r →
      r = k_rule 0.

End K_nd.