Require Export formulas.
Section Propositional_formulas.
Variable V : Type.
Variable L : modal_operators.
Definition propositional(f : lambda_formula V L) : Prop :=
rank_formula 1 f.
Lemma propositional_lf_prop : ∀(v : V),
propositional (lf_prop v).
Lemma propositional_neg : ∀(f : lambda_formula V L),
propositional (lf_neg f) → propositional f.
Lemma propositional_neg_inv : ∀(f : lambda_formula V L),
propositional f → propositional (lf_neg f).
Lemma propositional_lf_and : ∀(f1 f2 : lambda_formula V L),
propositional f1 →
propositional f2 →
propositional (lf_and f1 f2).
Lemma propositional_and_left : ∀(f1 f2 : lambda_formula V L),
propositional (lf_and f1 f2) → propositional f1.
Lemma propositional_and_right : ∀(f1 f2 : lambda_formula V L),
propositional (lf_and f1 f2) → propositional f2.
Lemma propositional_tcc_modal :
∀{X : Type}(op : operator L)
(args : counted_list (lambda_formula V L) (arity L op)),
propositional (lf_modal op args) → X.
Lemma propositional_lambda_or :
∀(f1 f2 : lambda_formula V L),
propositional f1 →
propositional f2 →
propositional (lambda_or f1 f2).
Definition propositional_sequent(s : sequent V L) : Prop :=
rank_sequent 1 s.
Lemma propositional_sequent_empty : propositional_sequent [].
Lemma propositional_sequent_head :
∀(s : sequent V L)(f : lambda_formula V L),
propositional_sequent (f :: s) → propositional f.
Lemma propositional_sequent_tail :
∀(s : sequent V L)(f : lambda_formula V L),
propositional_sequent (f :: s) → propositional_sequent s.
Lemma propositional_or_formula :
∀(nonempty_v : V)(s : sequent V L),
propositional_sequent s →
propositional (or_formula_of_sequent s nonempty_v).
Lemma propositional_sequent_cons :
∀(s : sequent V L)(f : lambda_formula V L),
propositional f →
propositional_sequent s →
propositional_sequent (f :: s).
Lemma propositional_sequent_append :
∀(sl sr : sequent V L),
propositional_sequent sl →
propositional_sequent sr →
propositional_sequent (sl ++ sr).
Lemma propositional_sequent_append_left :
∀(sl sr : sequent V L),
propositional_sequent (sl ++ sr) →
propositional_sequent sl.
Lemma propositional_sequent_append_right :
∀(sl sr : sequent V L),
propositional_sequent (sl ++ sr) →
propositional_sequent sr.
Lemma propositional_sequent_cons_append :
∀(l1 l2 : sequent V L)(f1 f2 : lambda_formula V L),
(propositional f1 → propositional f2) →
propositional_sequent (l1 ++ f1 :: l2) →
propositional_sequent (l1 ++ f2 :: l2).
Lemma prop_form_is_propositional : ∀(f : lambda_formula V L),
prop_form f → propositional f.
Lemma prop_sequent_is_propositional : ∀(s : sequent V L),
prop_sequent s → propositional_sequent s.
End Propositional_formulas.
Implicit Arguments propositional [[V] [L]].
Implicit Arguments propositional_neg [V L].
Implicit Arguments propositional_and_left [V L].
Implicit Arguments propositional_and_right [V L].
Implicit Arguments propositional_tcc_modal [V L X].
Implicit Arguments propositional_sequent [[V] [L]].
Implicit Arguments propositional_sequent_tail [V L].
Implicit Arguments propositional_lambda_or [V L].
Implicit Arguments propositional_sequent_append_right [V L].
Implicit Arguments propositional_sequent_head [V L].
Implicit Arguments propositional_sequent_append [V L].
Implicit Arguments propositional_or_formula [V L].
Implicit Arguments prop_sequent_is_propositional [V L].