Non-Contracting and Context-Sensitive

This file contains class-level comparison results between non-contracting grammars and context-sensitive grammars.

main results

• is_noncontracting_implies_is_CS — every non-contracting language is context-sensitive
• CS_is_noncontracting — every CS grammar induces a non-contracting unrestricted grammar
• noncontracting_transforms_length_le — non-contracting steps don't decrease length
• csg_of_noncontracting — translate a non-contracting grammar into a context-sensitive grammar
• grammar_language_subset_csg_of_noncontracting — forward correctness of the translation

theorem CS_is_noncontracting {T : Type} (g : CS_grammar T) : grammar_noncontracting (grammar_of_csg g)

The unrestricted grammar obtained from a context-sensitive grammar (via grammar_of_csg) is non-contracting.

theorem is_noncontracting_implies_is_CS {T : Type} {L : Language T} (h : is_noncontracting L) : is_CS L

Every non-contracting language is context-sensitive in the broader definition.

theorem noncontracting_transforms_length_le {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {w₁ w₂ : List (symbol T g.nt)} (h : grammar_transforms g w₁ w₂) : w₁.length ≤ w₂.length

A single transformation step in a non-contracting grammar does not decrease the length of the sentential form.

Non-contracting → CS

The conversion from a non-contracting grammar to a context-sensitive grammar is a classical construction. Given a non-contracting rule L ++ [A] ++ R → output with |output| ≥ |L| + 1 + |R|, we simulate it using context-sensitive rules with fresh auxiliary nonterminals.

Construction

The nonterminal type of the constructed CS grammar is g.nt ⊕ (T ⊕ (ℕ × ℕ)):

• Sum.inl n: original nonterminal n
• Sum.inr (Sum.inl t): a "lifted" nonterminal representing terminal t
• Sum.inr (Sum.inr (i, j)): auxiliary nonterminal for rule index i, step j

The sentential forms in the CS grammar always consist entirely of nonterminals (either Sum.inl n or Sum.inr (Sum.inl t)), except at the very end when un-lifting rules convert Sum.inr (Sum.inl t) to terminal t.

The rules are:

1. Un-lifting rules: Sum.inr (Sum.inl t) → [terminal t]
2. Direct rules (n = 1): Sum.inl A → map liftSym output
3. Phase 1 (n ≥ 2, marking): Replace pattern symbols with auxiliaries left-to-right
4. Phase 2 (n ≥ 2, output): Replace auxiliaries with output symbols right-to-left

@[reducible, inline]

abbrev NC_NT {T : Type} (g : grammar T) : Type

Nonterminal type for the CS grammar constructed from a non-contracting grammar.

Equations

• NC_NT g = (g.nt ⊕ T ⊕ ℕ × ℕ)

def nc_symToNT {T : Type} {g : grammar T} : symbol T g.nt → NC_NT g

Convert a symbol to a nonterminal in the new grammar (lifting terminals).

Equations

• nc_symToNT (symbol.terminal t) = Sum.inr (Sum.inl t)
• nc_symToNT (symbol.nonterminal n) = Sum.inl n

def nc_liftSym {T : Type} {g : grammar T} (s : symbol T g.nt) : symbol T (NC_NT g)

Lift a symbol: all symbols become nonterminal symbols in the new grammar.

Equations

• nc_liftSym s = symbol.nonterminal (nc_symToNT s)

def nc_aux {T : Type} {g : grammar T} (ri k : ℕ) : symbol T (NC_NT g)

Auxiliary nonterminal symbol for rule index ri, step k.

Equations

• nc_aux ri k = symbol.nonterminal (Sum.inr (Sum.inr (ri, k)))

def nc_collectTerminals {T N : Type} : List (symbol T N) → List T

Collect all terminals from a list of symbols.

Equations

• nc_collectTerminals [] = []
• nc_collectTerminals (symbol.terminal t :: rest) = t :: nc_collectTerminals rest
• nc_collectTerminals (symbol.nonterminal a :: rest) = nc_collectTerminals rest

def nc_grammarTerminals {T : Type} (g : grammar T) : List T

All terminals appearing in the grammar's rules (inputs and outputs).

Equations

• nc_grammarTerminals g = List.flatMap (fun (r : grule T g.nt) => nc_collectTerminals (r.input_L ++ r.input_R ++ r.output_string)) g.rules

def nc_unliftRules {T : Type} (g : grammar T) : List (csrule T (NC_NT g))

Un-lifting rules: convert lifted terminal nonterminals back to actual terminals.

Equations

• One or more equations did not get rendered due to their size.

def nc_simRules {T : Type} {g : grammar T} (ri : ℕ) (r : grule T g.nt) : List (csrule T (NC_NT g))

Generate CS rules for simulating one grammar rule at index ri.

Equations

• One or more equations did not get rendered due to their size.

def nc_allRules {T : Type} (g : grammar T) : List (csrule T (NC_NT g))

All CS rules: un-lifting rules plus simulation rules for each grammar rule.

Equations

• nc_allRules g = nc_unliftRules g ++ List.flatMap (fun (x : ℕ × grule T g.nt) => match x with | (i, r) => nc_simRules i r) ((List.range g.rules.length).zip g.rules)

theorem nc_unliftRules_output_nonempty {T : Type} (g : grammar T) (r : csrule T (NC_NT g)) (hr : r ∈ nc_unliftRules g) : r.output_string ≠ []

Every rule in nc_unliftRules has nonempty output.

theorem nc_simRules_output_nonempty {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (ri : ℕ) (grule : grule T g.nt) (hgrule : grule ∈ g.rules) (r : csrule T (NC_NT g)) (hr : r ∈ nc_simRules ri grule) : r.output_string ≠ []

Every rule in nc_simRules has nonempty output, provided the non-contracting property.

noncomputable def csg_of_noncontracting {T : Type} (g : grammar T) (hg : grammar_noncontracting g) : CS_grammar T

Construct a context-sensitive grammar equivalent to a given non-contracting grammar.

Equations

• csg_of_noncontracting g hg = { nt := NC_NT g, initial := Sum.inl g.initial, rules := nc_allRules g, output_nonempty := ⋯ }

Helper lemmas for language equivalence

theorem CS_deri_with_context {T : Type} {g : CS_grammar T} {w₁ w₂ : List (symbol T g.nt)} (p s : List (symbol T g.nt)) (h : CS_derives g w₁ w₂) : CS_derives g (p ++ w₁ ++ s) (p ++ w₂ ++ s)

theorem CS_transform_removed_symbol_is_input_general {T : Type} {g : CS_grammar T} {s₁ s₂ : List (symbol T g.nt)} {x : symbol T g.nt} (h : CS_transforms g s₁ s₂) (hx₁ : x ∈ s₁) (hx₂ : x ∉ s₂) : ∃ r ∈ g.rules, x = symbol.nonterminal r.input_nonterminal

theorem CS_transform_removed_symbol_actual_input {T : Type} {g : CS_grammar T} {s₁ s₂ : List (symbol T g.nt)} {x : symbol T g.nt} (h : CS_transforms g s₁ s₂) (hx₁ : x ∈ s₁) (hx₂ : x ∉ s₂) : ∃ (r : csrule T g.nt) (u : List (symbol T g.nt)) (v : List (symbol T g.nt)), r ∈ g.rules ∧ s₁ = u ++ r.context_left ++ [x] ++ r.context_right ++ v ∧ s₂ = u ++ r.context_left ++ r.output_string ++ r.context_right ++ v ∧ x = symbol.nonterminal r.input_nonterminal

theorem CS_transform_removed_symbol_is_input_with_output_mem {T : Type} {g : CS_grammar T} {s₁ s₂ : List (symbol T g.nt)} {x : symbol T g.nt} (h : CS_transforms g s₁ s₂) (hx₁ : x ∈ s₁) (hx₂ : x ∉ s₂) : ∃ r ∈ g.rules, x = symbol.nonterminal r.input_nonterminal ∧ ∀ y ∈ r.output_string, y ∈ s₂

theorem CS_transform_added_symbol_is_output_general {T : Type} {g : CS_grammar T} {s₁ s₂ : List (symbol T g.nt)} {x : symbol T g.nt} (h : CS_transforms g s₁ s₂) (hx₂ : x ∈ s₂) (hx₁ : x ∉ s₁) : ∃ r ∈ g.rules, x ∈ r.output_string

theorem CS_transform_added_symbol_is_output_with_input_mem {T : Type} {g : CS_grammar T} {s₁ s₂ : List (symbol T g.nt)} {x : symbol T g.nt} (h : CS_transforms g s₁ s₂) (hx₂ : x ∈ s₂) (hx₁ : x ∉ s₁) : ∃ r ∈ g.rules, x ∈ r.output_string ∧ symbol.nonterminal r.input_nonterminal ∈ s₁

theorem nc_unlift_one {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (t : T) (ht : t ∈ nc_grammarTerminals g) (u v : List (symbol T (NC_NT g))) : CS_transforms (csg_of_noncontracting g hg) (u ++ [symbol.nonterminal (Sum.inr (Sum.inl t))] ++ v) (u ++ [symbol.terminal t] ++ v)

theorem nc_unlift_all {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (w : List T) (hw : ∀ t ∈ w, t ∈ nc_grammarTerminals g) : CS_derives (csg_of_noncontracting g hg) (List.map (fun (t : T) => symbol.nonterminal (Sum.inr (Sum.inl t))) w) (List.map symbol.terminal w)

theorem terminal_in_output_mem_grammarTerminals {T : Type} (g : grammar T) (r : grule T g.nt) (hr : r ∈ g.rules) (t : T) (ht : symbol.terminal t ∈ r.output_string) : t ∈ nc_grammarTerminals g

theorem nc_simRule_mem {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (ri : ℕ) (r : grule T g.nt) (hri : ri < g.rules.length) (hr : g.rules[ri] = r) (cr : csrule T (NC_NT g)) (hcr : cr ∈ nc_simRules ri r) : cr ∈ (csg_of_noncontracting g hg).rules

theorem nc_rule_zip_mem_get {T : Type} (g : grammar T) {ri : ℕ} {r : grule T g.nt} (hpair : (ri, r) ∈ (List.range g.rules.length).zip g.rules) : ∃ (hri : ri < g.rules.length), g.rules[ri] = r

Membership in the zipped rule-index list recovers the indexed rule.

theorem nc_rule_zip_rule_unique {T : Type} (g : grammar T) {ri : ℕ} {r₁ r₂ : grule T g.nt} (h₁ : (ri, r₁) ∈ (List.range g.rules.length).zip g.rules) (h₂ : (ri, r₂) ∈ (List.range g.rules.length).zip g.rules) : r₁ = r₂

The rule component for a fixed simulation-rule index is unique.

theorem list_append_singleton_eq_of_not_mem {α : Type} {x : α} {a b c d : List α} (ha : x ∉ a) (hc : x ∉ c) (h : a ++ [x] ++ b = c ++ [x] ++ d) : a = c ∧ b = d

A list decomposition around the first occurrence of a marker is unique.

theorem list_prefix_not_mem_of_unique_singleton_decomp {α : Type} {x : α} {u w a b : List α} (hu : x ∉ u) (hw : x ∉ w) (h : u ++ [x] ++ w = a ++ [x] ++ b) : x ∉ a

If u ++ [x] ++ w has no x in u or w, then any decomposition of the same list as a ++ [x] ++ b has no x in a.

theorem nc_sim_pattern {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (ri : ℕ) (r : grule T g.nt) (hri : ri < g.rules.length) (hr : g.rules[ri] = r) : CS_derives (csg_of_noncontracting g hg) (List.map nc_liftSym (r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R)) (List.map nc_liftSym r.output_string)

theorem nc_sim_one_transform {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {w₁ w₂ : List (symbol T g.nt)} (h : grammar_transforms g w₁ w₂) : CS_derives (csg_of_noncontracting g hg) (List.map nc_liftSym w₁) (List.map nc_liftSym w₂)

A single grammar step can be simulated by CS derivation on lifted forms.

theorem nc_sim_derives {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {w₁ w₂ : List (symbol T g.nt)} (h : grammar_derives g w₁ w₂) : CS_derives (csg_of_noncontracting g hg) (List.map nc_liftSym w₁) (List.map nc_liftSym w₂)

theorem nc_derived_terminal_in_grammarTerminals {T : Type} (g : grammar T) (w : List T) (hw : w ∈ grammar_language g) (t : T) (ht : t ∈ w) : t ∈ nc_grammarTerminals g

theorem nc_forward {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (w : List T) (hw : w ∈ grammar_language g) : w ∈ CS_language (csg_of_noncontracting g hg)

theorem grammar_language_subset_csg_of_noncontracting {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (w : List T) : w ∈ grammar_language g → w ∈ CS_language (csg_of_noncontracting g hg)

Forward correctness of the non-contracting-to-CS construction.

Every terminal word generated by the original non-contracting unrestricted grammar is generated by the constructed context-sensitive grammar. The reverse containment is the remaining hard direction because derivations in the constructed grammar may pass through auxiliary nonterminals before returning to clean sentential forms.

Locked non-contracting → CS construction

The first construction above is convenient for forward simulation, but its phase-2 cleanup rules use clean output symbols as right context. That is too permissive for the reverse direction: a cleanup rule can match symbols from the surrounding sentential context and skip the locked output phase. The locked construction below uses fresh output markers for every produced output position, and only erases those markers to clean lifted symbols after the simulated rule has completed.

inductive NC_LockedNT {T : Type} (g : grammar T) : Type

Nonterminals for the locked CS construction.

• orig {T : Type} {g : grammar T} : g.nt → NC_LockedNT g
• term {T : Type} {g : grammar T} : T → NC_LockedNT g
• mark {T : Type} {g : grammar T} : ℕ → ℕ → NC_LockedNT g
• out {T : Type} {g : grammar T} : ℕ → ℕ → symbol T g.nt → NC_LockedNT g

def nc_locked_symToNT {T : Type} {g : grammar T} : symbol T g.nt → NC_LockedNT g

Convert an original symbol to a locked-construction nonterminal.

Equations

• nc_locked_symToNT (symbol.terminal t) = NC_LockedNT.term t
• nc_locked_symToNT (symbol.nonterminal n) = NC_LockedNT.orig n

theorem nc_locked_symToNT_ne_mark {T : Type} {g : grammar T} (s : symbol T g.nt) (ri k : ℕ) : nc_locked_symToNT s ≠ NC_LockedNT.mark ri k

theorem nc_locked_symToNT_ne_out {T : Type} {g : grammar T} (s : symbol T g.nt) (ri k : ℕ) (a : symbol T g.nt) : nc_locked_symToNT s ≠ NC_LockedNT.out ri k a

def nc_locked_liftSym {T : Type} {g : grammar T} (s : symbol T g.nt) : symbol T (NC_LockedNT g)

Lift an original symbol into the locked construction.

Equations

• nc_locked_liftSym s = symbol.nonterminal (nc_locked_symToNT s)

def nc_locked_mark {T : Type} {g : grammar T} (ri k : ℕ) : symbol T (NC_LockedNT g)

Input-position marker for a simulated rule.

Equations

• nc_locked_mark ri k = symbol.nonterminal (NC_LockedNT.mark ri k)

def nc_locked_out {T : Type} {g : grammar T} (ri k : ℕ) (s : symbol T g.nt) : symbol T (NC_LockedNT g)

Output-position marker for a simulated rule.

Equations

• nc_locked_out ri k s = symbol.nonterminal (NC_LockedNT.out ri k s)

def nc_locked_outputSuffix {T : Type} {g : grammar T} (ri : ℕ) (out : List (symbol T g.nt)) (dflt : symbol T g.nt) (k : ℕ) : List (symbol T (NC_LockedNT g))

Marked output suffix beginning at position k.

Equations

• nc_locked_outputSuffix ri out dflt k = List.map (fun (off : ℕ) => nc_locked_out ri (k + off) (out.getD (k + off) dflt)) (List.range (out.length - k))

def nc_locked_outputFrom {T : Type} {g : grammar T} (ri : ℕ) (out : List (symbol T g.nt)) (dflt : symbol T g.nt) (k : ℕ) : List (symbol T (NC_LockedNT g))

Marked output suffix beginning at position k, forced syntactically nonempty. For non-contracting rules the head index is in bounds; the default only keeps the definition total.

Equations

• nc_locked_outputFrom ri out dflt k = nc_locked_out ri k (out.getD k dflt) :: nc_locked_outputSuffix ri out dflt (k + 1)

def nc_locked_unliftRules {T : Type} (g : grammar T) : List (csrule T (NC_LockedNT g))

Un-lifting rules for the locked construction.

Equations

• One or more equations did not get rendered due to their size.

def nc_locked_simRules {T : Type} {g : grammar T} (ri : ℕ) (r : grule T g.nt) : List (csrule T (NC_LockedNT g))

Simulation rules for one original non-contracting rule in the locked construction.

Equations

• One or more equations did not get rendered due to their size.

def nc_locked_allRules {T : Type} (g : grammar T) : List (csrule T (NC_LockedNT g))

All locked-construction CS rules.

Equations

• One or more equations did not get rendered due to their size.

theorem nc_locked_unliftRules_output_nonempty {T : Type} (g : grammar T) (r : csrule T (NC_LockedNT g)) (hr : r ∈ nc_locked_unliftRules g) : r.output_string ≠ []

theorem nc_locked_simRules_output_nonempty {T : Type} (g : grammar T) (ri : ℕ) (grule : grule T g.nt) (r : csrule T (NC_LockedNT g)) (hr : r ∈ nc_locked_simRules ri grule) : r.output_string ≠ []

noncomputable def locked_csg_of_noncontracting {T : Type} (g : grammar T) (_hg : grammar_noncontracting g) : CS_grammar T

Locked CS grammar for a non-contracting grammar.

Equations

• locked_csg_of_noncontracting g _hg = { nt := NC_LockedNT g, initial := NC_LockedNT.orig g.initial, rules := nc_locked_allRules g, output_nonempty := ⋯ }

theorem nc_locked_simRule_mem {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (ri : ℕ) (r : grule T g.nt) (hri : ri < g.rules.length) (hr : g.rules[ri] = r) (cr : csrule T (NC_LockedNT g)) (hcr : cr ∈ nc_locked_simRules ri r) : cr ∈ (locked_csg_of_noncontracting g hg).rules

A locked simulation rule is a rule of the locked constructed CS grammar.

theorem nc_locked_unliftRule_mem {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {t : T} (ht : t ∈ nc_grammarTerminals g) : { context_left := [], input_nonterminal := NC_LockedNT.term t, context_right := [], output_string := [symbol.terminal t] } ∈ (locked_csg_of_noncontracting g hg).rules

An un-lifting rule is a rule of the locked constructed CS grammar.

theorem nc_locked_unlift_one {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (t : T) (ht : t ∈ nc_grammarTerminals g) (u v : List (symbol T (NC_LockedNT g))) : CS_transforms (locked_csg_of_noncontracting g hg) (u ++ [symbol.nonterminal (NC_LockedNT.term t)] ++ v) (u ++ [symbol.terminal t] ++ v)

Un-lift one locked terminal marker to the actual terminal.

theorem nc_locked_unlift_all {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (w : List T) (hw : ∀ t ∈ w, t ∈ nc_grammarTerminals g) : CS_derives (locked_csg_of_noncontracting g hg) (List.map (fun (t : T) => symbol.nonterminal (NC_LockedNT.term t)) w) (List.map symbol.terminal w)

Un-lift all locked terminal markers in a terminal word.

theorem nc_locked_cleanup_one {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (ri : ℕ) (r : grule T g.nt) (hri : ri < g.rules.length) (hr : g.rules[ri] = r) (j : ℕ) (hj : j < r.output_string.length) (u v : List (symbol T (NC_LockedNT g))) : CS_transforms (locked_csg_of_noncontracting g hg) (u ++ [nc_locked_out ri j (r.output_string.getD j (symbol.nonterminal r.input_N))] ++ v) (u ++ [nc_locked_liftSym (r.output_string.getD j (symbol.nonterminal r.input_N))] ++ v)

Clean up one locked output marker into the corresponding lifted output symbol.

theorem nc_locked_outputSuffix_nil_of_len_le {T : Type} (g : grammar T) (ri : ℕ) (out : List (symbol T g.nt)) (dflt : symbol T g.nt) (k : ℕ) (hk : out.length ≤ k) : nc_locked_outputSuffix ri out dflt k = []

theorem nc_locked_outputSuffix_cons {T : Type} (g : grammar T) (ri : ℕ) (out : List (symbol T g.nt)) (dflt : symbol T g.nt) (k : ℕ) (hk : k < out.length) : nc_locked_outputSuffix ri out dflt k = [nc_locked_out ri k (out.getD k dflt)] ++ nc_locked_outputSuffix ri out dflt (k + 1)

theorem nc_locked_outputFrom_eq_suffix {T : Type} (g : grammar T) (ri : ℕ) (out : List (symbol T g.nt)) (dflt : symbol T g.nt) (k : ℕ) (hk : k < out.length) : nc_locked_outputFrom ri out dflt k = nc_locked_outputSuffix ri out dflt k

theorem nc_locked_outputSuffix_mem_out_shape {T : Type} (g : grammar T) {ri ri' k k' : ℕ} {out : List (symbol T g.nt)} {dflt a : symbol T g.nt} (hmem : nc_locked_out ri' k' a ∈ nc_locked_outputSuffix ri out dflt k) : ri' = ri ∧ k ≤ k' ∧ k' < out.length ∧ a = out.getD k' dflt

theorem nc_locked_outputFrom_mem_out_shape {T : Type} (g : grammar T) {ri ri' k k' : ℕ} {out : List (symbol T g.nt)} {dflt a : symbol T g.nt} (hk : k < out.length) (hmem : nc_locked_out ri' k' a ∈ nc_locked_outputFrom ri out dflt k) : ri' = ri ∧ k ≤ k' ∧ k' < out.length ∧ a = out.getD k' dflt

theorem nc_locked_outputSuffix_head_mem {T : Type} (g : grammar T) (ri : ℕ) (out : List (symbol T g.nt)) (dflt : symbol T g.nt) (k : ℕ) (hk : k < out.length) : nc_locked_out ri k (out.getD k dflt) ∈ nc_locked_outputSuffix ri out dflt k

theorem nc_locked_take_succ_map {T : Type} (g : grammar T) (out : List (symbol T g.nt)) (dflt : symbol T g.nt) (k : ℕ) (hk : k < out.length) : List.map nc_locked_liftSym (List.take (k + 1) out) = List.map nc_locked_liftSym (List.take k out) ++ [nc_locked_liftSym (out.getD k dflt)]

theorem nc_locked_cleanup_suffix {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (ri : ℕ) (r : grule T g.nt) (hri : ri < g.rules.length) (hr : g.rules[ri] = r) (k : ℕ) (hk : k ≤ r.output_string.length) : CS_derives (locked_csg_of_noncontracting g hg) (List.map nc_locked_liftSym (List.take k r.output_string) ++ nc_locked_outputSuffix ri r.output_string (symbol.nonterminal r.input_N) k) (List.map nc_locked_liftSym r.output_string)

theorem nc_locked_cleanup_outputFrom_with_context {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {ri : ℕ} {r : grule T g.nt} (hpair : (ri, r) ∈ (List.range g.rules.length).zip g.rules) (u v : List (symbol T (NC_LockedNT g))) : CS_derives (locked_csg_of_noncontracting g hg) (u ++ nc_locked_outputFrom ri r.output_string (symbol.nonterminal r.input_N) 0 ++ v) (u ++ List.map nc_locked_liftSym r.output_string ++ v)

theorem nc_locked_sim_pattern {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (ri : ℕ) (r : grule T g.nt) (hri : ri < g.rules.length) (hr : g.rules[ri] = r) : CS_derives (locked_csg_of_noncontracting g hg) (List.map nc_locked_liftSym (r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R)) (List.map nc_locked_liftSym r.output_string)

theorem nc_locked_sim_one_transform {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {w₁ w₂ : List (symbol T g.nt)} (h : grammar_transforms g w₁ w₂) : CS_derives (locked_csg_of_noncontracting g hg) (List.map nc_locked_liftSym w₁) (List.map nc_locked_liftSym w₂)

theorem nc_locked_sim_derives {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {w₁ w₂ : List (symbol T g.nt)} (h : grammar_derives g w₁ w₂) : CS_derives (locked_csg_of_noncontracting g hg) (List.map nc_locked_liftSym w₁) (List.map nc_locked_liftSym w₂)

theorem nc_locked_forward {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (w : List T) (hw : w ∈ grammar_language g) : w ∈ CS_language (locked_csg_of_noncontracting g hg)

theorem grammar_language_subset_locked_csg_of_noncontracting {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (w : List T) : w ∈ grammar_language g → w ∈ CS_language (locked_csg_of_noncontracting g hg)

Forward correctness of the locked non-contracting-to-CS construction.

def nc_locked_proj_sym {T : Type} (g : grammar T) : symbol T (NC_LockedNT g) → symbol T g.nt

Projection from locked-construction symbols back to original grammar symbols.

Equations

• nc_locked_proj_sym g (symbol.terminal t) = symbol.terminal t
• nc_locked_proj_sym g (symbol.nonterminal (NC_LockedNT.orig n)) = symbol.nonterminal n
• nc_locked_proj_sym g (symbol.nonterminal (NC_LockedNT.term t)) = symbol.terminal t
• nc_locked_proj_sym g (symbol.nonterminal (NC_LockedNT.mark a a_1)) = symbol.nonterminal g.initial
• nc_locked_proj_sym g (symbol.nonterminal (NC_LockedNT.out a a_1 a_2)) = symbol.nonterminal g.initial

def nc_locked_proj {T : Type} (g : grammar T) (s : List (symbol T (NC_LockedNT g))) : List (symbol T g.nt)

Project a locked-construction sentential form back to original grammar symbols.

Equations

• nc_locked_proj g s = List.map (nc_locked_proj_sym g) s

theorem nc_locked_proj_liftSym {T : Type} (g : grammar T) (s : symbol T g.nt) : nc_locked_proj_sym g (nc_locked_liftSym s) = s

theorem nc_locked_proj_initial {T : Type} (g : grammar T) : nc_locked_proj g [symbol.nonterminal (NC_LockedNT.orig g.initial)] = [symbol.nonterminal g.initial]

theorem nc_locked_proj_terminal {T : Type} (g : grammar T) (w : List T) : nc_locked_proj g (List.map symbol.terminal w) = List.map symbol.terminal w

def nc_locked_is_clean {T : Type} (g : grammar T) (s : List (symbol T (NC_LockedNT g))) : Prop

A locked sentential form is clean if it contains no input or output markers.

Equations

• nc_locked_is_clean g s = ∀ x ∈ s, (∀ (ri k : ℕ), x ≠ symbol.nonterminal (NC_LockedNT.mark ri k)) ∧ ∀ (ri k : ℕ) (a : symbol T g.nt), x ≠ symbol.nonterminal (NC_LockedNT.out ri k a)

theorem nc_locked_initial_clean {T : Type} (g : grammar T) : nc_locked_is_clean g [symbol.nonterminal (NC_LockedNT.orig g.initial)]

theorem nc_locked_terminal_clean {T : Type} (g : grammar T) (w : List T) : nc_locked_is_clean g (List.map symbol.terminal w)

theorem nc_locked_liftSym_clean {T : Type} (g : grammar T) (s : symbol T g.nt) : nc_locked_is_clean g [nc_locked_liftSym s]

theorem nc_locked_map_liftSym_clean {T : Type} (g : grammar T) (s : List (symbol T g.nt)) : nc_locked_is_clean g (List.map nc_locked_liftSym s)

theorem nc_locked_is_clean_of_subset {T : Type} (g : grammar T) {s t : List (symbol T (NC_LockedNT g))} (hclean : nc_locked_is_clean g t) (hsub : ∀ x ∈ s, x ∈ t) : nc_locked_is_clean g s

theorem nc_locked_is_clean_append {T : Type} (g : grammar T) {s t : List (symbol T (NC_LockedNT g))} (hs : nc_locked_is_clean g s) (ht : nc_locked_is_clean g t) : nc_locked_is_clean g (s ++ t)

theorem nc_locked_not_clean_iff_exists_marker {T : Type} (g : grammar T) (s : List (symbol T (NC_LockedNT g))) : ¬nc_locked_is_clean g s ↔ (∃ (ri : ℕ) (k : ℕ), nc_locked_mark ri k ∈ s) ∨ ∃ (ri : ℕ) (k : ℕ) (a : symbol T g.nt), nc_locked_out ri k a ∈ s

theorem nc_locked_clean_step_proj_eq {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) (hclean₁ : nc_locked_is_clean g s₁) (hclean₂ : nc_locked_is_clean g s₂) : nc_locked_proj g s₁ = nc_locked_proj g s₂

theorem nc_locked_clean_step_grammar_derives {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) (hclean₁ : nc_locked_is_clean g s₁) (hclean₂ : nc_locked_is_clean g s₂) : grammar_derives g (nc_locked_proj g s₁) (nc_locked_proj g s₂)

theorem nc_locked_clean_step_dirty_mark_zero_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) (hclean : nc_locked_is_clean g s₁) (hdirty : ¬nc_locked_is_clean g s₂) : ∃ (simRi : ℕ) (grule : grule T g.nt) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; have dflt := symbol.nonterminal grule.input_N; s₁ = u ++ [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v ∧ s₂ = u ++ [nc_locked_mark simRi 0] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v

theorem nc_locked_dirty_step_clean_cleanup_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) (hdirty : ¬nc_locked_is_clean g s₁) (hclean : nc_locked_is_clean g s₂) : ∃ (simRi : ℕ) (grule : grule T g.nt) (k : ℕ) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ k < grule.output_string.length ∧ have dflt := symbol.nonterminal grule.input_N; s₁ = u ++ [nc_locked_out simRi k (grule.output_string.getD k dflt)] ++ v ∧ s₂ = u ++ [nc_locked_liftSym (grule.output_string.getD k dflt)] ++ v

theorem nc_locked_rule_mem_cases {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {cr : csrule T (NC_LockedNT g)} (hcr : cr ∈ (locked_csg_of_noncontracting g hg).rules) : (∃ t ∈ nc_grammarTerminals g, cr = { context_left := [], input_nonterminal := NC_LockedNT.term t, context_right := [], output_string := [symbol.terminal t] }) ∨ ∃ (simRi : ℕ) (grule : grule T g.nt), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; have dflt := symbol.nonterminal grule.input_N; (∃ k < pattern.length, cr = { context_left := List.map (nc_locked_mark simRi) (List.range k), input_nonterminal := nc_locked_symToNT (pattern.getD k dflt), context_right := List.map nc_locked_liftSym (List.drop (k + 1) pattern), output_string := [nc_locked_mark simRi k] }) ∨ cr = { context_left := List.map (nc_locked_mark simRi) (List.range (pattern.length - 1)), input_nonterminal := NC_LockedNT.mark simRi (pattern.length - 1), context_right := [], output_string := nc_locked_outputFrom simRi grule.output_string dflt (pattern.length - 1) } ∨ (∃ k < pattern.length - 1, cr = { context_left := List.map (nc_locked_mark simRi) (List.range k), input_nonterminal := NC_LockedNT.mark simRi k, context_right := nc_locked_outputSuffix simRi grule.output_string dflt (k + 1), output_string := [nc_locked_out simRi k (grule.output_string.getD k dflt)] }) ∨ ∃ k < grule.output_string.length, cr = { context_left := [], input_nonterminal := NC_LockedNT.out simRi k (grule.output_string.getD k dflt), context_right := [], output_string := [nc_locked_liftSym (grule.output_string.getD k dflt)] }

theorem nc_locked_rule_input_mark_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {cr : csrule T (NC_LockedNT g)} (hcr : cr ∈ (locked_csg_of_noncontracting g hg).rules) {ri k : ℕ} (hinput : cr.input_nonterminal = NC_LockedNT.mark ri k) : ∃ (simRi : ℕ) (grule : grule T g.nt), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; have dflt := symbol.nonterminal grule.input_N; k = pattern.length - 1 ∧ cr = { context_left := List.map (nc_locked_mark simRi) (List.range (pattern.length - 1)), input_nonterminal := NC_LockedNT.mark simRi (pattern.length - 1), context_right := [], output_string := nc_locked_outputFrom simRi grule.output_string dflt (pattern.length - 1) } ∨ k < pattern.length - 1 ∧ cr = { context_left := List.map (nc_locked_mark simRi) (List.range k), input_nonterminal := NC_LockedNT.mark simRi k, context_right := nc_locked_outputSuffix simRi grule.output_string dflt (k + 1), output_string := [nc_locked_out simRi k (grule.output_string.getD k dflt)] }

theorem nc_locked_rule_input_out_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {cr : csrule T (NC_LockedNT g)} (hcr : cr ∈ (locked_csg_of_noncontracting g hg).rules) {ri k : ℕ} {a : symbol T g.nt} (hinput : cr.input_nonterminal = NC_LockedNT.out ri k a) : ∃ (simRi : ℕ) (grule : grule T g.nt), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ k < grule.output_string.length ∧ a = grule.output_string.getD k (symbol.nonterminal grule.input_N) ∧ cr = { context_left := [], input_nonterminal := NC_LockedNT.out simRi k (grule.output_string.getD k (symbol.nonterminal grule.input_N)), context_right := [], output_string := [nc_locked_liftSym (grule.output_string.getD k (symbol.nonterminal grule.input_N))] }

theorem nc_locked_rule_output_mark_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {cr : csrule T (NC_LockedNT g)} (hcr : cr ∈ (locked_csg_of_noncontracting g hg).rules) {ri k : ℕ} (hout : nc_locked_mark ri k ∈ cr.output_string) : ∃ (simRi : ℕ) (grule : grule T g.nt), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; have dflt := symbol.nonterminal grule.input_N; k < pattern.length ∧ cr = { context_left := List.map (nc_locked_mark simRi) (List.range k), input_nonterminal := nc_locked_symToNT (pattern.getD k dflt), context_right := List.map nc_locked_liftSym (List.drop (k + 1) pattern), output_string := [nc_locked_mark simRi k] }

theorem nc_locked_rule_output_out_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {cr : csrule T (NC_LockedNT g)} (hcr : cr ∈ (locked_csg_of_noncontracting g hg).rules) {ri k : ℕ} {a : symbol T g.nt} (hout : nc_locked_out ri k a ∈ cr.output_string) : ∃ (simRi : ℕ) (grule : grule T g.nt), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ k < grule.output_string.length ∧ a = grule.output_string.getD k (symbol.nonterminal grule.input_N) ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; have dflt := symbol.nonterminal grule.input_N; pattern.length - 1 ≤ k ∧ cr = { context_left := List.map (nc_locked_mark simRi) (List.range (pattern.length - 1)), input_nonterminal := NC_LockedNT.mark simRi (pattern.length - 1), context_right := [], output_string := nc_locked_outputFrom simRi grule.output_string dflt (pattern.length - 1) } ∨ k < pattern.length - 1 ∧ cr = { context_left := List.map (nc_locked_mark simRi) (List.range k), input_nonterminal := NC_LockedNT.mark simRi k, context_right := nc_locked_outputSuffix simRi grule.output_string dflt (k + 1), output_string := [nc_locked_out simRi k (grule.output_string.getD k dflt)] }

theorem nc_locked_transform_added_mark_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) {ri k : ℕ} (htgt : nc_locked_mark ri k ∈ s₂) (hsrc : nc_locked_mark ri k ∉ s₁) : ∃ (simRi : ℕ) (grule : grule T g.nt), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; have dflt := symbol.nonterminal grule.input_N; k < pattern.length ∧ ∃ cr ∈ (locked_csg_of_noncontracting g hg).rules, cr.context_left = List.map (nc_locked_mark simRi) (List.range k) ∧ cr.input_nonterminal = nc_locked_symToNT (pattern.getD k dflt) ∧ cr.context_right = List.map nc_locked_liftSym (List.drop (k + 1) pattern) ∧ cr.output_string = [nc_locked_mark simRi k]

theorem nc_locked_transform_added_mark_source_context_marks {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) {ri k : ℕ} (htgt : nc_locked_mark ri k ∈ s₂) (hsrc : nc_locked_mark ri k ∉ s₁) : ∃ (simRi : ℕ) (grule : grule T g.nt), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; k < pattern.length ∧ ∀ j < k, nc_locked_mark simRi j ∈ s₁

If a transform newly creates marker k, then the rule that creates it is a phase-1 marking rule and all lower markers for that same simulation occur in the source. This records the context dependency of the locked input-marking phase.

theorem nc_locked_transform_added_mark_from_single_mark_source {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) {baseRi targetRi targetK : ℕ} (htgt : nc_locked_mark targetRi targetK ∈ s₂) (hsrc : nc_locked_mark targetRi targetK ∉ s₁) (hmarks : ∀ (ri k : ℕ), nc_locked_mark ri k ∈ s₁ ↔ (ri, k) = (baseRi, 0)) : ∃ (simRi : ℕ) (grule : grule T g.nt), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ targetRi = simRi ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; targetK < pattern.length ∧ (targetK = 0 ∨ simRi = baseRi ∧ targetK = 1)

theorem nc_locked_transform_added_base_one_mark_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) {baseRi : ℕ} (htgt : nc_locked_mark baseRi 1 ∈ s₂) (hsrc : nc_locked_mark baseRi 1 ∉ s₁) (_hmarks : ∀ (ri k : ℕ), nc_locked_mark ri k ∈ s₁ ↔ (ri, k) = (baseRi, 0)) : ∃ (grule : grule T g.nt), (baseRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; have dflt := symbol.nonterminal grule.input_N; 1 < pattern.length ∧ ∃ cr ∈ (locked_csg_of_noncontracting g hg).rules, cr.context_left = [nc_locked_mark baseRi 0] ∧ cr.input_nonterminal = nc_locked_symToNT (pattern.getD 1 dflt) ∧ cr.context_right = List.map nc_locked_liftSym (List.drop 2 pattern) ∧ cr.output_string = [nc_locked_mark baseRi 1]

If a step whose source contains a single phase-0 marker creates the phase-1 marker for that same simulation, then the step is exactly the first continuation marking rule for the corresponding original production.

theorem nc_locked_transform_added_base_one_mark_exact {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {ri : ℕ} {r : grule T g.nt} {u v smid : List (symbol T (NC_LockedNT g))} (hpair : (ri, r) ∈ (List.range g.rules.length).zip g.rules) (hu : nc_locked_is_clean g u) (hv : nc_locked_is_clean g v) (hstep : CS_transforms (locked_csg_of_noncontracting g hg) (u ++ [nc_locked_mark ri 0] ++ List.map nc_locked_liftSym (List.drop 1 (r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R)) ++ v) smid) (hone : nc_locked_mark ri 1 ∈ smid) : have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; 1 < pattern.length ∧ smid = u ++ [nc_locked_mark ri 0] ++ [nc_locked_mark ri 1] ++ List.map nc_locked_liftSym (List.drop 2 pattern) ++ v

Exact source and target shape for the first continuation marking step of a locked simulation. Once the boundary phase-1 marker is newly created, the whole step is forced to replace the second lifted input symbol by that marker, with the original surrounding context unchanged.

theorem nc_locked_mark_not_mem_prior_range {T : Type} (g : grammar T) (ri n : ℕ) : nc_locked_mark ri n ∉ List.map (nc_locked_mark ri) (List.range n)

theorem nc_locked_mark_range_succ {T : Type} (g : grammar T) (ri k : ℕ) : List.map (nc_locked_mark ri) (List.range (k + 1)) = List.map (nc_locked_mark ri) (List.range k) ++ [nc_locked_mark ri k]

theorem nc_locked_transform_added_mark_preserves_source_mark {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) {targetRi targetK ri k : ℕ} (htgt : nc_locked_mark targetRi targetK ∈ s₂) (hsrc : nc_locked_mark targetRi targetK ∉ s₁) (hmark : nc_locked_mark ri k ∈ s₁) : nc_locked_mark ri k ∈ s₂

theorem nc_locked_transform_added_out_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) {ri k : ℕ} {a : symbol T g.nt} (htgt : nc_locked_out ri k a ∈ s₂) (hsrc : nc_locked_out ri k a ∉ s₁) : ∃ (simRi : ℕ) (grule : grule T g.nt), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ k < grule.output_string.length ∧ a = grule.output_string.getD k (symbol.nonterminal grule.input_N) ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; have dflt := symbol.nonterminal grule.input_N; (pattern.length - 1 ≤ k ∧ ∃ cr ∈ (locked_csg_of_noncontracting g hg).rules, cr.context_left = List.map (nc_locked_mark simRi) (List.range (pattern.length - 1)) ∧ cr.input_nonterminal = NC_LockedNT.mark simRi (pattern.length - 1) ∧ cr.context_right = [] ∧ cr.output_string = nc_locked_outputFrom simRi grule.output_string dflt (pattern.length - 1)) ∨ k < pattern.length - 1 ∧ ∃ cr ∈ (locked_csg_of_noncontracting g hg).rules, cr.context_left = List.map (nc_locked_mark simRi) (List.range k) ∧ cr.input_nonterminal = NC_LockedNT.mark simRi k ∧ cr.context_right = nc_locked_outputSuffix simRi grule.output_string dflt (k + 1) ∧ cr.output_string = [nc_locked_out simRi k (grule.output_string.getD k dflt)]

theorem nc_locked_transform_added_out_source_mark {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) {ri k : ℕ} {a : symbol T g.nt} (htgt : nc_locked_out ri k a ∈ s₂) (hsrc : nc_locked_out ri k a ∉ s₁) : ∃ (simRi : ℕ) (grule : grule T g.nt) (markIdx : ℕ), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ k < grule.output_string.length ∧ a = grule.output_string.getD k (symbol.nonterminal grule.input_N) ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; markIdx < pattern.length ∧ (pattern.length - 1 ≤ k ∧ markIdx = pattern.length - 1 ∨ k < pattern.length - 1 ∧ markIdx = k) ∧ nc_locked_mark simRi markIdx ∈ s₁

theorem nc_locked_transform_added_out_from_out_free_source {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) {ri k : ℕ} {a : symbol T g.nt} (htgt : nc_locked_out ri k a ∈ s₂) (hsrc : nc_locked_out ri k a ∉ s₁) (hnoout : ∀ (ri k : ℕ) (a : symbol T g.nt), nc_locked_out ri k a ∉ s₁) : ∃ (simRi : ℕ) (grule : grule T g.nt), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ k < grule.output_string.length ∧ a = grule.output_string.getD k (symbol.nonterminal grule.input_N) ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; pattern.length - 1 ≤ k ∧ nc_locked_mark simRi (pattern.length - 1) ∈ s₁

theorem nc_locked_transform_removed_mark_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) {ri k : ℕ} (hsrc : nc_locked_mark ri k ∈ s₁) (htgt : nc_locked_mark ri k ∉ s₂) : ∃ (simRi : ℕ) (grule : grule T g.nt), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; have dflt := symbol.nonterminal grule.input_N; (k = pattern.length - 1 ∧ ∃ cr ∈ (locked_csg_of_noncontracting g hg).rules, cr.input_nonterminal = NC_LockedNT.mark simRi (pattern.length - 1) ∧ cr.context_left = List.map (nc_locked_mark simRi) (List.range (pattern.length - 1)) ∧ cr.context_right = [] ∧ cr.output_string = nc_locked_outputFrom simRi grule.output_string dflt (pattern.length - 1)) ∨ k < pattern.length - 1 ∧ ∃ cr ∈ (locked_csg_of_noncontracting g hg).rules, cr.input_nonterminal = NC_LockedNT.mark simRi k ∧ cr.context_left = List.map (nc_locked_mark simRi) (List.range k) ∧ cr.context_right = nc_locked_outputSuffix simRi grule.output_string dflt (k + 1) ∧ cr.output_string = [nc_locked_out simRi k (grule.output_string.getD k dflt)]

theorem nc_locked_transform_removed_mark_adds_out {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) {ri k : ℕ} (hsrc : nc_locked_mark ri k ∈ s₁) (htgt : nc_locked_mark ri k ∉ s₂) : ∃ (simRi : ℕ) (grule : grule T g.nt) (j : ℕ), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ j < grule.output_string.length ∧ nc_locked_out simRi j (grule.output_string.getD j (symbol.nonterminal grule.input_N)) ∈ s₂

theorem nc_locked_transform_removed_out_adds_liftSym {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) {ri k : ℕ} {a : symbol T g.nt} (hsrc : nc_locked_out ri k a ∈ s₁) (htgt : nc_locked_out ri k a ∉ s₂) : ∃ (simRi : ℕ) (grule : grule T g.nt), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ k < grule.output_string.length ∧ a = grule.output_string.getD k (symbol.nonterminal grule.input_N) ∧ nc_locked_liftSym a ∈ s₂

theorem nc_locked_clean_step_dirty_mark_zero_unique {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) (hclean : nc_locked_is_clean g s₁) (hdirty : ¬nc_locked_is_clean g s₂) : ∃ (simRi : ℕ) (grule : grule T g.nt) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ nc_locked_is_clean g u ∧ nc_locked_is_clean g v ∧ (have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; have dflt := symbol.nonterminal grule.input_N; s₁ = u ++ [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v ∧ s₂ = u ++ [nc_locked_mark simRi 0] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v) ∧ (∀ (ri k : ℕ), nc_locked_mark ri k ∈ s₂ ↔ (ri, k) = (simRi, 0)) ∧ ∀ (ri k : ℕ) (a : symbol T g.nt), nc_locked_out ri k a ∉ s₂

theorem nc_locked_dirty_step_clean_cleanup_unique {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) (hdirty : ¬nc_locked_is_clean g s₁) (hclean : nc_locked_is_clean g s₂) : ∃ (simRi : ℕ) (grule : grule T g.nt) (k : ℕ) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ k < grule.output_string.length ∧ nc_locked_is_clean g u ∧ nc_locked_is_clean g v ∧ (have dflt := symbol.nonterminal grule.input_N; s₁ = u ++ [nc_locked_out simRi k (grule.output_string.getD k dflt)] ++ v ∧ s₂ = u ++ [nc_locked_liftSym (grule.output_string.getD k dflt)] ++ v) ∧ (∀ (ri j : ℕ), nc_locked_mark ri j ∉ s₁) ∧ ∀ (ri j : ℕ) (a : symbol T g.nt), nc_locked_out ri j a ∈ s₁ ↔ ri = simRi ∧ j = k ∧ a = grule.output_string.getD k (symbol.nonterminal grule.input_N)

Counted locked derivations

inductive NC_locked_derives_n {T : Type} (g : grammar T) (hg : grammar_noncontracting g) : ℕ → List (symbol T (NC_LockedNT g)) → List (symbol T (NC_LockedNT g)) → Prop

Step-counted derivations for the locked construction. This is equivalent to CS_derives, but exposes split points needed by the dirty-phase grouping proof.

• zero {T : Type} {g : grammar T} {hg : grammar_noncontracting g} (s : List (symbol T (NC_LockedNT g))) : NC_locked_derives_n g hg 0 s s
• step {T : Type} {g : grammar T} {hg : grammar_noncontracting g} {n : ℕ} {s₁ s₂ : List (symbol T (locked_csg_of_noncontracting g hg).nt)} {s₃ : List (symbol T (NC_LockedNT g))} : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂ → NC_locked_derives_n g hg n s₂ s₃ → NC_locked_derives_n g hg (n + 1) s₁ s₃

theorem nc_locked_derives_n_append {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ s₃ : List (symbol T (NC_LockedNT g))} (h : NC_locked_derives_n g hg n s₁ s₂) (hstep : CS_transforms (locked_csg_of_noncontracting g hg) s₂ s₃) : NC_locked_derives_n g hg (n + 1) s₁ s₃

theorem nc_locked_derives_to_derives_n {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : CS_derives (locked_csg_of_noncontracting g hg) s₁ s₂) : ∃ (n : ℕ), NC_locked_derives_n g hg n s₁ s₂

theorem nc_locked_derives_n_removed_mark_event {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_derives_n g hg n s₁ s₂) {ri k : ℕ} (hsrc : nc_locked_mark ri k ∈ s₁) (htgt : nc_locked_mark ri k ∉ s₂) : ∃ (m : ℕ) (rest : ℕ) (smid : List (symbol T (NC_LockedNT g))) (simRi : ℕ) (grule : grule T g.nt) (j : ℕ), n = m + rest ∧ NC_locked_derives_n g hg m s₁ smid ∧ NC_locked_derives_n g hg rest smid s₂ ∧ (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ j < grule.output_string.length ∧ nc_locked_out simRi j (grule.output_string.getD j (symbol.nonterminal grule.input_N)) ∈ smid

theorem nc_locked_derives_n_removed_mark_step_event {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_derives_n g hg n s₁ s₂) {ri k : ℕ} (hsrc : nc_locked_mark ri k ∈ s₁) (htgt : nc_locked_mark ri k ∉ s₂) : ∃ (pre : ℕ) (rest : ℕ) (spre : List (symbol T (NC_LockedNT g))) (spost : List (symbol T (locked_csg_of_noncontracting g hg).nt)) (simRi : ℕ) (grule : grule T g.nt) (j : ℕ), n = pre + 1 + rest ∧ NC_locked_derives_n g hg pre s₁ spre ∧ CS_transforms (locked_csg_of_noncontracting g hg) spre spost ∧ NC_locked_derives_n g hg rest spost s₂ ∧ (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ j < grule.output_string.length ∧ nc_locked_mark ri k ∈ spre ∧ nc_locked_mark ri k ∉ spost ∧ nc_locked_out simRi j (grule.output_string.getD j (symbol.nonterminal grule.input_N)) ∈ spost

theorem nc_locked_derives_n_removed_out_event {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_derives_n g hg n s₁ s₂) {ri k : ℕ} {a : symbol T g.nt} (hsrc : nc_locked_out ri k a ∈ s₁) (htgt : nc_locked_out ri k a ∉ s₂) : ∃ (m : ℕ) (rest : ℕ) (smid : List (symbol T (NC_LockedNT g))) (simRi : ℕ) (grule : grule T g.nt), n = m + rest ∧ NC_locked_derives_n g hg m s₁ smid ∧ NC_locked_derives_n g hg rest smid s₂ ∧ (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ k < grule.output_string.length ∧ a = grule.output_string.getD k (symbol.nonterminal grule.input_N) ∧ nc_locked_liftSym a ∈ smid

theorem nc_locked_derives_n_added_out_event {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_derives_n g hg n s₁ s₂) {ri k : ℕ} {a : symbol T g.nt} (hsrc : nc_locked_out ri k a ∉ s₁) (htgt : nc_locked_out ri k a ∈ s₂) : ∃ (m : ℕ) (rest : ℕ) (smid : List (symbol T (NC_LockedNT g))) (simRi : ℕ) (grule : grule T g.nt), n = m + rest ∧ NC_locked_derives_n g hg m s₁ smid ∧ NC_locked_derives_n g hg rest smid s₂ ∧ (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ k < grule.output_string.length ∧ a = grule.output_string.getD k (symbol.nonterminal grule.input_N) ∧ nc_locked_out ri k a ∈ smid

theorem nc_locked_derives_n_added_out_step_event {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_derives_n g hg n s₁ s₂) {ri k : ℕ} {a : symbol T g.nt} (hsrc : nc_locked_out ri k a ∉ s₁) (htgt : nc_locked_out ri k a ∈ s₂) : ∃ (pre : ℕ) (rest : ℕ) (spre : List (symbol T (NC_LockedNT g))) (spost : List (symbol T (locked_csg_of_noncontracting g hg).nt)) (simRi : ℕ) (grule : grule T g.nt), n = pre + 1 + rest ∧ NC_locked_derives_n g hg pre s₁ spre ∧ CS_transforms (locked_csg_of_noncontracting g hg) spre spost ∧ NC_locked_derives_n g hg rest spost s₂ ∧ (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ k < grule.output_string.length ∧ a = grule.output_string.getD k (symbol.nonterminal grule.input_N) ∧ nc_locked_out ri k a ∉ spre ∧ nc_locked_out ri k a ∈ spost

theorem nc_locked_derives_n_added_out_step_source_mark_event {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_derives_n g hg n s₁ s₂) {ri k : ℕ} {a : symbol T g.nt} (hsrc : nc_locked_out ri k a ∉ s₁) (htgt : nc_locked_out ri k a ∈ s₂) : ∃ (pre : ℕ) (rest : ℕ) (spre : List (symbol T (NC_LockedNT g))) (spost : List (symbol T (locked_csg_of_noncontracting g hg).nt)) (simRi : ℕ) (grule : grule T g.nt) (markIdx : ℕ), n = pre + 1 + rest ∧ NC_locked_derives_n g hg pre s₁ spre ∧ CS_transforms (locked_csg_of_noncontracting g hg) spre spost ∧ NC_locked_derives_n g hg rest spost s₂ ∧ (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ k < grule.output_string.length ∧ a = grule.output_string.getD k (symbol.nonterminal grule.input_N) ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; markIdx < pattern.length ∧ (pattern.length - 1 ≤ k ∧ markIdx = pattern.length - 1 ∨ k < pattern.length - 1 ∧ markIdx = k) ∧ nc_locked_mark simRi markIdx ∈ spre

theorem nc_locked_derives_n_to_clean_mark_event {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_derives_n g hg n s₁ s₂) (hclean₂ : nc_locked_is_clean g s₂) {ri k : ℕ} (hsrc : nc_locked_mark ri k ∈ s₁) : ∃ (m : ℕ) (rest : ℕ) (smid : List (symbol T (NC_LockedNT g))) (simRi : ℕ) (grule : grule T g.nt) (j : ℕ), n = m + rest ∧ NC_locked_derives_n g hg m s₁ smid ∧ NC_locked_derives_n g hg rest smid s₂ ∧ (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ j < grule.output_string.length ∧ nc_locked_out simRi j (grule.output_string.getD j (symbol.nonterminal grule.input_N)) ∈ smid

theorem nc_locked_derives_n_to_clean_out_event {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_derives_n g hg n s₁ s₂) (hclean₂ : nc_locked_is_clean g s₂) {ri k : ℕ} {a : symbol T g.nt} (hsrc : nc_locked_out ri k a ∈ s₁) : ∃ (m : ℕ) (rest : ℕ) (smid : List (symbol T (NC_LockedNT g))) (simRi : ℕ) (grule : grule T g.nt), n = m + rest ∧ NC_locked_derives_n g hg m s₁ smid ∧ NC_locked_derives_n g hg rest smid s₂ ∧ (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ k < grule.output_string.length ∧ a = grule.output_string.getD k (symbol.nonterminal grule.input_N) ∧ nc_locked_liftSym a ∈ smid

inductive NC_locked_dirty_derives_n {T : Type} (g : grammar T) (hg : grammar_noncontracting g) : ℕ → List (symbol T (NC_LockedNT g)) → List (symbol T (NC_LockedNT g)) → Prop

Counted locked derivations whose every boundary state is dirty.

• zero {T : Type} {g : grammar T} {hg : grammar_noncontracting g} {s : List (symbol T (NC_LockedNT g))} : ¬nc_locked_is_clean g s → NC_locked_dirty_derives_n g hg 0 s s
• step {T : Type} {g : grammar T} {hg : grammar_noncontracting g} {n : ℕ} {s₁ s₂ : List (symbol T (locked_csg_of_noncontracting g hg).nt)} {s₃ : List (symbol T (NC_LockedNT g))} : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂ → ¬nc_locked_is_clean g s₁ → ¬nc_locked_is_clean g s₂ → NC_locked_dirty_derives_n g hg n s₂ s₃ → NC_locked_dirty_derives_n g hg (n + 1) s₁ s₃

theorem nc_locked_dirty_derives_n_to_derives_n {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_dirty_derives_n g hg n s₁ s₂) : NC_locked_derives_n g hg n s₁ s₂

theorem nc_locked_dirty_derives_n_end_dirty {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_dirty_derives_n g hg n s₁ s₂) : ¬nc_locked_is_clean g s₂

theorem nc_locked_dirty_return_mark_event {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hdirty : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) {ri k : ℕ} (hmark : nc_locked_mark ri k ∈ s_after) : ∃ (pre : ℕ) (rest : ℕ) (smid : List (symbol T (NC_LockedNT g))) (simRi : ℕ) (grule : grule T g.nt) (j : ℕ), m + 1 = pre + rest ∧ NC_locked_derives_n g hg pre s_after smid ∧ NC_locked_derives_n g hg rest smid s_clean ∧ (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ j < grule.output_string.length ∧ nc_locked_out simRi j (grule.output_string.getD j (symbol.nonterminal grule.input_N)) ∈ smid

theorem nc_locked_dirty_return_mark_step_event {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hdirty : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) {ri k : ℕ} (hmark : nc_locked_mark ri k ∈ s_after) : ∃ (pre : ℕ) (rest : ℕ) (spre : List (symbol T (NC_LockedNT g))) (spost : List (symbol T (locked_csg_of_noncontracting g hg).nt)) (simRi : ℕ) (grule : grule T g.nt) (j : ℕ), m + 1 = pre + 1 + rest ∧ NC_locked_derives_n g hg pre s_after spre ∧ CS_transforms (locked_csg_of_noncontracting g hg) spre spost ∧ NC_locked_derives_n g hg rest spost s_clean ∧ (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ ri = simRi ∧ j < grule.output_string.length ∧ nc_locked_mark ri k ∈ spre ∧ nc_locked_mark ri k ∉ spost ∧ nc_locked_out simRi j (grule.output_string.getD j (symbol.nonterminal grule.input_N)) ∈ spost

theorem nc_locked_dirty_interval_final_cleanup_added_out_event {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_start s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hstart : CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after) (hclean_start : nc_locked_is_clean g s_start) (hdirty_after : ¬nc_locked_is_clean g s_after) (hmid : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hdirty : ¬nc_locked_is_clean g s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) : ∃ (ri : ℕ) (r : grule T g.nt) (k : ℕ) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))) (pre : ℕ) (rest : ℕ) (smid : List (symbol T (NC_LockedNT g))), (ri, r) ∈ (List.range g.rules.length).zip g.rules ∧ k < r.output_string.length ∧ (have dflt := symbol.nonterminal r.input_N; s_dirty = u ++ [nc_locked_out ri k (r.output_string.getD k dflt)] ++ v ∧ s_clean = u ++ [nc_locked_liftSym (r.output_string.getD k dflt)] ++ v) ∧ m = pre + rest ∧ NC_locked_derives_n g hg pre s_after smid ∧ NC_locked_derives_n g hg rest smid s_dirty ∧ nc_locked_out ri k (r.output_string.getD k (symbol.nonterminal r.input_N)) ∈ smid

In a dirty interval that starts from a clean form, the unique output marker cleaned by the final dirty-to-clean step must have been introduced during the dirty part of the interval.

theorem nc_locked_dirty_interval_final_cleanup_added_out_step_event {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_start s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hstart : CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after) (hclean_start : nc_locked_is_clean g s_start) (hdirty_after : ¬nc_locked_is_clean g s_after) (hmid : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hdirty : ¬nc_locked_is_clean g s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) : ∃ (ri : ℕ) (r : grule T g.nt) (k : ℕ) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))) (pre : ℕ) (rest : ℕ) (spre : List (symbol T (NC_LockedNT g))) (spost : List (symbol T (locked_csg_of_noncontracting g hg).nt)), (ri, r) ∈ (List.range g.rules.length).zip g.rules ∧ k < r.output_string.length ∧ (have dflt := symbol.nonterminal r.input_N; s_dirty = u ++ [nc_locked_out ri k (r.output_string.getD k dflt)] ++ v ∧ s_clean = u ++ [nc_locked_liftSym (r.output_string.getD k dflt)] ++ v) ∧ m = pre + 1 + rest ∧ NC_locked_derives_n g hg pre s_after spre ∧ CS_transforms (locked_csg_of_noncontracting g hg) spre spost ∧ NC_locked_derives_n g hg rest spost s_dirty ∧ nc_locked_out ri k (r.output_string.getD k (symbol.nonterminal r.input_N)) ∉ spre ∧ nc_locked_out ri k (r.output_string.getD k (symbol.nonterminal r.input_N)) ∈ spost

A step-split form of nc_locked_dirty_interval_final_cleanup_added_out_event: the output marker cleaned by the final return-to-clean step has a concrete introduction step inside the dirty interval.

theorem nc_locked_dirty_interval_mid_length_pos {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_start s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hstart : CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after) (hclean_start : nc_locked_is_clean g s_start) (hdirty_after : ¬nc_locked_is_clean g s_after) (hmid : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hdirty : ¬nc_locked_is_clean g s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) : 0 < m

A dirty interval cannot return to a clean form immediately after its clean-to-dirty start. The start state contains a single input marker and no output marker, while a dirty-to-clean step must clean a unique output marker.

theorem nc_locked_dirty_derives_n_step_split_of_pos {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (hpos : 0 < m) (h : NC_locked_dirty_derives_n g hg m s₁ s₂) : ∃ (m' : ℕ) (smid : List (symbol T (locked_csg_of_noncontracting g hg).nt)), m = m' + 1 ∧ CS_transforms (locked_csg_of_noncontracting g hg) s₁ smid ∧ ¬nc_locked_is_clean g smid ∧ NC_locked_dirty_derives_n g hg m' smid s₂

theorem nc_locked_dirty_interval_first_dirty_step {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_start s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hstart : CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after) (hclean_start : nc_locked_is_clean g s_start) (hdirty_after : ¬nc_locked_is_clean g s_after) (hmid : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hdirty : ¬nc_locked_is_clean g s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) : ∃ (m' : ℕ) (smid : List (symbol T (locked_csg_of_noncontracting g hg).nt)), m = m' + 1 ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_after smid ∧ ¬nc_locked_is_clean g smid ∧ NC_locked_dirty_derives_n g hg m' smid s_dirty

Nondegenerate dirty intervals expose their first dirty-to-dirty step.

theorem nc_locked_dirty_interval_first_step_removed_start_mark_summary {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_start s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hstart : CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after) (hclean_start : nc_locked_is_clean g s_start) (hdirty_after : ¬nc_locked_is_clean g s_after) (hmid : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hdirty : ¬nc_locked_is_clean g s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) : ∃ (ri : ℕ) (r : grule T g.nt) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))) (m' : ℕ) (smid : List (symbol T (locked_csg_of_noncontracting g hg).nt)), (ri, r) ∈ (List.range g.rules.length).zip g.rules ∧ (have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; s_start = u ++ [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v ∧ s_after = u ++ [nc_locked_mark ri 0] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v) ∧ m = m' + 1 ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_after smid ∧ ¬nc_locked_is_clean g smid ∧ NC_locked_dirty_derives_n g hg m' smid s_dirty ∧ (nc_locked_mark ri 0 ∉ smid → (r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R).length = 1 ∧ (∀ (targetRi targetK : ℕ), nc_locked_mark targetRi targetK ∉ smid) ∧ ∃ j < r.output_string.length, nc_locked_out ri j (r.output_string.getD j (symbol.nonterminal r.input_N)) ∈ smid)

Packaged consumed-boundary branch for the first dirty-to-dirty step: if the marker opened by the clean-to-dirty boundary disappears, then the simulated input pattern had length one, the next state has no input markers, and the same step produced an output marker for that simulation.

theorem nc_locked_dirty_interval_first_step_removed_start_mark_endpoint {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_start s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hstart : CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after) (hclean_start : nc_locked_is_clean g s_start) (hdirty_after : ¬nc_locked_is_clean g s_after) (hmid : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hdirty : ¬nc_locked_is_clean g s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) : ∃ (ri : ℕ) (r : grule T g.nt) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))) (m' : ℕ) (smid : List (symbol T (locked_csg_of_noncontracting g hg).nt)), (ri, r) ∈ (List.range g.rules.length).zip g.rules ∧ (have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; s_start = u ++ [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v ∧ s_after = u ++ [nc_locked_mark ri 0] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v) ∧ m = m' + 1 ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_after smid ∧ ¬nc_locked_is_clean g smid ∧ NC_locked_dirty_derives_n g hg m' smid s_dirty ∧ (nc_locked_mark ri 0 ∉ smid → smid = u ++ nc_locked_outputFrom ri r.output_string (symbol.nonterminal r.input_N) 0 ++ v)

In the consumed-boundary branch, the first dirty-to-dirty step has exactly the clean macro target for the opened original rule.

theorem nc_locked_dirty_trace_first_clean_step_split {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_derives_n g hg n s₁ s₂) (hdirty₁ : ¬nc_locked_is_clean g s₁) (hclean₂ : nc_locked_is_clean g s₂) : ∃ (m : ℕ) (rest : ℕ) (s_dirty : List (symbol T (NC_LockedNT g))) (s_clean : List (symbol T (locked_csg_of_noncontracting g hg).nt)), n = m + 1 + rest ∧ NC_locked_derives_n g hg m s₁ s_dirty ∧ ¬nc_locked_is_clean g s_dirty ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean ∧ nc_locked_is_clean g s_clean ∧ NC_locked_derives_n g hg rest s_clean s₂

theorem nc_locked_dirty_trace_first_clean_step_dirty_split {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_derives_n g hg n s₁ s₂) (hdirty₁ : ¬nc_locked_is_clean g s₁) (hclean₂ : nc_locked_is_clean g s₂) : ∃ (m : ℕ) (rest : ℕ) (s_dirty : List (symbol T (NC_LockedNT g))) (s_clean : List (symbol T (locked_csg_of_noncontracting g hg).nt)), n = m + 1 + rest ∧ NC_locked_dirty_derives_n g hg m s₁ s_dirty ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean ∧ nc_locked_is_clean g s_clean ∧ NC_locked_derives_n g hg rest s_clean s₂

Locked clean reverse traces

inductive NC_locked_clean_macro_step {T : Type} (g : grammar T) (hg : grammar_noncontracting g) : List (symbol T (NC_LockedNT g)) → List (symbol T (NC_LockedNT g)) → Prop

Clean macro steps in the locked construction. The sim constructor is the macro endpoint for one complete locked simulation of an original non-contracting rule under arbitrary surrounding context.

• clean {T : Type} {g : grammar T} {hg : grammar_noncontracting g} {s₁ s₂ : List (symbol T (locked_csg_of_noncontracting g hg).nt)} : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂ → nc_locked_is_clean g s₁ → nc_locked_is_clean g s₂ → NC_locked_clean_macro_step g hg s₁ s₂
• sim {T : Type} {g : grammar T} {hg : grammar_noncontracting g} {ri : ℕ} {r : grule T g.nt} {u v : List (symbol T (NC_LockedNT g))} : (ri, r) ∈ (List.range g.rules.length).zip g.rules → NC_locked_clean_macro_step g hg (u ++ List.map nc_locked_liftSym (r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R) ++ v) (u ++ List.map nc_locked_liftSym r.output_string ++ v)

theorem nc_locked_clean_macro_step_grammar_derives {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_clean_macro_step g hg s₁ s₂) : grammar_derives g (nc_locked_proj g s₁) (nc_locked_proj g s₂)

Every locked clean macro step projects to an unrestricted derivation in the original grammar.

inductive NC_locked_clean_macro_derives_n {T : Type} (g : grammar T) (hg : grammar_noncontracting g) : ℕ → List (symbol T (NC_LockedNT g)) → List (symbol T (NC_LockedNT g)) → Prop

Step-counted traces of locked clean macro steps.

• zero {T : Type} {g : grammar T} {hg : grammar_noncontracting g} {s : List (symbol T (NC_LockedNT g))} : nc_locked_is_clean g s → NC_locked_clean_macro_derives_n g hg 0 s s
• step {T : Type} {g : grammar T} {hg : grammar_noncontracting g} {n : ℕ} {s₁ s₂ s₃ : List (symbol T (NC_LockedNT g))} : NC_locked_clean_macro_step g hg s₁ s₂ → NC_locked_clean_macro_derives_n g hg n s₂ s₃ → NC_locked_clean_macro_derives_n g hg (n + 1) s₁ s₃

theorem nc_locked_clean_macro_trace_grammar_derives {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_clean_macro_derives_n g hg n s₁ s₂) : grammar_derives g (nc_locked_proj g s₁) (nc_locked_proj g s₂)

Locked clean macro traces project to unrestricted derivations in the original grammar.

theorem nc_locked_clean_macro_derives_n_trans {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m n : ℕ} {s₁ s₂ s₃ : List (symbol T (NC_LockedNT g))} (h₁ : NC_locked_clean_macro_derives_n g hg m s₁ s₂) (h₂ : NC_locked_clean_macro_derives_n g hg n s₂ s₃) : NC_locked_clean_macro_derives_n g hg (m + n) s₁ s₃

inductive NC_locked_clean_derives_n {T : Type} (g : grammar T) (hg : grammar_noncontracting g) : ℕ → List (symbol T (NC_LockedNT g)) → List (symbol T (NC_LockedNT g)) → Prop

A finite locked CS derivation trace whose adjacent endpoints are all clean.

• zero {T : Type} {g : grammar T} {hg : grammar_noncontracting g} {s : List (symbol T (NC_LockedNT g))} : nc_locked_is_clean g s → NC_locked_clean_derives_n g hg 0 s s
• step {T : Type} {g : grammar T} {hg : grammar_noncontracting g} {n : ℕ} {s₁ s₂ : List (symbol T (locked_csg_of_noncontracting g hg).nt)} {s₃ : List (symbol T (NC_LockedNT g))} : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂ → nc_locked_is_clean g s₁ → nc_locked_is_clean g s₂ → NC_locked_clean_derives_n g hg n s₂ s₃ → NC_locked_clean_derives_n g hg (n + 1) s₁ s₃

theorem nc_locked_clean_trace_or_first_dirty_segment {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_derives_n g hg n s₁ s₂) (hclean₁ : nc_locked_is_clean g s₁) (hclean₂ : nc_locked_is_clean g s₂) : NC_locked_clean_derives_n g hg n s₁ s₂ ∨ ∃ (pre : ℕ) (m : ℕ) (rest : ℕ) (s_start : List (symbol T (NC_LockedNT g))) (s_after : List (symbol T (NC_LockedNT g))) (s_dirty : List (symbol T (NC_LockedNT g))) (s_clean : List (symbol T (NC_LockedNT g))), n = pre + 1 + m + 1 + rest ∧ NC_locked_clean_derives_n g hg pre s₁ s_start ∧ nc_locked_is_clean g s_start ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after ∧ ¬nc_locked_is_clean g s_after ∧ NC_locked_derives_n g hg m s_after s_dirty ∧ ¬nc_locked_is_clean g s_dirty ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean ∧ nc_locked_is_clean g s_clean ∧ NC_locked_derives_n g hg rest s_clean s₂

theorem nc_locked_clean_trace_or_first_dirty_segment_dirty {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_derives_n g hg n s₁ s₂) (hclean₁ : nc_locked_is_clean g s₁) (hclean₂ : nc_locked_is_clean g s₂) : NC_locked_clean_derives_n g hg n s₁ s₂ ∨ ∃ (pre : ℕ) (m : ℕ) (rest : ℕ) (s_start : List (symbol T (NC_LockedNT g))) (s_after : List (symbol T (NC_LockedNT g))) (s_dirty : List (symbol T (NC_LockedNT g))) (s_clean : List (symbol T (NC_LockedNT g))), n = pre + 1 + m + 1 + rest ∧ NC_locked_clean_derives_n g hg pre s₁ s_start ∧ nc_locked_is_clean g s_start ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after ∧ ¬nc_locked_is_clean g s_after ∧ NC_locked_dirty_derives_n g hg m s_after s_dirty ∧ ¬nc_locked_is_clean g s_dirty ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean ∧ nc_locked_is_clean g s_clean ∧ NC_locked_derives_n g hg rest s_clean s₂

theorem nc_locked_clean_trace_to_macro_trace {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_clean_derives_n g hg n s₁ s₂) : NC_locked_clean_macro_derives_n g hg n s₁ s₂

Ordinary locked clean traces are a special case of locked clean macro traces.

def NC_locked_dirty_interval_macro_property {T : Type} (g : grammar T) (hg : grammar_noncontracting g) : Prop

The remaining local grouping property for the locked construction: any dirty interval bracketed by one clean-to-dirty step and one dirty-to-clean step compresses to some clean macro trace.

Equations

• One or more equations did not get rendered due to their size.

theorem nc_locked_clean_endpoints_to_macro_trace_of_dirty_interval_macro {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (h : NC_locked_derives_n g hg n s₁ s₂) (hclean₁ : nc_locked_is_clean g s₁) (hclean₂ : nc_locked_is_clean g s₂) (hgroup : NC_locked_dirty_interval_macro_property g hg) : ∃ (k : ℕ), NC_locked_clean_macro_derives_n g hg k s₁ s₂

Abstract compression principle for locked traces. Once every dirty interval between clean endpoints can be replaced by a clean macro trace, every clean-to-clean locked derivation can be compressed to a clean macro trace.

theorem CS_language_subset_locked_csg_of_noncontracting_of_dirty_interval_macro {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (hgroup : NC_locked_dirty_interval_macro_property g hg) (w : List T) : w ∈ CS_language (locked_csg_of_noncontracting g hg) → w ∈ grammar_language g

Reverse language inclusion for the locked construction, assuming the local dirty-interval grouping property.

theorem locked_csg_of_noncontracting_language_eq_of_dirty_interval_macro {T : Type} (g : grammar T) (hg : grammar_noncontracting g) (hgroup : NC_locked_dirty_interval_macro_property g hg) : CS_language (locked_csg_of_noncontracting g hg) = grammar_language g

Language equality for the locked construction, reduced to the local dirty-interval grouping property.

theorem nc_locked_proj_sim_source_head_drop {T : Type} (g : grammar T) (r : grule T g.nt) (u v : List (symbol T (NC_LockedNT g))) : have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; nc_locked_proj g (u ++ [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v) = nc_locked_proj g u ++ pattern ++ nc_locked_proj g v

theorem nc_locked_lifted_pattern_eq_head_drop {T : Type} (g : grammar T) (r : grule T g.nt) : have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) = List.map nc_locked_liftSym pattern

theorem nc_locked_proj_sim_target {T : Type} (g : grammar T) (r : grule T g.nt) (u v : List (symbol T (NC_LockedNT g))) : nc_locked_proj g (u ++ List.map nc_locked_liftSym r.output_string ++ v) = nc_locked_proj g u ++ r.output_string ++ nc_locked_proj g v

theorem nc_locked_boundary_macro_step {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {ri : ℕ} {r : grule T g.nt} {u v s₁ s₂ : List (symbol T (NC_LockedNT g))} (hpair : (ri, r) ∈ (List.range g.rules.length).zip g.rules) (hs₁ : have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; s₁ = u ++ [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v) (hs₂ : s₂ = u ++ List.map nc_locked_liftSym r.output_string ++ v) : NC_locked_clean_macro_step g hg s₁ s₂

theorem nc_locked_dirty_interval_consumed_boundary_macro_target {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_start s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hstart : CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after) (hclean_start : nc_locked_is_clean g s_start) (hdirty_after : ¬nc_locked_is_clean g s_after) (hmid : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hdirty : ¬nc_locked_is_clean g s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) : ∃ (ri : ℕ) (r : grule T g.nt) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))) (m' : ℕ) (smid : List (symbol T (locked_csg_of_noncontracting g hg).nt)), (ri, r) ∈ (List.range g.rules.length).zip g.rules ∧ (have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; s_start = u ++ [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v ∧ s_after = u ++ [nc_locked_mark ri 0] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v) ∧ m = m' + 1 ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_after smid ∧ ¬nc_locked_is_clean g smid ∧ NC_locked_dirty_derives_n g hg m' smid s_dirty ∧ (nc_locked_mark ri 0 ∉ smid → smid = u ++ nc_locked_outputFrom ri r.output_string (symbol.nonterminal r.input_N) 0 ++ v ∧ CS_derives (locked_csg_of_noncontracting g hg) smid (u ++ List.map nc_locked_liftSym r.output_string ++ v) ∧ NC_locked_clean_macro_step g hg s_start (u ++ List.map nc_locked_liftSym r.output_string ++ v))

The consumed-boundary first-step case has the expected macro endpoint: the dirty state produced by consuming the boundary marker is the locked output block, that block cleans to the macro target, and the original clean boundary step already determines the corresponding clean macro simulation.

theorem nc_locked_dirty_interval_consumed_boundary_macro_prefix {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_start s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hstart : CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after) (hclean_start : nc_locked_is_clean g s_start) (hdirty_after : ¬nc_locked_is_clean g s_after) (hmid : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hdirty : ¬nc_locked_is_clean g s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) : ∃ (ri : ℕ) (r : grule T g.nt) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))) (m' : ℕ) (smid : List (symbol T (locked_csg_of_noncontracting g hg).nt)), (ri, r) ∈ (List.range g.rules.length).zip g.rules ∧ (have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; s_start = u ++ [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v ∧ s_after = u ++ [nc_locked_mark ri 0] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v) ∧ m = m' + 1 ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_after smid ∧ ¬nc_locked_is_clean g smid ∧ NC_locked_dirty_derives_n g hg m' smid s_dirty ∧ (nc_locked_mark ri 0 ∉ smid → have target := u ++ List.map nc_locked_liftSym r.output_string ++ v; CS_derives (locked_csg_of_noncontracting g hg) smid target ∧ nc_locked_is_clean g target ∧ NC_locked_clean_macro_derives_n g hg 1 s_start target)

Counted clean-macro pref for the consumed-boundary branch. This is the canonical first macro segment that will later be concatenated with whatever clean behavior remains after all dirty markers have disappeared.

theorem nc_locked_dirty_interval_first_step_macro_prefix_or_mark_retained {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_start s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hstart : CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after) (hclean_start : nc_locked_is_clean g s_start) (hdirty_after : ¬nc_locked_is_clean g s_after) (hmid : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hdirty : ¬nc_locked_is_clean g s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) : ∃ (ri : ℕ) (r : grule T g.nt) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))) (m' : ℕ) (smid : List (symbol T (locked_csg_of_noncontracting g hg).nt)), (ri, r) ∈ (List.range g.rules.length).zip g.rules ∧ (have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; s_start = u ++ [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v ∧ s_after = u ++ [nc_locked_mark ri 0] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v) ∧ m = m' + 1 ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_after smid ∧ ¬nc_locked_is_clean g smid ∧ NC_locked_dirty_derives_n g hg m' smid s_dirty ∧ (nc_locked_mark ri 0 ∈ smid ∨ have target := u ++ List.map nc_locked_liftSym r.output_string ++ v; CS_derives (locked_csg_of_noncontracting g hg) smid target ∧ nc_locked_is_clean g target ∧ NC_locked_clean_macro_derives_n g hg 1 s_start target)

First-step dichotomy for dirty intervals, in a form suitable for the final grouping induction. After the first dirty-to-dirty step, either the marker opened by the clean-to-dirty boundary is still present, or that first step has already completed the boundary simulation and yields a canonical one-step clean macro pref.

theorem nc_locked_dirty_interval_first_step_event_or_macro_prefix {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_start s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hstart : CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after) (hclean_start : nc_locked_is_clean g s_start) (hdirty_after : ¬nc_locked_is_clean g s_after) (hmid : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hdirty : ¬nc_locked_is_clean g s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) : ∃ (ri : ℕ) (r : grule T g.nt) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))) (m' : ℕ) (smid : List (symbol T (locked_csg_of_noncontracting g hg).nt)), (ri, r) ∈ (List.range g.rules.length).zip g.rules ∧ (have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; s_start = u ++ [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v ∧ s_after = u ++ [nc_locked_mark ri 0] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v) ∧ m = m' + 1 ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_after smid ∧ ¬nc_locked_is_clean g smid ∧ NC_locked_dirty_derives_n g hg m' smid s_dirty ∧ ((nc_locked_mark ri 0 ∈ smid ∧ ∃ (pre : ℕ) (rest : ℕ) (sevent : List (symbol T (NC_LockedNT g))) (j : ℕ), m' + 1 = pre + rest ∧ NC_locked_derives_n g hg pre smid sevent ∧ NC_locked_derives_n g hg rest sevent s_clean ∧ j < r.output_string.length ∧ nc_locked_out ri j (r.output_string.getD j (symbol.nonterminal r.input_N)) ∈ sevent) ∨ have target := u ++ List.map nc_locked_liftSym r.output_string ++ v; CS_derives (locked_csg_of_noncontracting g hg) smid target ∧ nc_locked_is_clean g target ∧ NC_locked_clean_macro_derives_n g hg 1 s_start target)

First-step dichotomy with the retained branch expanded to its eventual output event. If the marker opened by the clean-to-dirty boundary survives the first dirty step, then the remaining dirty interval must later emit an output marker for the same original rule before it can return to a clean form.

theorem nc_locked_dirty_interval_first_step_emit_step_or_macro_prefix {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_start s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hstart : CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after) (hclean_start : nc_locked_is_clean g s_start) (hdirty_after : ¬nc_locked_is_clean g s_after) (hmid : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hdirty : ¬nc_locked_is_clean g s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) : ∃ (ri : ℕ) (r : grule T g.nt) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))) (m' : ℕ) (smid : List (symbol T (locked_csg_of_noncontracting g hg).nt)), (ri, r) ∈ (List.range g.rules.length).zip g.rules ∧ (have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; s_start = u ++ [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v ∧ s_after = u ++ [nc_locked_mark ri 0] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v) ∧ m = m' + 1 ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_after smid ∧ ¬nc_locked_is_clean g smid ∧ NC_locked_dirty_derives_n g hg m' smid s_dirty ∧ ((nc_locked_mark ri 0 ∈ smid ∧ ∃ (pre : ℕ) (rest : ℕ) (spre : List (symbol T (NC_LockedNT g))) (spost : List (symbol T (locked_csg_of_noncontracting g hg).nt)) (j : ℕ), m' + 1 = pre + 1 + rest ∧ NC_locked_derives_n g hg pre smid spre ∧ CS_transforms (locked_csg_of_noncontracting g hg) spre spost ∧ NC_locked_derives_n g hg rest spost s_clean ∧ j < r.output_string.length ∧ nc_locked_mark ri 0 ∈ spre ∧ nc_locked_mark ri 0 ∉ spost ∧ nc_locked_out ri j (r.output_string.getD j (symbol.nonterminal r.input_N)) ∈ spost) ∨ have target := u ++ List.map nc_locked_liftSym r.output_string ++ v; CS_derives (locked_csg_of_noncontracting g hg) smid target ∧ nc_locked_is_clean g target ∧ NC_locked_clean_macro_derives_n g hg 1 s_start target)

Step-split version of nc_locked_dirty_interval_first_step_event_or_macro_prefix. In the retained branch this records the exact later transform that removes the start marker and emits an output marker for the same original rule.

theorem nc_locked_removed_zero_mark_step_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {ri : ℕ} {r : grule T g.nt} {s₁ s₂ : List (symbol T (NC_LockedNT g))} (hpair : (ri, r) ∈ (List.range g.rules.length).zip g.rules) (h : CS_transforms (locked_csg_of_noncontracting g hg) s₁ s₂) (hsrc : nc_locked_mark ri 0 ∈ s₁) (htgt : nc_locked_mark ri 0 ∉ s₂) : have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; (pattern.length = 1 ∧ ∃ (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))), s₁ = u ++ [nc_locked_mark ri 0] ++ v ∧ s₂ = u ++ nc_locked_outputFrom ri r.output_string dflt 0 ++ v) ∨ 1 < pattern.length ∧ ∃ (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))), s₁ = u ++ [nc_locked_mark ri 0] ++ nc_locked_outputSuffix ri r.output_string dflt 1 ++ v ∧ s₂ = u ++ [nc_locked_out ri 0 (r.output_string.getD 0 dflt)] ++ nc_locked_outputSuffix ri r.output_string dflt 1 ++ v

If a step removes the phase-0 marker for a fixed original rule, then it is one of exactly two emit steps. For a unit input pattern it is the emitLast rule and exposes the whole marked output block; otherwise it is the emitRest rule at index 0 and requires the already-emitted output suffix as right context.

theorem nc_locked_dirty_interval_first_step_emit_shape_or_macro_prefix {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_start s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hstart : CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after) (hclean_start : nc_locked_is_clean g s_start) (hdirty_after : ¬nc_locked_is_clean g s_after) (hmid : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hdirty : ¬nc_locked_is_clean g s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) : ∃ (ri : ℕ) (r : grule T g.nt) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))) (m' : ℕ) (smid : List (symbol T (locked_csg_of_noncontracting g hg).nt)), (ri, r) ∈ (List.range g.rules.length).zip g.rules ∧ (have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; s_start = u ++ [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v ∧ s_after = u ++ [nc_locked_mark ri 0] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v) ∧ m = m' + 1 ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_after smid ∧ ¬nc_locked_is_clean g smid ∧ NC_locked_dirty_derives_n g hg m' smid s_dirty ∧ ((nc_locked_mark ri 0 ∈ smid ∧ ∃ (pre : ℕ) (rest : ℕ) (spre : List (symbol T (NC_LockedNT g))) (spost : List (symbol T (locked_csg_of_noncontracting g hg).nt)) (j : ℕ), m' + 1 = pre + 1 + rest ∧ NC_locked_derives_n g hg pre smid spre ∧ CS_transforms (locked_csg_of_noncontracting g hg) spre spost ∧ NC_locked_derives_n g hg rest spost s_clean ∧ j < r.output_string.length ∧ nc_locked_mark ri 0 ∈ spre ∧ nc_locked_mark ri 0 ∉ spost ∧ nc_locked_out ri j (r.output_string.getD j (symbol.nonterminal r.input_N)) ∈ spost ∧ have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; (pattern.length = 1 ∧ ∃ (eu : List (symbol T (NC_LockedNT g))) (ev : List (symbol T (NC_LockedNT g))), spre = eu ++ [nc_locked_mark ri 0] ++ ev ∧ spost = eu ++ nc_locked_outputFrom ri r.output_string dflt 0 ++ ev) ∨ 1 < pattern.length ∧ ∃ (eu : List (symbol T (NC_LockedNT g))) (ev : List (symbol T (NC_LockedNT g))), spre = eu ++ [nc_locked_mark ri 0] ++ nc_locked_outputSuffix ri r.output_string dflt 1 ++ ev ∧ spost = eu ++ [nc_locked_out ri 0 (r.output_string.getD 0 dflt)] ++ nc_locked_outputSuffix ri r.output_string dflt 1 ++ ev) ∨ have target := u ++ List.map nc_locked_liftSym r.output_string ++ v; CS_derives (locked_csg_of_noncontracting g hg) smid target ∧ nc_locked_is_clean g target ∧ NC_locked_clean_macro_derives_n g hg 1 s_start target)

First-step dichotomy with the retained branch expanded to the local shape of the later emit step. This is the form needed by the eventual grouping argument: the branch where the boundary marker survives the first dirty step now carries the exact source and target decomposition of the step that finally removes that marker.

theorem nc_locked_dirty_interval_first_step_emit_shape_or_macro_prefix_with_added_mark_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_start s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hstart : CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after) (hclean_start : nc_locked_is_clean g s_start) (hdirty_after : ¬nc_locked_is_clean g s_after) (hmid : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hdirty : ¬nc_locked_is_clean g s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) : ∃ (ri : ℕ) (r : grule T g.nt) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))) (m' : ℕ) (smid : List (symbol T (locked_csg_of_noncontracting g hg).nt)), (ri, r) ∈ (List.range g.rules.length).zip g.rules ∧ (have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; s_start = u ++ [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v ∧ s_after = u ++ [nc_locked_mark ri 0] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v) ∧ m = m' + 1 ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_after smid ∧ ¬nc_locked_is_clean g smid ∧ NC_locked_dirty_derives_n g hg m' smid s_dirty ∧ (∀ (targetRi targetK : ℕ), nc_locked_mark targetRi targetK ∈ smid → nc_locked_mark targetRi targetK ∉ s_after → ∃ (simRi : ℕ) (grule : grule T g.nt), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ targetRi = simRi ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; targetK < pattern.length ∧ (targetK = 0 ∨ simRi = ri ∧ targetK = 1)) ∧ ((nc_locked_mark ri 0 ∈ smid ∧ ∃ (pre : ℕ) (rest : ℕ) (spre : List (symbol T (NC_LockedNT g))) (spost : List (symbol T (locked_csg_of_noncontracting g hg).nt)) (j : ℕ), m' + 1 = pre + 1 + rest ∧ NC_locked_derives_n g hg pre smid spre ∧ CS_transforms (locked_csg_of_noncontracting g hg) spre spost ∧ NC_locked_derives_n g hg rest spost s_clean ∧ j < r.output_string.length ∧ nc_locked_mark ri 0 ∈ spre ∧ nc_locked_mark ri 0 ∉ spost ∧ nc_locked_out ri j (r.output_string.getD j (symbol.nonterminal r.input_N)) ∈ spost ∧ have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; (pattern.length = 1 ∧ ∃ (eu : List (symbol T (NC_LockedNT g))) (ev : List (symbol T (NC_LockedNT g))), spre = eu ++ [nc_locked_mark ri 0] ++ ev ∧ spost = eu ++ nc_locked_outputFrom ri r.output_string dflt 0 ++ ev) ∨ 1 < pattern.length ∧ ∃ (eu : List (symbol T (NC_LockedNT g))) (ev : List (symbol T (NC_LockedNT g))), spre = eu ++ [nc_locked_mark ri 0] ++ nc_locked_outputSuffix ri r.output_string dflt 1 ++ ev ∧ spost = eu ++ [nc_locked_out ri 0 (r.output_string.getD 0 dflt)] ++ nc_locked_outputSuffix ri r.output_string dflt 1 ++ ev) ∨ have target := u ++ List.map nc_locked_liftSym r.output_string ++ v; CS_derives (locked_csg_of_noncontracting g hg) smid target ∧ nc_locked_is_clean g target ∧ NC_locked_clean_macro_derives_n g hg 1 s_start target)

First-step dichotomy plus the marker-introduction invariant for that same first dirty step. In the retained branch this keeps the later emit-step shape, while also recording that the first dirty step can only introduce a fresh phase-0 marker or the phase-1 marker for the boundary simulation.

theorem nc_locked_dirty_interval_first_step_base_one_mark_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_start s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hstart : CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after) (hclean_start : nc_locked_is_clean g s_start) (hdirty_after : ¬nc_locked_is_clean g s_after) (hmid : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hdirty : ¬nc_locked_is_clean g s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) : ∃ (ri : ℕ) (r : grule T g.nt) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))) (m' : ℕ) (smid : List (symbol T (locked_csg_of_noncontracting g hg).nt)), (ri, r) ∈ (List.range g.rules.length).zip g.rules ∧ (have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; s_start = u ++ [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v ∧ s_after = u ++ [nc_locked_mark ri 0] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v) ∧ m = m' + 1 ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_after smid ∧ ¬nc_locked_is_clean g smid ∧ NC_locked_dirty_derives_n g hg m' smid s_dirty ∧ (nc_locked_mark ri 1 ∈ smid → have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; 1 < pattern.length ∧ ∃ cr ∈ (locked_csg_of_noncontracting g hg).rules, cr.context_left = [nc_locked_mark ri 0] ∧ cr.input_nonterminal = nc_locked_symToNT (pattern.getD 1 dflt) ∧ cr.context_right = List.map nc_locked_liftSym (List.drop 2 pattern) ∧ cr.output_string = [nc_locked_mark ri 1])

Dirty-interval first-step data specialized to the case where the step creates the boundary simulation's phase-1 marker. This identifies that branch as the first continuation marking rule of the same original production.

theorem nc_locked_dirty_interval_first_step_macro_or_base_one_or_new_zero {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_start s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hstart : CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after) (hclean_start : nc_locked_is_clean g s_start) (hdirty_after : ¬nc_locked_is_clean g s_after) (hmid : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hdirty : ¬nc_locked_is_clean g s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) : ∃ (ri : ℕ) (r : grule T g.nt) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))) (m' : ℕ) (smid : List (symbol T (locked_csg_of_noncontracting g hg).nt)), (ri, r) ∈ (List.range g.rules.length).zip g.rules ∧ (have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; s_start = u ++ [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v ∧ s_after = u ++ [nc_locked_mark ri 0] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v) ∧ m = m' + 1 ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_after smid ∧ ¬nc_locked_is_clean g smid ∧ NC_locked_dirty_derives_n g hg m' smid s_dirty ∧ ((have target := u ++ List.map nc_locked_liftSym r.output_string ++ v; CS_derives (locked_csg_of_noncontracting g hg) smid target ∧ nc_locked_is_clean g target ∧ NC_locked_clean_macro_derives_n g hg 1 s_start target) ∨ (nc_locked_mark ri 0 ∈ smid ∧ nc_locked_mark ri 1 ∈ smid ∧ have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; 1 < pattern.length ∧ smid = u ++ [nc_locked_mark ri 0] ++ [nc_locked_mark ri 1] ++ List.map nc_locked_liftSym (List.drop 2 pattern) ++ v) ∨ nc_locked_mark ri 0 ∈ smid ∧ nc_locked_mark ri 1 ∉ smid ∧ ∀ (targetRi targetK : ℕ), nc_locked_mark targetRi targetK ∈ smid → nc_locked_mark targetRi targetK ∉ s_after → ∃ (grule : grule T g.nt), (targetRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ targetK = 0 ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; targetK < pattern.length)

Full first-step trichotomy for a dirty interval opened from a clean form. Either the first dirty-to-dirty step already gives the complete one-step clean macro pref, or it advances the boundary simulation from phase 0 to phase 1 with exact target shape, or it leaves the boundary phase-1 marker absent and any newly introduced marker is a nested phase-0 marker.

theorem nc_locked_dirty_interval_first_step_macro_or_base_one_or_fresh_zero {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {m : ℕ} {s_start s_after s_dirty s_clean : List (symbol T (NC_LockedNT g))} (hstart : CS_transforms (locked_csg_of_noncontracting g hg) s_start s_after) (hclean_start : nc_locked_is_clean g s_start) (hdirty_after : ¬nc_locked_is_clean g s_after) (hmid : NC_locked_dirty_derives_n g hg m s_after s_dirty) (hdirty : ¬nc_locked_is_clean g s_dirty) (hreturn : CS_transforms (locked_csg_of_noncontracting g hg) s_dirty s_clean) (hclean : nc_locked_is_clean g s_clean) : ∃ (ri : ℕ) (r : grule T g.nt) (u : List (symbol T (NC_LockedNT g))) (v : List (symbol T (NC_LockedNT g))) (m' : ℕ) (smid : List (symbol T (locked_csg_of_noncontracting g hg).nt)), (ri, r) ∈ (List.range g.rules.length).zip g.rules ∧ (have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; have dflt := symbol.nonterminal r.input_N; s_start = u ++ [nc_locked_liftSym (pattern.getD 0 dflt)] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v ∧ s_after = u ++ [nc_locked_mark ri 0] ++ List.map nc_locked_liftSym (List.drop 1 pattern) ++ v) ∧ m = m' + 1 ∧ CS_transforms (locked_csg_of_noncontracting g hg) s_after smid ∧ ¬nc_locked_is_clean g smid ∧ NC_locked_dirty_derives_n g hg m' smid s_dirty ∧ ((have target := u ++ List.map nc_locked_liftSym r.output_string ++ v; CS_derives (locked_csg_of_noncontracting g hg) smid target ∧ nc_locked_is_clean g target ∧ NC_locked_clean_macro_derives_n g hg 1 s_start target) ∨ (nc_locked_mark ri 0 ∈ smid ∧ nc_locked_mark ri 1 ∈ smid ∧ have pattern := r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R; 1 < pattern.length ∧ smid = u ++ [nc_locked_mark ri 0] ++ [nc_locked_mark ri 1] ++ List.map nc_locked_liftSym (List.drop 2 pattern) ++ v) ∨ nc_locked_mark ri 0 ∈ smid ∧ nc_locked_mark ri 1 ∉ smid ∧ ∀ (targetRi targetK : ℕ), nc_locked_mark targetRi targetK ∈ smid → nc_locked_mark targetRi targetK ∉ s_after → targetK = 0 ∧ ∃ (grule : grule T g.nt), (targetRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ have pattern := grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R; 0 < pattern.length)

Retained-branch version of the first-step trichotomy with fresh markers normalized. If the boundary simulation has not advanced to phase 1, then any marker created by the first dirty step is a phase-0 marker for a genuine simulation rule whose input pattern is nonempty.

theorem nc_locked_clean_macro_trace_terminal_mem_grammar_language {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {w : List T} (h : NC_locked_clean_macro_derives_n g hg n [symbol.nonterminal (NC_LockedNT.orig g.initial)] (List.map symbol.terminal w)) : w ∈ grammar_language g

Terminal words reached by locked clean macro traces are generated by the original non-contracting grammar.

Backward direction helpers

def nc_proj_sym {T : Type} (g : grammar T) : symbol T (NC_NT g) → symbol T g.nt

Projection from extended grammar symbols to original grammar symbols. For clean forms (no aux nonterminals), this is the natural "un-lifting" map.

Equations

• nc_proj_sym g (symbol.terminal t) = symbol.terminal t
• nc_proj_sym g (symbol.nonterminal (Sum.inl n)) = symbol.nonterminal n
• nc_proj_sym g (symbol.nonterminal (Sum.inr (Sum.inl t))) = symbol.terminal t
• nc_proj_sym g (symbol.nonterminal (Sum.inr (Sum.inr val))) = symbol.nonterminal g.initial

def nc_proj {T : Type} (g : grammar T) (s : List (symbol T (NC_NT g))) : List (symbol T g.nt)

Projection on lists: apply nc_proj_sym pointwise.

Equations

• nc_proj g s = List.map (nc_proj_sym g) s

theorem nc_proj_liftSym {T : Type} (g : grammar T) (s : symbol T g.nt) : nc_proj_sym g (nc_liftSym s) = s

proj ∘ liftSym = id: projecting a lifted symbol recovers the original.

def nc_is_clean {T : Type} (g : grammar T) (s : List (symbol T (NC_NT g))) : Prop

A sentential form is "clean" if it has no auxiliary nonterminals.

Equations

• nc_is_clean g s = ∀ x ∈ s, ∀ (p : ℕ × ℕ), x ≠ symbol.nonterminal (Sum.inr (Sum.inr p))

theorem nc_is_clean_of_subset {T : Type} (g : grammar T) {s t : List (symbol T (NC_NT g))} (hclean : nc_is_clean g t) (hsub : ∀ x ∈ s, x ∈ t) : nc_is_clean g s

Cleanliness is preserved by taking a sublist in the membership sense.

theorem nc_liftSym_clean {T : Type} (g : grammar T) (s : symbol T g.nt) : nc_is_clean g [nc_liftSym s]

Lifted original symbols are clean.

theorem nc_map_liftSym_clean {T : Type} (g : grammar T) (s : List (symbol T g.nt)) : nc_is_clean g (List.map nc_liftSym s)

Lifted original sentential forms are clean.

theorem nc_not_clean_iff_exists_aux {T : Type} (g : grammar T) (s : List (symbol T (NC_NT g))) : ¬nc_is_clean g s ↔ ∃ (ri : ℕ) (k : ℕ), nc_aux ri k ∈ s

Failure of cleanliness is exactly the presence of an auxiliary nonterminal.

theorem nc_symToNT_ne_aux {T : Type} (g : grammar T) (s : symbol T g.nt) (p : ℕ × ℕ) : nc_symToNT s ≠ Sum.inr (Sum.inr p)

Original symbols never lift to auxiliary nonterminals.

theorem nc_proj_initial {T : Type} (g : grammar T) : nc_proj g [symbol.nonterminal (Sum.inl g.initial)] = [symbol.nonterminal g.initial]

Projection of the initial symbol.

theorem nc_proj_terminal {T : Type} (g : grammar T) (w : List T) : nc_proj g (List.map symbol.terminal w) = List.map symbol.terminal w

Projection of a terminal string.

theorem CS_transform_new_symbol_mem_rule_output {T : Type} {g : CS_grammar T} {s₁ s₂ : List (symbol T g.nt)} {x : symbol T g.nt} (h : CS_transforms g s₁ s₂) (hx₂ : x ∈ s₂) (hx₁ : x ∉ s₁) : ∃ r ∈ g.rules, x ∈ r.output_string

If a CS step creates a symbol that was not present before the step, that symbol must come from the selected rule's output string.

theorem nc_clean_step_dirty_new_aux {T : Type} (g : grammar T) {s₁ s₂ : List (symbol T (NC_NT g))} (hclean : nc_is_clean g s₁) (hdirty : ¬nc_is_clean g s₂) : ∃ (ri : ℕ) (k : ℕ), nc_aux ri k ∈ s₂ ∧ nc_aux ri k ∉ s₁

If a clean step becomes dirty, some auxiliary was newly introduced.

theorem nc_rule_output_aux_is_phase1 {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {cr : csrule T (NC_NT g)} (hcr : cr ∈ (csg_of_noncontracting g hg).rules) {ri k : ℕ} (haux : nc_aux ri k ∈ cr.output_string) : ∃ (simRi : ℕ) (grule : grule T g.nt) (phaseK : ℕ), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ phaseK < (grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R).length - 1 ∧ cr.output_string = [nc_aux simRi phaseK]

The only rules of the non-contracting simulation whose output string contains an auxiliary nonterminal are phase-1 marking rules.

theorem nc_rule_output_aux_phase1_rule_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {cr : csrule T (NC_NT g)} (hcr : cr ∈ (csg_of_noncontracting g hg).rules) {ri k : ℕ} (haux : nc_aux ri k ∈ cr.output_string) : ∃ (simRi : ℕ) (grule : grule T g.nt) (phaseK : ℕ), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ phaseK < (grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R).length - 1 ∧ cr = { context_left := List.map (nc_aux simRi) (List.range phaseK), input_nonterminal := nc_symToNT ((grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R).getD phaseK (symbol.nonterminal grule.input_N)), context_right := List.map nc_liftSym (List.drop (phaseK + 1) (grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R)), output_string := [nc_aux simRi phaseK] }

Stronger form of nc_rule_output_aux_is_phase1: if a constructed rule outputs an auxiliary, the whole selected rule is exactly the corresponding phase-1 rule.

theorem nc_clean_step_dirty_phase1_zero_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_NT g))} (h : CS_transforms (csg_of_noncontracting g hg) s₁ s₂) (hclean : nc_is_clean g s₁) (hdirty : ¬nc_is_clean g s₂) : ∃ (simRi : ℕ) (grule : grule T g.nt) (u : List (symbol T (NC_NT g))) (v : List (symbol T (NC_NT g))), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ 0 < (grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R).length - 1 ∧ s₁ = u ++ [symbol.nonterminal (nc_symToNT ((grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R).getD 0 (symbol.nonterminal grule.input_N)))] ++ List.map nc_liftSym (List.drop 1 (grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R)) ++ v ∧ s₂ = u ++ [nc_aux simRi 0] ++ List.map nc_liftSym (List.drop 1 (grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R)) ++ v

A clean-to-dirty step is specifically phase 0 of a simulated rule. Positive phase-1 steps have an auxiliary in their left context, so they cannot apply to a clean source.

theorem nc_rule_input_aux_phase2_rest_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {cr : csrule T (NC_NT g)} (hcr : cr ∈ (csg_of_noncontracting g hg).rules) {ri k : ℕ} (hinput : cr.input_nonterminal = Sum.inr (Sum.inr (ri, k))) : ∃ (simRi : ℕ) (grule : grule T g.nt) (phaseK : ℕ), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ phaseK < (grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R).length - 1 ∧ cr = { context_left := List.map (nc_aux simRi) (List.range phaseK), input_nonterminal := Sum.inr (Sum.inr (simRi, phaseK)), context_right := List.map nc_liftSym (List.drop (phaseK + 1) grule.output_string), output_string := [nc_liftSym (grule.output_string.getD phaseK (symbol.nonterminal grule.input_N))] }

If a selected constructed rule rewrites an auxiliary nonterminal, then it is one of the right-to-left phase-2 cleanup rules.

theorem nc_dirty_step_clean_phase2_zero_shape {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_NT g))} (h : CS_transforms (csg_of_noncontracting g hg) s₁ s₂) (hdirty : ¬nc_is_clean g s₁) (hclean : nc_is_clean g s₂) : ∃ (simRi : ℕ) (grule : grule T g.nt) (u : List (symbol T (NC_NT g))) (v : List (symbol T (NC_NT g))), (simRi, grule) ∈ (List.range g.rules.length).zip g.rules ∧ 0 < (grule.input_L ++ [symbol.nonterminal grule.input_N] ++ grule.input_R).length - 1 ∧ s₁ = u ++ [nc_aux simRi 0] ++ List.map nc_liftSym (List.drop 1 grule.output_string) ++ v ∧ s₂ = u ++ [nc_liftSym (grule.output_string.getD 0 (symbol.nonterminal grule.input_N))] ++ List.map nc_liftSym (List.drop 1 grule.output_string) ++ v

