N-step semantics 4.9 - 4.10, 4.12
- simplified n-step sequent semantics
- upward correctness of G wrt. n-step semantics
- relation to propositional models/validity
- projections of the n-step semantics for modal and propositional sequents
- relation to X,tau |= f and TX,tau |= f semantics via substitutions
Require Export classic slice semantics build_proof propositional_models.
Section Step_semantics.
Variable V : Type.
Variable L : modal_operators.
Variable T : functor.
Fixpoint step_semantics(LS : lambda_structure L T)
(f : lambda_formula V L)
(n : nat)(rank : rank_formula (S n) f) :
set (terminal_obj_sequence V T n) :=
match f
return rank_formula (S n) f → set (terminal_obj_sequence V T n)
with
| lf_prop v ⇒
fun(rank : rank_formula (S n) (lf_prop v)) ⇒
inv_img (terminal_obj_sequence_pi_2 n) (sets_containing v)
| lf_neg f ⇒
fun(rank : rank_formula (S n) (lf_neg f)) ⇒
set_inverse (step_semantics LS f n
(rank_formula_lf_neg_TCC (S n) f rank))
| lf_and f1 f2 ⇒
fun(rank : rank_formula (S n) (lf_and f1 f2)) ⇒
intersection
(step_semantics LS f1 n (rank_formula_and_left (S n) f1 f2 rank))
(step_semantics LS f2 n (rank_formula_and_right (S n) f1 f2 rank))
| lf_modal op args ⇒
fun(rank : rank_formula (S n) (lf_modal op args)) ⇒
match n
return rank_formula (S n) (lf_modal op args) →
set (terminal_obj_sequence V T n)
with
| 0 ⇒
fun(rank : rank_formula 1 (lf_modal op args)) ⇒
rank_formula_modal_1_TCC _ _ _ rank
| S n ⇒
fun(rank : rank_formula (2 + n) (lf_modal op args)) ⇒
inv_img
(terminal_obj_sequence_pi_1 n)
(modal_semantics LS op
((fix map_args(len : nat)
(args : counted_list (lambda_formula V L) len)
(rank : every_nth (rank_formula (S n))
(list_of_counted_list args))
: counted_list
(set (terminal_obj_sequence V T n)) len :=
match args
in counted_list _ len
return every_nth (rank_formula (S n))
(list_of_counted_list args)
→ counted_list
(set (terminal_obj_sequence V T n)) len
with
| counted_nil ⇒ fun _ ⇒ counted_nil
| counted_cons len f rargs ⇒
fun(rank : every_nth (rank_formula (S n))
(f :: (list_of_counted_list rargs))) ⇒
counted_cons
(step_semantics LS f n
(every_nth_head _ _ _ rank))
(map_args len rargs (every_nth_tail _ _ _ rank))
end rank
) (arity L op) args
(rank_formula_modal_args_TCC _ _ _ rank)
))
end rank
end rank.
Define the inner fixpoint on counted lists in the previous
definition as separate function.
Fixpoint step_semantics_args(LS : lambda_structure L T)(len : nat)
(args : counted_list (lambda_formula V L) len)
(n : nat)
(rank : every_nth (rank_formula (S n))
(list_of_counted_list args))
: counted_list (set (terminal_obj_sequence V T n)) len :=
match args in counted_list _ len
return every_nth (rank_formula (S n)) (list_of_counted_list args) →
counted_list (set (terminal_obj_sequence V T n)) len
with
| counted_nil ⇒ fun _ ⇒ counted_nil
| counted_cons len f rargs ⇒
fun(rank : every_nth (rank_formula (S n))
(f :: (list_of_counted_list rargs))) ⇒
counted_cons
(step_semantics LS f n (every_nth_head _ _ _ rank))
(step_semantics_args LS len rargs n (every_nth_tail _ _ _ rank))
end rank.
Lemma step_semantics_modal :
∀(LS : lambda_structure L T)
(op : operator L)
(args : counted_list (lambda_formula V L) (arity L op))
(n : nat)(rank : rank_formula (2 + n) (lf_modal op args)),
step_semantics LS (lf_modal op args) (S n) rank =
inv_img (terminal_obj_sequence_pi_1 n)
(modal_semantics LS op
(step_semantics_args LS (arity L op) args n
(rank_formula_modal_args_TCC _ _ _ rank))).
Lemma step_semantics_tcc_irr_eq :
∀(LS : lambda_structure L T)(f : lambda_formula V L)
(n : nat)(rank1 rank2 : rank_formula (S n) f),
step_semantics LS f n rank1 = step_semantics LS f n rank2.
Lemma step_semantics_tcc_irr :
∀(LS : lambda_structure L T)(n : nat)
(x : terminal_obj_sequence V T n)(f : lambda_formula V L)
(rank1 rank2 : rank_formula (S n) f),
step_semantics LS f n rank1 x → step_semantics LS f n rank2 x.
Lemma nth_step_semantics_args :
∀(LS : lambda_structure L T)
(len : nat)(args : counted_list (lambda_formula V L) len)
(n : nat)
(rank : every_nth (rank_formula (S n)) (list_of_counted_list args))
(i : nat)(i_less : i < len),
nth (list_of_counted_list (step_semantics_args LS len args n rank))
i (less_length_counted_list _ _ _ i_less) =
step_semantics LS
(nth (list_of_counted_list args)
i (less_length_counted_list _ _ _ i_less))
n (rank i (less_length_counted_list _ _ _ i_less)).
Lemma step_semantics_lf_neg_rev :
∀(LS : lambda_structure L T)(f : lambda_formula V L)(n : nat)
(rank : rank_formula (S n) f)(x : terminal_obj_sequence V T n),
not (step_semantics LS f n rank x) →
step_semantics LS (lf_neg f) n
(iff_right (rank_formula_lf_neg _ _) rank) x.
Lemma step_semantics_false :
∀(nonempty_v : V)(LS : lambda_structure L T)(n : nat)
(rank : rank_formula (S n) (lambda_false nonempty_v))
(x : terminal_obj_sequence V T n),
not (step_semantics LS (lambda_false nonempty_v) n rank x).
(args : counted_list (lambda_formula V L) len)
(n : nat)
(rank : every_nth (rank_formula (S n))
(list_of_counted_list args))
: counted_list (set (terminal_obj_sequence V T n)) len :=
match args in counted_list _ len
return every_nth (rank_formula (S n)) (list_of_counted_list args) →
counted_list (set (terminal_obj_sequence V T n)) len
with
| counted_nil ⇒ fun _ ⇒ counted_nil
| counted_cons len f rargs ⇒
fun(rank : every_nth (rank_formula (S n))
(f :: (list_of_counted_list rargs))) ⇒
counted_cons
(step_semantics LS f n (every_nth_head _ _ _ rank))
(step_semantics_args LS len rargs n (every_nth_tail _ _ _ rank))
end rank.
Lemma step_semantics_modal :
∀(LS : lambda_structure L T)
(op : operator L)
(args : counted_list (lambda_formula V L) (arity L op))
(n : nat)(rank : rank_formula (2 + n) (lf_modal op args)),
step_semantics LS (lf_modal op args) (S n) rank =
inv_img (terminal_obj_sequence_pi_1 n)
(modal_semantics LS op
(step_semantics_args LS (arity L op) args n
(rank_formula_modal_args_TCC _ _ _ rank))).
Lemma step_semantics_tcc_irr_eq :
∀(LS : lambda_structure L T)(f : lambda_formula V L)
(n : nat)(rank1 rank2 : rank_formula (S n) f),
step_semantics LS f n rank1 = step_semantics LS f n rank2.
Lemma step_semantics_tcc_irr :
∀(LS : lambda_structure L T)(n : nat)
(x : terminal_obj_sequence V T n)(f : lambda_formula V L)
(rank1 rank2 : rank_formula (S n) f),
step_semantics LS f n rank1 x → step_semantics LS f n rank2 x.
Lemma nth_step_semantics_args :
∀(LS : lambda_structure L T)
(len : nat)(args : counted_list (lambda_formula V L) len)
(n : nat)
(rank : every_nth (rank_formula (S n)) (list_of_counted_list args))
(i : nat)(i_less : i < len),
nth (list_of_counted_list (step_semantics_args LS len args n rank))
i (less_length_counted_list _ _ _ i_less) =
step_semantics LS
(nth (list_of_counted_list args)
i (less_length_counted_list _ _ _ i_less))
n (rank i (less_length_counted_list _ _ _ i_less)).
Lemma step_semantics_lf_neg_rev :
∀(LS : lambda_structure L T)(f : lambda_formula V L)(n : nat)
(rank : rank_formula (S n) f)(x : terminal_obj_sequence V T n),
not (step_semantics LS f n rank x) →
step_semantics LS (lf_neg f) n
(iff_right (rank_formula_lf_neg _ _) rank) x.
Lemma step_semantics_false :
∀(nonempty_v : V)(LS : lambda_structure L T)(n : nat)
(rank : rank_formula (S n) (lambda_false nonempty_v))
(x : terminal_obj_sequence V T n),
not (step_semantics LS (lambda_false nonempty_v) n rank x).
Definition step_semantics_sequent
(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
(n : nat)(rank : rank_sequent (S n) s) :
set (terminal_obj_sequence V T n) :=
step_semantics LS (or_formula_of_sequent s nonempty_v) n
(rank_formula_succ_or_formula_of_sequent n nonempty_v s rank).
Lemma step_semantics_sequent_tcc_irr :
∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
(n : nat)(rank1 rank2 : rank_sequent (S n) s),
step_semantics_sequent nonempty_v LS s n rank1 =
step_semantics_sequent nonempty_v LS s n rank2.
Lemma step_semantics_sequent_empty :
∀(nonempty_v : V)(LS : lambda_structure L T)
(n : nat)(rank : rank_sequent (S n) []),
set_equal (step_semantics_sequent nonempty_v LS [] n rank)
(empty_set (terminal_obj_sequence V T n)).
Definition step_semantics_valid
(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
(n : nat)(rank : rank_sequent (S n) s) : Prop :=
is_full_set (step_semantics_sequent nonempty_v LS s n rank).
Lemma step_semantics_valid_tcc_irr :
∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
(n : nat)(rank1 rank2 : rank_sequent (S n) s),
step_semantics_valid nonempty_v LS s n rank1 →
step_semantics_valid nonempty_v LS s n rank2.
Lemma step_semantics_valid_nonempty :
∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
(n : nat)(rank : rank_sequent (S n) s),
step_semantics_valid nonempty_v LS s n rank →
(∃(x : terminal_obj_sequence V T n), True) →
s ≠ [].
Lemma step_semantics_valid_taut :
∀(nonempty_v : V)(LS : lambda_structure L T)
(sigma : lambda_subst V L)(s : sequent V L)
(k : nat)(rank : rank_sequent (S k) s),
subst_Ax_set sigma s →
step_semantics_valid nonempty_v LS s k rank.
Definition step_semantics_valid_at_rank
(nonempty_v : V)(LS : lambda_structure L T)(n : nat)
: set (sequent V L) :=
fun(s : sequent V L) ⇒
rank # rank_sequent (S n) s
/#\ step_semantics_valid nonempty_v LS s n rank.
Definition slice_model(m : model V T)
: (state m) → slice_obj_T T (state m) V :=
pair (coalg m) (coval m).
Lemma semantics_step_semantics :
∀(LS : lambda_structure L T)(m : model V T)
(f : lambda_formula V L)(n : nat)(rank : rank_formula (S n) f),
set_equal
(form_semantics LS m f)
(inv_img (terminal_seq_cone (slice_model m) n)
(step_semantics LS f n rank)).
Definition nth_unit_model(c : slice_unit_coalg V T)(n : nat) : model V T :=
{| state := terminal_obj_sequence V T n;
coalg := terminal_obj_sequence_pi_1 n ∘ unit_coalg_sequence c n;
coval := terminal_obj_sequence_pi_2 (S n) ∘ unit_coalg_sequence c n
|}.
Lemma slice_model_nth_unit :
∀(c : slice_unit_coalg V T)(n : nat),
slice_model (nth_unit_model c n) ≡ unit_coalg_sequence c n.
Lemma step_semantics_validity :
∀(nonempty_v : V)(LS : lambda_structure L T)(n : nat)
(s : sequent V L)(rank : rank_sequent (S n) s),
non_trivial_functor T →
(valid_all_models nonempty_v LS s ↔
step_semantics_valid nonempty_v LS s n rank).
∀(nonempty_v : V)(LS : lambda_structure L T)(n : nat)
(s : sequent V L)(rank : rank_sequent (S n) s),
non_trivial_functor T →
(valid_all_models nonempty_v LS s ↔
step_semantics_valid nonempty_v LS s n rank).
Definition state_seq_step_form_pred(LS : lambda_structure L T)(n : nat)
(x : terminal_obj_sequence V T n)
(f : lambda_formula V L)
(rank_f : rank_formula (S n) f) : Prop :=
step_semantics LS f n rank_f x.
Definition state_seq_step_semantics(LS : lambda_structure L T)
(s : sequent V L)
(n : nat)(rank : rank_sequent (S n) s)
(x : terminal_obj_sequence V T n) : Prop :=
some_neg_dep (rank_formula (S n))
(state_seq_step_form_pred LS n x) s rank.
Lemma state_seq_step_semantics_tcc_irr :
∀(LS : lambda_structure L T)(s : sequent V L)
(n : nat)(rank1 rank2 : rank_sequent (S n) s)
(x : terminal_obj_sequence V T n),
state_seq_step_semantics LS s n rank1 x →
state_seq_step_semantics LS s n rank2 x.
Lemma state_seq_step_semantics_list_reorder :
∀(LS : lambda_structure L T)(s1 s2 : sequent V L)
(n : nat)(rank : rank_sequent (S n) s2)
(x : terminal_obj_sequence V T n)
(reorder : list_reorder s1 s2),
state_seq_step_semantics LS s1 n
(iff_left (rank_sequent_list_reorder _ _ (S n) reorder) rank) x →
state_seq_step_semantics LS s2 n rank x.
Lemma state_seq_step_semantics_list_reorder_rev :
∀(LS : lambda_structure L T)(s1 s2 : sequent V L)
(n : nat)(rank : rank_sequent (S n) s1)
(x : terminal_obj_sequence V T n)
(reorder : list_reorder s1 s2),
state_seq_step_semantics LS s1 n rank x →
state_seq_step_semantics LS s2 n
(iff_right (rank_sequent_list_reorder _ _ (S n) reorder) rank) x.
Lemma state_seq_step_semantics_append :
∀(LS : lambda_structure L T)(s1 s2 : sequent V L)
(n : nat)(rank : rank_sequent (S n) (s1 ++ s2))
(x : terminal_obj_sequence V T n),
state_seq_step_semantics LS (s1 ++ s2) n rank x →
~(~state_seq_step_semantics LS s1 n
(rank_sequent_append_left _ _ _ rank) x ∧
¬state_seq_step_semantics LS s2 n
(rank_sequent_append_right _ _ _ rank) x).
Lemma state_seq_step_semantics_append_right :
∀(LS : lambda_structure L T)(s1 s2 : sequent V L)
(n : nat)(rank_s1 : rank_sequent (S n) s1)
(rank_app : rank_sequent (S n) (s1 ++ s2))
(x : terminal_obj_sequence V T n),
state_seq_step_semantics LS s1 n rank_s1 x →
state_seq_step_semantics LS (s1 ++ s2) n rank_app x.
Lemma state_seq_step_semantics_append_left :
∀(LS : lambda_structure L T)(s1 s2 : sequent V L)
(n : nat)(rank_s2 : rank_sequent (S n) s2)
(rank_app : rank_sequent (S n) (s1 ++ s2))
(x : terminal_obj_sequence V T n),
state_seq_step_semantics LS s2 n rank_s2 x →
state_seq_step_semantics LS (s1 ++ s2) n rank_app x.
Lemma state_seq_step_semantics_long_neg_intro :
∀(LS : lambda_structure L T)(s : sequent V L)
(n : nat)(rank : rank_sequent (S n) s)
(x : terminal_obj_sequence V T n),
length s ≠ 1 →
~~state_seq_step_semantics LS s n rank x →
state_seq_step_semantics LS s n rank x.
Lemma state_seq_step_form_pred_lambda_or :
∀(LS : lambda_structure L T)(n : nat)
(x : terminal_obj_sequence V T n)(f1 f2 : lambda_formula V L)
(rf1 : rank_formula (S n) f1)(rf2 : rank_formula (S n) f2),
state_seq_step_form_pred LS n x (lambda_or f1 f2)
(rank_formula_lambda_or (S n) f1 f2 rf1 rf2)
↔
~(~state_seq_step_form_pred LS n x f1 rf1 ∧
¬ state_seq_step_form_pred LS n x f2 rf2).
Lemma state_seq_step_semantics_correct :
∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
(n : nat)(rank : rank_sequent (S n) s)
(x : terminal_obj_sequence V T n),
state_seq_step_semantics LS s n rank x ↔
step_semantics_sequent nonempty_v LS s n rank x.
Definition state_seq_step_semantics_valid
(LS : lambda_structure L T)(s : sequent V L)
(n : nat)(rank : rank_sequent (S n) s) : Prop :=
∀(x : terminal_obj_sequence V T n),
state_seq_step_semantics LS s n rank x.
Lemma state_seq_step_semantics_valid_correct :
∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
(n : nat)(rank : rank_sequent (S n) s),
step_semantics_valid nonempty_v LS s n rank ↔
state_seq_step_semantics_valid LS s n rank.
Lemma step_semantics_valid_list_reorder :
∀(nonempty_v : V)(LS : lambda_structure L T)(s1 s2 : sequent V L)
(n : nat)(rank_1 : rank_sequent (S n) s1)
(rank_2 : rank_sequent (S n) s2),
list_reorder s1 s2 →
step_semantics_valid nonempty_v LS s1 n rank_1 →
step_semantics_valid nonempty_v LS s2 n rank_2.
Lemma step_semantics_valid_at_rank_list_reorder :
∀(nonempty_v : V)(LS : lambda_structure L T)(n : nat)
(s1 s2 : sequent V L),
list_reorder s1 s2 →
step_semantics_valid_at_rank nonempty_v LS n s1 →
step_semantics_valid_at_rank nonempty_v LS n s2.
Lemma step_semantics_sequent_append :
∀(nonempty_v : V)(LS : lambda_structure L T)(n : nat)
(s1 s2 : sequent V L)(rank : rank_sequent (S n) (s1 ++ s2)),
subset
(step_semantics_sequent nonempty_v LS (s1 ++ s2) n rank)
(set_inverse
(intersection
(set_inverse
(step_semantics_sequent nonempty_v LS s1 n
(rank_sequent_append_left _ _ _ rank)))
(set_inverse
(step_semantics_sequent nonempty_v LS s2 n
(rank_sequent_append_right _ _ _ rank))))).
Definition upward_step_correct_rule(nonempty_v : V)(r : sequent_rule V L)
(n : nat)(rank : rule_has_rank (S n) r) : Prop :=
∀(LS : lambda_structure L T)(x : terminal_obj_sequence V T n),
step_semantics_sequent nonempty_v LS (conclusion r) n (proj2 rank) x →
∀(i : nat)(i_less : i < length (assumptions r)),
step_semantics_sequent nonempty_v LS (nth (assumptions r) i i_less)
n (proj1 rank i i_less) x.
Lemma upward_step_correct_context :
∀(nonempty_v : V)(r : sequent_rule V L)(sl sr : sequent V L)(n : nat)
(rank_context : rule_has_rank (S n) (rule_add_context sl sr r)),
every_nth (fun(a : sequent V L) ⇒ a ≠ []) (assumptions r) →
upward_step_correct_rule nonempty_v r n
(rank_rule_add_context_rev sl sr r (S n) rank_context)
→
upward_step_correct_rule nonempty_v (rule_add_context sl sr r)
n rank_context.
Lemma upward_step_correct_ax :
∀(nonempty_v : V)(r : sequent_rule V L)
(n : nat)(rank : rule_has_rank (S n) r),
is_ax_rule r → upward_step_correct_rule nonempty_v r n rank.
Lemma upward_step_correct_and :
∀(nonempty_v : V)(r : sequent_rule V L)
(n : nat)(rank : rule_has_rank (S n) r),
is_and_rule r →
upward_step_correct_rule nonempty_v r n rank.
Lemma upward_step_correct_neg_and :
∀(nonempty_v : V)(r : sequent_rule V L)
(n : nat)(rank : rule_has_rank (S n) r),
is_neg_and_rule r →
upward_step_correct_rule nonempty_v r n rank.
Lemma upward_step_correct_neg_neg :
∀(nonempty_v : V)(r : sequent_rule V L)
(n : nat)(rank : rule_has_rank (S n) r),
classical_logic →
is_neg_neg_rule r →
upward_step_correct_rule nonempty_v r n rank.
Lemma upward_step_correct_G :
∀(nonempty_v : V)(r : sequent_rule V L)
(n : nat)(rank : rule_has_rank (S n) r),
classical_logic →
G_set V L r →
upward_step_correct_rule nonempty_v r n rank.
Lemma step_semantics_valid_G_rule_inductive :
∀(nonempty_v : V)(LS : lambda_structure L T)(n : nat),
classical_logic →
rule_inductive (G_n_set V L (S n))
(step_semantics_valid_at_rank nonempty_v LS n).
Lemma one_step_semantics_propositional :
∀(LS : lambda_structure L T)(n : nat)(f : lambda_formula V L)
(prop_f : propositional f)(rank : rank_formula (S n) f)
(x : terminal_obj_sequence V T n),
step_semantics LS f n rank x ↔
is_prop_model (terminal_obj_sequence_pi_2 n x) f prop_f.
Lemma one_step_semantics_valid_propositional :
∀(nonempty_v : V)(LS : lambda_structure L T)
(n : nat)(s : sequent V L)
(prop_s : propositional_sequent s)(rank : rank_sequent (S n) s),
non_trivial_functor T →
step_semantics_valid nonempty_v LS s n rank →
prop_valid_sequent nonempty_v s prop_s.
Lemma step_mod_sequent_semantics :
∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
(n : nat)(rank : rank_sequent (2 + n) s),
prop_modal_sequent s →
∃(mod_sem_s : set (obj T (terminal_obj_sequence V T n))),
set_equal (step_semantics_sequent nonempty_v LS s (S n) rank)
(inv_img (terminal_obj_sequence_pi_1 n) mod_sem_s).
Lemma step_prop_sequent_semantics :
∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
(n : nat)(rank : rank_sequent (S n) s),
propositional_sequent s →
∃(prop_sem_s : set (set V)),
set_equal (step_semantics_sequent nonempty_v LS s n rank)
(inv_img (terminal_obj_sequence_pi_2 n) prop_sem_s).
Definition n_step_subst_coval(LS : lambda_structure L T)
(sigma : lambda_subst V L)
(n : nat)(rank_sigma : rank_subst (S n) sigma)
: (terminal_obj_sequence V T n) → set V :=
fun(x : terminal_obj_sequence V T n)(v : V) ⇒
step_semantics LS (sigma v) n (rank_sigma v) x.
Lemma subst_coval_modal_step_semantics :
∀(LS : lambda_structure L T)(f : lambda_formula V L)
(propm_f : prop_modal_prop f)(sigma : lambda_subst V L)(n : nat)
(rank_subst_f : rank_formula (2 + n) (subst_form sigma f))
(rank_sigma : rank_subst (S n) sigma)
(sx : obj T (terminal_obj_sequence V T n))(pv : set V),
step_semantics LS (subst_form sigma f) (S n) rank_subst_f (sx, pv) ↔
prop_modal_prop_valuation LS (n_step_subst_coval LS sigma n rank_sigma)
f propm_f sx.
Lemma subst_coval_modal_step_semantics_valid :
∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
(nonempty_s : s ≠ [])(propm_s : prop_modal_prop_sequent s)
(sigma : lambda_subst V L)
(n : nat)
(rank_subst_s : rank_sequent (2 + n) (subst_sequent sigma s))
(rank_sigma : rank_subst (S n) sigma),
step_semantics_valid nonempty_v LS (subst_sequent sigma s)
(S n) rank_subst_s
↔
mod_seq_val_valid LS (n_step_subst_coval LS sigma n rank_sigma)
s nonempty_s propm_s.
Lemma scssv_4_13_nonempty_tcc :
∀(s simple_s : sequent V L)
(sigma : lambda_subst V L),
s ≠ [] →
subst_sequent sigma simple_s = s →
simple_s ≠ [].
Lemma subst_coval_modal_step_semantics_valid_for_4_13 :
∀(nonempty_v : V)(LS : lambda_structure L T)
(s simple_s : sequent V L)
(nonempty_s : s ≠ [])
(simple_simple_s : simple_modal_sequent simple_s)
(n : nat)
(rank : rank_sequent (2 + n) s)
(sigma : lambda_subst V L)
(rank_sigma : rank_subst (S n) sigma)
(s_subst_eq : subst_sequent sigma simple_s = s),
step_semantics_valid nonempty_v LS s (S n) rank →
mod_seq_val_valid LS (n_step_subst_coval LS sigma n rank_sigma)
simple_s (scssv_4_13_nonempty_tcc _ _ _ nonempty_s s_subst_eq)
(simple_modal_sequent_is_prop_modal_prop _ simple_simple_s).
Lemma subst_coval_prop_step_semantics :
∀(LS : lambda_structure L T)(f : lambda_formula V L)
(prop_f : propositional f)(sigma : lambda_subst V L)(n : nat)
(rank_subst_f : rank_formula (S n) (subst_form sigma f))
(rank_sigma : rank_subst (S n) sigma),
set_equal
(step_semantics LS (subst_form sigma f) n rank_subst_f)
(propositional_valuation (n_step_subst_coval LS sigma n rank_sigma)
f prop_f).
Lemma subst_coval_prop_step_semantics_valid :
∀(nonempty_v : V)(LS : lambda_structure L T)(s : sequent V L)
(prop_s : propositional_sequent s)
(sigma : lambda_subst V L)
(n : nat)
(rank_subst_s : rank_sequent (S n) (subst_sequent sigma s))
(rank_sigma : rank_subst (S n) sigma),
prop_seq_val_valid nonempty_v
(n_step_subst_coval LS sigma n rank_sigma) s prop_s →
step_semantics_valid nonempty_v LS (subst_sequent sigma s)
n rank_subst_s.
End Step_semantics.
Implicit Arguments step_semantics_valid [V L T].
Implicit Arguments slice_model [V T].
Implicit Arguments nth_unit_model [V T].
Implicit Arguments step_semantics_valid_nonempty [V L T].
Implicit Arguments step_semantics_valid_at_rank [V L T].
Implicit Arguments step_semantics_valid_G_rule_inductive [V L T].
Implicit Arguments step_mod_sequent_semantics [V L T].
Implicit Arguments step_prop_sequent_semantics [V L T].
Implicit Arguments n_step_subst_coval [V L T].
Implicit Arguments subst_coval_modal_step_semantics_valid_for_4_13 [V L T].