Context-Sensitive Derivation Toolbox

This file provides elementary lemmas for context-sensitive derivations.

Main declarations

• CS_deri_self
• CS_deri_of_deri_deri
• CS_tran_or_id_of_deri

theorem CS_deri_self {T : Type} {g : CS_grammar T} {w : List (symbol T g.nt)} : CS_derives g w w

The Relation CS_derives is reflexive.

theorem CS_deri_of_tran {T : Type} {g : CS_grammar T} {v w : List (symbol T g.nt)} : CS_transforms g v w → CS_derives g v w

theorem CS_deri_of_deri_deri {T : Type} {g : CS_grammar T} {u v w : List (symbol T g.nt)} (huv : CS_derives g u v) (hvw : CS_derives g v w) : CS_derives g u w

The Relation CS_derives is transitive.

theorem CS_deri_of_deri_tran {T : Type} {g : CS_grammar T} {u v w : List (symbol T g.nt)} (huv : CS_derives g u v) (hvw : CS_transforms g v w) : CS_derives g u w

theorem CS_deri_of_tran_deri {T : Type} {g : CS_grammar T} {u v w : List (symbol T g.nt)} (huv : CS_transforms g u v) (hvw : CS_derives g v w) : CS_derives g u w

theorem CS_tran_or_id_of_deri {T : Type} {g : CS_grammar T} {u w : List (symbol T g.nt)} (ass : CS_derives g u w) : u = w ∨ ∃ (v : List (symbol T g.nt)), CS_transforms g u v ∧ CS_derives g v w