A dirty-to-clean step must be the final phase-2 cleanup rule at phase 0. Positive phase-2 cleanup rules preserve earlier auxiliaries in their left context, so their target cannot be clean.

theorem nc_clean_step_grammar_derives {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_NT g))} (h : CS_transforms (csg_of_noncontracting g hg) s₁ s₂) (h₁ : nc_is_clean g s₁) (h₂ : nc_is_clean g s₂) : grammar_derives g (nc_proj g s₁) (nc_proj g s₂)

inductive CS_derives_n {T : Type} (g : CS_grammar T) : ℕ → List (symbol T g.nt) → List (symbol T g.nt) → Prop

Inductive step-count version of CS_derives.

• zero {T : Type} {g : CS_grammar T} (s : List (symbol T g.nt)) : CS_derives_n g 0 s s
• step {T : Type} {g : CS_grammar T} {n : ℕ} {s₁ s₂ s₃ : List (symbol T g.nt)} : CS_transforms g s₁ s₂ → CS_derives_n g n s₂ s₃ → CS_derives_n g (n + 1) s₁ s₃

Clean reverse traces

The final reverse direction has two conceptual parts:

1. clean-to-clean steps project to derivations in the original grammar;
2. dirty auxiliary phases can be grouped into clean-to-clean macro steps.

