Definition KV : Set := nat.
Definition kv_enum : enumerator KV.
Definition kv_eq : eq_type KV := eq_nat_dec.
Inductive k_operator : Set := box_op : k_operator.
Definition KL : modal_operators :=
{| operator := k_operator;
arity := fun _ ⇒ 1
|}.
Definition kop_eq : eq_type (operator KL).
Definition k_formulas : Type := lambda_formula KV KL.
Definition k_sequent : Type := sequent KV KL.
Definition box(f : lambda_formula KV KL) : lambda_formula KV KL :=
lf_modal (box_op : operator KL) (counted_cons f counted_nil).
Definition neg_v(v : KV) : lambda_formula KV KL := lf_neg (lf_prop v).
Definition box_v(v : KV) : lambda_formula KV KL := box (lf_prop v).
Definition neg_box_v(v : KV) : lambda_formula KV KL :=
lf_neg (box (lf_prop v)).
Lemma propositional_neg_v : ∀(v : KV), propositional (neg_v v).
Lemma simple_modal_box_v :
∀(v : KV), neg_form_maybe simple_modal_form (box_v v).
Lemma simple_modal_neg_box_v :
∀(v : KV), neg_form_maybe simple_modal_form (neg_box_v v).
Lemma injective_neg_box_v : injective neg_box_v.
Lemma destruct_neg_sequent : ∀(s : sequent KV KL),
prop_sequent s →
every_nth neg_form s →
s = map neg_v (prop_var_sequent s).
Lemma destruct_mod_form : ∀(f : lambda_formula KV KL),
simple_modal_form f →
∃(v : KV),
prop_var_formula f = [v] ∧ f = box_v v.
Lemma destruct_mod_sequent : ∀(s : sequent KV KL),
every_nth simple_modal_form s →
s = map box_v (prop_var_sequent s).
Lemma destruct_neg_mod_form : ∀(f : lambda_formula KV KL),
neg_form_maybe simple_modal_form f →
neg_form f →
∃(v : KV),
prop_var_formula f = [v] ∧ f = neg_box_v v.
Lemma destruct_neg_mod_sequent : ∀(s : sequent KV KL),
simple_modal_sequent s →
every_nth neg_form s →
s = map neg_box_v (prop_var_sequent s).
Definition k_assumption_tail(n : nat) : sequent KV KL := map neg_v (seq 1 n).
Definition k_assumption(n : nat) : sequent KV KL :=
(lf_prop 0) :: (k_assumption_tail n).
Lemma length_k_assumption_tail : ∀(n : nat),
length (k_assumption_tail n) = n.
Lemma length_k_assumption : ∀(n : nat),
length (k_assumption n) = S n.
Lemma nth_k_assumption_tail :
∀(i n : nat)(i_less : i < length (k_assumption_tail n)),
nth (k_assumption_tail n) i i_less = neg_v (S i).
Lemma nth_subst_k_assumption_tail :
∀(sigma : lambda_subst KV KL)(i n : nat)
(i_less : i < length (subst_sequent sigma (k_assumption_tail n))),
nth (subst_sequent sigma (k_assumption_tail n)) i i_less =
lf_neg (sigma (S i)).
Lemma prop_sequent_k_assumption_tail : ∀(n : nat),
prop_sequent (k_assumption_tail n).
Lemma prop_sequent_k_assumption : ∀(n : nat),
prop_sequent (k_assumption n).
Lemma prop_sequent_subst_k_assumption_tail :
∀(sigma : lambda_subst KV KL)(n : nat),
renaming sigma →
prop_sequent (subst_sequent sigma (k_assumption_tail n)).
Lemma prop_sequent_subst_k_assumption :
∀(sigma : lambda_subst KV KL)(n : nat),
renaming sigma →
prop_sequent (subst_sequent sigma (k_assumption n)).
Lemma propositional_sequent_k_assumption_tail : ∀(n : nat),
propositional_sequent (k_assumption_tail n).
Lemma propositional_sequent_k_assumption : ∀(n : nat),
propositional_sequent (k_assumption n).
Lemma neg_sequent_subst_k_assumption_tail :
∀(sigma : lambda_subst KV KL)(n : nat),
every_nth neg_form (subst_sequent sigma (k_assumption_tail n)).
Lemma prop_var_sequent_k_assumption : ∀(n : nat),
prop_var_sequent (k_assumption n) = seq 0 (S n).
Definition k_conclusion_tail(n : nat) : sequent KV KL :=
map neg_box_v (seq 1 n).
Definition k_conclusion(n : nat) : sequent KV KL :=
(box_v 0) :: (k_conclusion_tail n).
Lemma k_conclusion_nonempty : ∀(n : nat),
k_conclusion n ≠ [].
Lemma length_k_conclusion_tail : ∀(n : nat),
length (k_conclusion_tail n) = n.
Lemma length_k_conclusion : ∀(n : nat),
length (k_conclusion n) = S n.
Lemma nth_k_conclusion_tail :
∀(i n : nat)(i_less : i < length (k_conclusion_tail n)),
nth (k_conclusion_tail n) i i_less = lf_neg (box (lf_prop (S i))).
Lemma nth_subst_k_conclusion_tail :
∀(sigma : lambda_subst KV KL)(i n : nat)
(i_less : i < length (subst_sequent sigma (k_conclusion_tail n))),
nth (subst_sequent sigma (k_conclusion_tail n)) i i_less =
lf_neg (box (sigma (S i))).
Lemma simple_modal_sequent_k_conclusion_tail : ∀(n : nat),
simple_modal_sequent (k_conclusion_tail n).
Lemma simple_modal_sequent_k_conclusion : ∀(n : nat),
simple_modal_sequent (k_conclusion n).
Lemma simple_modal_sequent_subst_k_conclusion_tail :
∀(sigma : lambda_subst KV KL)(n : nat),
renaming sigma →
simple_modal_sequent (subst_sequent sigma (k_conclusion_tail n)).
Lemma prop_modal_prop_sequent_k_conclusion : ∀(n : nat),
prop_modal_prop_sequent (k_conclusion n).
Lemma neg_sequent_subst_k_conclusion_tail :
∀(sigma : lambda_subst KV KL)(n : nat),
every_nth neg_form (subst_sequent sigma (k_conclusion_tail n)).
Lemma prop_var_sequent_k_conclusion : ∀(n : nat),
prop_var_sequent (k_conclusion n) = seq 0 (S n).
Definition k_rule(n : nat) : sequent_rule KV KL :=
{| assumptions := [k_assumption n]; conclusion := k_conclusion n |}.
Definition k_rules(r : sequent_rule KV KL) : Prop :=
∃(n : nat)(sa : sequent KV KL),
assumptions r = [sa] ∧ list_reorder sa (k_assumption n) ∧
list_reorder (conclusion r) (k_conclusion n).
Lemma k_rules_rule : ∀(n : nat), k_rules (k_rule n).
Lemma one_step_rule_set_k_rules : one_step_rule_set k_rules.
Definition k_rename_fun(vl : list KV) : KV → KV := fun(v : KV) ⇒
match lt_dec v (length vl) with
| left v_less ⇒ nth vl v v_less
| right _ ⇒ v
end.
Lemma k_rename_fun_less :
∀(vl : list KV)(n : nat)(n_less : n < length vl),
k_rename_fun vl n = nth vl n n_less.
Lemma subst_k_rename_k_assumption :
∀(v : KV)(vl : list KV),
subst_sequent (rename_of_fun (k_rename_fun (v :: vl)))
(k_assumption (length vl))
= (lf_prop v) :: (map neg_v vl).
Lemma subst_k_rename_k_conclusion :
∀(v : KV)(vl : list KV),
subst_sequent (rename_of_fun (k_rename_fun (v :: vl)))
(k_conclusion (length vl))
= (box_v v) :: (map neg_box_v vl).
Lemma subst_form_box_v :
∀(sigma : lambda_subst KV KL)(v : KV),
renaming sigma →
∃(v' : KV),
sigma v = lf_prop v' ∧
subst_form sigma (box_v v) = box_v v'.
Lemma subst_form_neg_box_v :
∀(sigma : lambda_subst KV KL)(v : KV),
renaming sigma →
∃(v' : KV),
sigma v = lf_prop v' ∧
subst_form sigma (neg_box_v v) = neg_box_v v'.
Lemma prop_var_sequent_subst_k_conclusion_tail_ind :
∀(sigma : lambda_subst KV KL)(vl : list KV),
renaming sigma →
prop_var_sequent (subst_sequent sigma (map neg_box_v vl)) =
prop_var_sequent (subst_sequent sigma (map neg_v vl)).
Lemma prop_var_sequent_subst_k_conclusion_tail :
∀(sigma : lambda_subst KV KL)(n : nat),
renaming sigma →
prop_var_sequent (subst_sequent sigma (k_conclusion_tail n)) =
prop_var_sequent (subst_sequent sigma (k_assumption_tail n)).
End K_syntax.