The first part is captured below. The remaining work is the phase-grouping argument for derivations that temporarily contain nc_aux symbols.

inductive NC_clean_macro_step {T : Type} (g : grammar T) (hg : grammar_noncontracting g) : List (symbol T (NC_NT g)) → List (symbol T (NC_NT g)) → Prop

Clean macro steps in the constructed grammar. The second constructor is the intended endpoint of dirty-phase grouping: one complete auxiliary simulation of an original non-contracting rule, under arbitrary surrounding context.

• clean {T : Type} {g : grammar T} {hg : grammar_noncontracting g} {s₁ s₂ : List (symbol T (csg_of_noncontracting g hg).nt)} : CS_transforms (csg_of_noncontracting g hg) s₁ s₂ → nc_is_clean g s₁ → nc_is_clean g s₂ → NC_clean_macro_step g hg s₁ s₂
• sim {T : Type} {g : grammar T} {hg : grammar_noncontracting g} {ri : ℕ} {r : grule T g.nt} {u v : List (symbol T (NC_NT g))} : (ri, r) ∈ (List.range g.rules.length).zip g.rules → NC_clean_macro_step g hg (u ++ List.map nc_liftSym (r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R) ++ v) (u ++ List.map nc_liftSym r.output_string ++ v)

theorem nc_clean_macro_step_grammar_derives {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {s₁ s₂ : List (symbol T (NC_NT g))} (h : NC_clean_macro_step g hg s₁ s₂) : grammar_derives g (nc_proj g s₁) (nc_proj g s₂)

Every clean macro step projects to an unrestricted derivation in the original grammar.

inductive NC_clean_macro_derives_n {T : Type} (g : grammar T) (hg : grammar_noncontracting g) : ℕ → List (symbol T (NC_NT g)) → List (symbol T (NC_NT g)) → Prop

Step-counted traces of clean macro steps.

• zero {T : Type} {g : grammar T} {hg : grammar_noncontracting g} {s : List (symbol T (NC_NT g))} : nc_is_clean g s → NC_clean_macro_derives_n g hg 0 s s
• step {T : Type} {g : grammar T} {hg : grammar_noncontracting g} {n : ℕ} {s₁ s₂ s₃ : List (symbol T (NC_NT g))} : NC_clean_macro_step g hg s₁ s₂ → NC_clean_macro_derives_n g hg n s₂ s₃ → NC_clean_macro_derives_n g hg (n + 1) s₁ s₃

theorem nc_clean_macro_trace_grammar_derives {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_NT g))} (h : NC_clean_macro_derives_n g hg n s₁ s₂) : grammar_derives g (nc_proj g s₁) (nc_proj g s₂)

Clean macro traces project to unrestricted derivations in the original grammar.

inductive NC_clean_derives_n {T : Type} (g : grammar T) (hg : grammar_noncontracting g) : ℕ → List (symbol T (NC_NT g)) → List (symbol T (NC_NT g)) → Prop

A finite CS derivation trace all of whose adjacent endpoints are clean.

• zero {T : Type} {g : grammar T} {hg : grammar_noncontracting g} {s : List (symbol T (NC_NT g))} : nc_is_clean g s → NC_clean_derives_n g hg 0 s s
• step {T : Type} {g : grammar T} {hg : grammar_noncontracting g} {n : ℕ} {s₁ s₂ : List (symbol T (csg_of_noncontracting g hg).nt)} {s₃ : List (symbol T (NC_NT g))} : CS_transforms (csg_of_noncontracting g hg) s₁ s₂ → nc_is_clean g s₁ → nc_is_clean g s₂ → NC_clean_derives_n g hg n s₂ s₃ → NC_clean_derives_n g hg (n + 1) s₁ s₃

theorem nc_clean_trace_grammar_derives {T : Type} (g : grammar T) (hg : grammar_noncontracting g) {n : ℕ} {s₁ s₂ : List (symbol T (NC_NT g))} (h : NC_clean_derives_n g hg n s₁ s₂) : grammar_derives g (nc_proj g s₁) (nc_proj g s₂)

Clean CS traces project to unrestricted derivations in the original grammar.