Work-track completeness for Aho's row checker

For every semantic composite certificate, this module constructs the corresponding finite logical-slot trace. The constructions cover replacements, one- and two-slot shifts, pop frames, frame returns, and the final dispatch theorem producing WorkTraceAccepts.

theorem IndexedGrammar.Aho.WorkTrace.append {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) {q r s : WorkScanState g} {xs ys : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)} (h₁ : WorkTrace g cert q xs r) (h₂ : WorkTrace g cert r ys s) : WorkTrace g cert q (xs ++ ys) s

def IndexedGrammar.Aho.samePrefixRows {T : Type} (g : IndexedGrammar T) (xs : List (WorkSym g)) : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)

Equations

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

@[simp]

theorem IndexedGrammar.Aho.samePrefixRows_old {T : Type} (g : IndexedGrammar T) (xs : List (WorkSym g)) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) (samePrefixRows g xs) = List.map inactive xs

@[simp]

theorem IndexedGrammar.Aho.samePrefixRows_new {T : Type} (g : IndexedGrammar T) (xs : List (WorkSym g)) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) (samePrefixRows g xs) = List.map inactive xs

theorem IndexedGrammar.Aho.trace_same_prefix {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (h : WorkHistory g) (xs : List (WorkSym g)) (henabled : CertEnabled g cert) : WorkTrace g cert { phase := WorkPhase.prefix, history := h, oldEnded := false, newEnded := false } (samePrefixRows g xs) { phase := WorkPhase.prefix, history := historySame h xs, oldEnded := false, newEnded := false }

theorem IndexedGrammar.Aho.trace_productive_boundary {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (alpha : List (WorkSym g)) (henabled : CertEnabled g cert) (hproductive : cert.productive = true) : ∃ (rows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)) (h : WorkHistory g), WorkTrace g cert (initialWorkScan g) rows { phase := WorkPhase.stage1, history := h, oldEnded := false, newEnded := false } ∧ List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) rows = List.map inactive (alpha ++ [WorkSym.dollar]) ∧ List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) rows = List.map inactive (markProductivePrefix alpha ++ [WorkSym.dollar])

theorem IndexedGrammar.Aho.trace_plain_boundary {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (alpha : List (WorkSym g)) (henabled : CertEnabled g cert) (hproductive : cert.productive = false) : ∃ (rows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)) (h : WorkHistory g), WorkTrace g cert (initialWorkScan g) rows { phase := WorkPhase.stage1, history := h, oldEnded := false, newEnded := false } ∧ List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) rows = List.map inactive (alpha ++ [WorkSym.dollar]) ∧ List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) rows = List.map inactive (alpha ++ [WorkSym.dollar])

def IndexedGrammar.Aho.sameSuffixRows {T✝ : Type} {g : IndexedGrammar T✝} (xs : List (Option (WorkSlot g))) : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)

Equations

• IndexedGrammar.Aho.sameSuffixRows xs = List.map (fun (x : Option (IndexedGrammar.Aho.WorkSlot g)) => (x, x, IndexedGrammar.Aho.WorkPhase.suffixSame)) xs

theorem IndexedGrammar.Aho.trace_same_suffix_padded {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (h : WorkHistory g) (beta : List (WorkSym g)) (k : ℕ) (hloop : ∀ (h : WorkHistory g) (x : Option (WorkSlot g)), InactiveOpt x → WorkEdge g cert WorkPhase.suffixSame WorkPhase.suffixSame h x x) : ∃ (result : WorkScanState g), WorkTrace g cert { phase := WorkPhase.suffixSame, history := h, oldEnded := false, newEnded := false } (sameSuffixRows (List.map inactive beta ++ List.replicate k none)) result ∧ result.phase = WorkPhase.suffixSame

theorem IndexedGrammar.Aho.accepts_replace_one {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (prefixRows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)) (h : WorkHistory g) (hprefix : WorkTrace g cert (initialWorkScan g) prefixRows { phase := WorkPhase.stage1, history := h, oldEnded := false, newEnded := false }) (oldFocus newFocus : WorkSym g) (beta : List (WorkSym g)) (k : ℕ) (hfocus : ∀ (h : WorkHistory g), WorkEdge g cert WorkPhase.stage1 WorkPhase.suffixSame h (active oldFocus) (active newFocus)) (hloop : ∀ (h : WorkHistory g) (x : Option (WorkSlot g)), InactiveOpt x → WorkEdge g cert WorkPhase.suffixSame WorkPhase.suffixSame h x x) : WorkTraceAccepts g cert (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) prefixRows ++ [active oldFocus] ++ List.map inactive beta ++ List.replicate k none) (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) prefixRows ++ [active newFocus] ++ List.map inactive beta ++ List.replicate k none)

theorem IndexedGrammar.Aho.accepts_plainTerminal {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {A : g.nt} {a : T} {alpha beta : List (WorkSym g)} (k : ℕ) (hrule : AugTerminal g A a) : WorkTraceAccepts g (CompositeCert.plainTerminal A a) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.plain A)] ++ List.map inactive beta ++ List.replicate k none) (List.map inactive (markProductivePrefix alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.terminal a)] ++ List.map inactive beta ++ List.replicate k none)

theorem IndexedGrammar.Aho.accepts_plainPushSkip {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {A B : g.nt} {f : g.flag} {alpha beta : List (WorkSym g)} (k : ℕ) (hrule : AugPush g A B f) : WorkTraceAccepts g (CompositeCert.plainPushSkip A B f) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.plain A)] ++ List.map inactive beta ++ List.replicate k none) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.plain B)] ++ List.map inactive beta ++ List.replicate k none)

def IndexedGrammar.Aho.shift1Rows {T : Type} (g : IndexedGrammar T) (prev : Option (WorkSlot g)) : List (Option (WorkSlot g)) → List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)

Equations

• IndexedGrammar.Aho.shift1Rows g prev [] = [(none, prev, IndexedGrammar.Aho.WorkPhase.suffixPlus1)]
• IndexedGrammar.Aho.shift1Rows g prev (x_1 :: xs) = (x_1, prev, IndexedGrammar.Aho.WorkPhase.suffixPlus1) :: IndexedGrammar.Aho.shift1Rows g x_1 xs

@[simp]

theorem IndexedGrammar.Aho.shift1Rows_old {T : Type} (g : IndexedGrammar T) (prev : Option (WorkSlot g)) (xs : List (Option (WorkSlot g))) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) (shift1Rows g prev xs) = xs ++ [none]

@[simp]

theorem IndexedGrammar.Aho.shift1Rows_new {T : Type} (g : IndexedGrammar T) (prev : Option (WorkSlot g)) (xs : List (Option (WorkSlot g))) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) (shift1Rows g prev xs) = prev :: xs

def IndexedGrammar.Aho.plus2ShiftRows {T : Type} (g : IndexedGrammar T) (prev2 prev1 : Option (WorkSlot g)) : List (Option (WorkSlot g)) → List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)

Equations

• IndexedGrammar.Aho.plus2ShiftRows g prev2 prev1 [] = [(none, prev2, IndexedGrammar.Aho.WorkPhase.suffixPlus2), (none, prev1, IndexedGrammar.Aho.WorkPhase.suffixPlus2)]
• IndexedGrammar.Aho.plus2ShiftRows g prev2 prev1 (x_1 :: xs) = (x_1, prev2, IndexedGrammar.Aho.WorkPhase.suffixPlus2) :: IndexedGrammar.Aho.plus2ShiftRows g prev1 x_1 xs

@[simp]

theorem IndexedGrammar.Aho.plus2ShiftRows_old {T : Type} (g : IndexedGrammar T) (prev2 prev1 : Option (WorkSlot g)) (xs : List (Option (WorkSlot g))) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) (plus2ShiftRows g prev2 prev1 xs) = xs ++ [none, none]

@[simp]

theorem IndexedGrammar.Aho.plus2ShiftRows_new {T : Type} (g : IndexedGrammar T) (prev2 prev1 : Option (WorkSlot g)) (xs : List (Option (WorkSlot g))) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) (plus2ShiftRows g prev2 prev1 xs) = prev2 :: prev1 :: xs

def IndexedGrammar.Aho.plus2FromRows {T : Type} (g : IndexedGrammar T) (inserted1 inserted2 : WorkSym g) : List (Option (WorkSlot g)) → List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)

Equations

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

@[simp]

theorem IndexedGrammar.Aho.plus2FromRows_old {T : Type} (g : IndexedGrammar T) (inserted1 inserted2 : WorkSym g) (xs : List (Option (WorkSlot g))) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) (plus2FromRows g inserted1 inserted2 xs) = xs ++ [none, none]

@[simp]

theorem IndexedGrammar.Aho.plus2FromRows_new {T : Type} (g : IndexedGrammar T) (inserted1 inserted2 : WorkSym g) (xs : List (Option (WorkSlot g))) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) (plus2FromRows g inserted1 inserted2 xs) = active inserted1 :: inactive inserted2 :: xs

def IndexedGrammar.Aho.nextOr {X : Type u_1} (fallback : X) : List X → X

Equations

• IndexedGrammar.Aho.nextOr fallback [] = fallback
• IndexedGrammar.Aho.nextOr fallback (x_1 :: tail) = x_1

def IndexedGrammar.Aho.popChainRows {T : Type} (g : IndexedGrammar T) (R : CFlag g) (d : IndexMark) : List (WorkSym g) → List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)

Equations

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

@[simp]

theorem IndexedGrammar.Aho.popChainRows_old {T : Type} (g : IndexedGrammar T) (R : CFlag g) (d : IndexMark) (beta : List (WorkSym g)) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) (popChainRows g R d beta) = List.map inactive beta ++ [inactive (WorkSym.index R d)]

theorem IndexedGrammar.Aho.popChainRows_new {T : Type} (g : IndexedGrammar T) (R : CFlag g) (d : IndexMark) (beta : List (WorkSym g)) : inactive (nextOr (WorkSym.index R d.markUsed) beta) :: List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) (popChainRows g R d beta) = List.map inactive beta ++ [inactive (WorkSym.index R d.markUsed), inactive WorkSym.dollar]

theorem IndexedGrammar.Aho.accepts_pop {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (R : CFlag g) (d : IndexMark) (alpha beta gamma : List (WorkSym g)) (oldFocus newFocus : WorkSym g) (k : ℕ) (henabled : CertEnabled g cert) (hproductive : cert.productive = false) (hfree : IndexFree beta) (hfocus : ∀ (h : WorkHistory g), WorkEdge g cert WorkPhase.stage1 WorkPhase.popBeta h (active oldFocus) (inactive (nextOr (WorkSym.index R d.markUsed) beta))) (hloopBeta : ∀ (h : WorkHistory g) (old new : Option (WorkSlot g)), InactiveNonIndex old → h.new1 = some old → InactiveOpt new → WorkEdge g cert WorkPhase.popBeta WorkPhase.popBeta h old new) (hfinish : ∀ (h : WorkHistory g), h.new1 = some (inactive (WorkSym.index R d.markUsed)) → WorkEdge g cert WorkPhase.popBeta WorkPhase.stage2 h (inactive (WorkSym.index R d)) (inactive WorkSym.dollar)) (hnewFocus : ∀ (h : WorkHistory g) (old : Option (WorkSlot g)), InactiveOpt old → WorkEdge g cert WorkPhase.stage2 WorkPhase.stage3 h old (active newFocus)) (hclose : ∀ (h : WorkHistory g) (old : Option (WorkSlot g)), InactiveOpt old → WorkEdge g cert WorkPhase.stage3 WorkPhase.suffixPlus2 h old (inactive WorkSym.close)) (hloop2 : ∀ (h : WorkHistory g) (old new : Option (WorkSlot g)), plus2Suffix h old new → WorkEdge g cert WorkPhase.suffixPlus2 WorkPhase.suffixPlus2 h old new) : WorkTraceAccepts g cert (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active oldFocus] ++ List.map inactive beta ++ [inactive (WorkSym.index R d)] ++ List.map inactive gamma ++ List.replicate (k + 2) none) (List.map inactive (alpha ++ [WorkSym.dollar] ++ beta ++ [WorkSym.index R d.markUsed, WorkSym.dollar]) ++ [active newFocus, inactive WorkSym.close] ++ List.map inactive gamma ++ List.replicate k none)

theorem IndexedGrammar.Aho.accepts_popPlain {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {R : CFlag g} {d : IndexMark} {A B : g.nt} {alpha beta gamma : List (WorkSym g)} (k : ℕ) (hrule : R A B = true) (hfree : IndexFree beta) : WorkTraceAccepts g (CompositeCert.popPlain R d A B) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.live A)] ++ List.map inactive beta ++ [inactive (WorkSym.index R d)] ++ List.map inactive gamma ++ List.replicate (k + 2) none) (List.map inactive (alpha ++ [WorkSym.dollar] ++ beta ++ [WorkSym.index R d.markUsed, WorkSym.dollar]) ++ [active (WorkSym.plain B), inactive WorkSym.close] ++ List.map inactive gamma ++ List.replicate k none)

theorem IndexedGrammar.Aho.accepts_popLive {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {R : CFlag g} {d : IndexMark} {A B : g.nt} {alpha beta gamma : List (WorkSym g)} (k : ℕ) (hrule : R A B = true) (hlater : d.later = true) (hfree : IndexFree beta) : WorkTraceAccepts g (CompositeCert.popLive R d A B) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.live A)] ++ List.map inactive beta ++ [inactive (WorkSym.index R d)] ++ List.map inactive gamma ++ List.replicate (k + 2) none) (List.map inactive (alpha ++ [WorkSym.dollar] ++ beta ++ [WorkSym.index R d.markUsed, WorkSym.dollar]) ++ [active (WorkSym.live B), inactive WorkSym.close] ++ List.map inactive gamma ++ List.replicate k none)

def IndexedGrammar.Aho.plus1FromRows {T : Type} (g : IndexedGrammar T) (inserted : WorkSym g) : List (Option (WorkSlot g)) → List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)

Equations

• IndexedGrammar.Aho.plus1FromRows g inserted [] = [(none, IndexedGrammar.Aho.inactive inserted, IndexedGrammar.Aho.WorkPhase.suffixPlus1)]
• IndexedGrammar.Aho.plus1FromRows g inserted (x_1 :: xs) = (x_1, IndexedGrammar.Aho.inactive inserted, IndexedGrammar.Aho.WorkPhase.suffixPlus1) :: IndexedGrammar.Aho.shift1Rows g x_1 xs

def IndexedGrammar.Aho.firstPad {X : Type u_1} : List (Option X) → Option X

Equations

• IndexedGrammar.Aho.firstPad [] = none
• IndexedGrammar.Aho.firstPad (x_1 :: tail) = x_1

@[simp]

theorem IndexedGrammar.Aho.plus1FromRows_old {T : Type} (g : IndexedGrammar T) (inserted : WorkSym g) (xs : List (Option (WorkSlot g))) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) (plus1FromRows g inserted xs) = xs ++ [none]

@[simp]

theorem IndexedGrammar.Aho.plus1FromRows_new {T : Type} (g : IndexedGrammar T) (inserted : WorkSym g) (xs : List (Option (WorkSlot g))) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) (plus1FromRows g inserted xs) = inactive inserted :: xs

theorem IndexedGrammar.Aho.accepts_insert_one {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (prefixRows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)) (h : WorkHistory g) (hprefix : WorkTrace g cert (initialWorkScan g) prefixRows { phase := WorkPhase.stage1, history := h, oldEnded := false, newEnded := false }) (oldFocus newFocus inserted : WorkSym g) (beta : List (WorkSym g)) (k : ℕ) (hfocus : ∀ (h : WorkHistory g), WorkEdge g cert WorkPhase.stage1 WorkPhase.stage2 h (active oldFocus) (active newFocus)) (hinsert : ∀ (h : WorkHistory g), WorkEdge g cert WorkPhase.stage2 WorkPhase.suffixPlus1 h (firstPad (List.map inactive beta ++ List.replicate k none)) (inactive inserted)) (hloop : ∀ (h : WorkHistory g) (old new : Option (WorkSlot g)), plus1Suffix h old new → WorkEdge g cert WorkPhase.suffixPlus1 WorkPhase.suffixPlus1 h old new) : WorkTraceAccepts g cert (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) prefixRows ++ [active oldFocus] ++ List.map inactive beta ++ List.replicate (k + 1) none) (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) prefixRows ++ [active newFocus, inactive inserted] ++ List.map inactive beta ++ List.replicate k none)

@[simp]

theorem IndexedGrammar.Aho.firstPad_inactive_padded {T : Type} (g : IndexedGrammar T) (beta : List (WorkSym g)) (k : ℕ) : InactiveOpt (firstPad (List.map inactive beta ++ List.replicate k none))

theorem IndexedGrammar.Aho.firstPad_inactive_of_all {T : Type} (g : IndexedGrammar T) {xs : List (Option (WorkSlot g))} (hxs : ∀ x ∈ xs, InactiveOpt x) : InactiveOpt (firstPad xs)

@[simp]

theorem IndexedGrammar.Aho.length_markProductivePrefix {T : Type} (g : IndexedGrammar T) (alpha : List (WorkSym g)) : (markProductivePrefix alpha).length = alpha.length

theorem IndexedGrammar.Aho.paddedCursor_eq_append {T : Type} (g : IndexedGrammar T) (n : ℕ) (c : WorkCursor g) (hwork : c.word.length ≤ n * workWidth) : paddedWork n c.slots = List.map inactive c.left ++ [active c.focus] ++ List.map inactive c.right ++ List.replicate (n * workWidth - c.word.length) none

theorem IndexedGrammar.Aho.accepts_plainBinary {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {A B C : g.nt} {alpha beta : List (WorkSym g)} (k : ℕ) (hrule : AugBinary g A B C) : WorkTraceAccepts g (CompositeCert.plainBinary A B C) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.plain A)] ++ List.map inactive beta ++ List.replicate (k + 1) none) (List.map inactive (markProductivePrefix alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.plain B), inactive (WorkSym.plain C)] ++ List.map inactive beta ++ List.replicate k none)

theorem IndexedGrammar.Aho.accepts_plainPushUse {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {A B : g.nt} {f : g.flag} {alpha beta : List (WorkSym g)} (k : ℕ) (hrule : AugPush g A B f) : WorkTraceAccepts g (CompositeCert.plainPushUse A B f) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.plain A)] ++ List.map inactive beta ++ List.replicate (k + 1) none) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.live B), inactive (WorkSym.index (cflagBase g f) IndexMark.firstPending)] ++ List.map inactive beta ++ List.replicate k none)

theorem IndexedGrammar.Aho.accepts_liveBinaryBoth {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {A B C : g.nt} {alpha beta : List (WorkSym g)} {Z : WorkSym g} (k : ℕ) (hrule : AugBinary g A B C) : WorkTraceAccepts g (CompositeCert.liveBinaryBoth A B C) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.live A), inactive Z] ++ List.map inactive beta ++ List.replicate (k + 1) none) (List.map inactive (markProductivePrefix alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.live B), inactive (WorkSym.live C), inactive Z] ++ List.map inactive beta ++ List.replicate k none)

theorem IndexedGrammar.Aho.accepts_liveBinaryLeft {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {A B C : g.nt} {alpha beta : List (WorkSym g)} {Z : WorkSym g} (k : ℕ) (hrule : AugBinary g A B C) : WorkTraceAccepts g (CompositeCert.liveBinaryLeft A B C) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.live A), inactive Z] ++ List.map inactive beta ++ List.replicate (k + 1) none) (List.map inactive (markProductivePrefix alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.live B), inactive (WorkSym.plain C), inactive Z] ++ List.map inactive beta ++ List.replicate k none)

theorem IndexedGrammar.Aho.accepts_liveBinaryRight {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {A B C : g.nt} {alpha beta : List (WorkSym g)} {Z : WorkSym g} (k : ℕ) (hrule : AugBinary g A B C) : WorkTraceAccepts g (CompositeCert.liveBinaryRight A B C) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.live A), inactive Z] ++ List.map inactive beta ++ List.replicate (k + 1) none) (List.map inactive (markProductivePrefix alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.plain B), inactive (WorkSym.live C), inactive Z] ++ List.map inactive beta ++ List.replicate k none)

theorem IndexedGrammar.Aho.accepts_livePushFresh {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {A B : g.nt} {f : g.flag} {alpha beta : List (WorkSym g)} {Z : WorkSym g} (k : ℕ) (hrule : AugPush g A B f) : WorkTraceAccepts g (CompositeCert.livePushFresh A B f) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.live A), inactive Z] ++ List.map inactive beta ++ List.replicate (k + 1) none) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.live B), inactive (WorkSym.index (cflagBase g f) IndexMark.laterPending), inactive Z] ++ List.map inactive beta ++ List.replicate k none)

theorem IndexedGrammar.Aho.accepts_replace_two {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (prefixRows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)) (h : WorkHistory g) (hprefix : WorkTrace g cert (initialWorkScan g) prefixRows { phase := WorkPhase.stage1, history := h, oldEnded := false, newEnded := false }) (oldFocus newFocus oldNext newNext : WorkSym g) (beta : List (WorkSym g)) (k : ℕ) (hfocus : ∀ (h : WorkHistory g), WorkEdge g cert WorkPhase.stage1 WorkPhase.stage2 h (active oldFocus) (active newFocus)) (hnext : ∀ (h : WorkHistory g), WorkEdge g cert WorkPhase.stage2 WorkPhase.suffixSame h (inactive oldNext) (inactive newNext)) (hloop : ∀ (h : WorkHistory g) (x : Option (WorkSlot g)), InactiveOpt x → WorkEdge g cert WorkPhase.suffixSame WorkPhase.suffixSame h x x) : WorkTraceAccepts g cert (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) prefixRows ++ [active oldFocus, inactive oldNext] ++ List.map inactive beta ++ List.replicate k none) (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) prefixRows ++ [active newFocus, inactive newNext] ++ List.map inactive beta ++ List.replicate k none)

theorem IndexedGrammar.Aho.accepts_livePushCompress {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {A B : g.nt} {f : g.flag} {R : CFlag g} {d : IndexMark} {alpha beta : List (WorkSym g)} (k : ℕ) (hrule : AugPush g A B f) (hcomp : (cflagComp g (cflagBase g f) R).Nonempty) : WorkTraceAccepts g (CompositeCert.livePushCompress A B f R d) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.live A), inactive (WorkSym.index R d)] ++ List.map inactive beta ++ List.replicate k none) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.live B), inactive (WorkSym.index (cflagComp g (cflagBase g f) R) d)] ++ List.map inactive beta ++ List.replicate k none)

def IndexedGrammar.Aho.minus1ShiftRows {T : Type} (g : IndexedGrammar T) (prev : Option (WorkSlot g)) : List (Option (WorkSlot g)) → List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)

Equations

• IndexedGrammar.Aho.minus1ShiftRows g prev [] = [(prev, none, IndexedGrammar.Aho.WorkPhase.suffixMinus1)]
• IndexedGrammar.Aho.minus1ShiftRows g prev (x_1 :: xs) = (prev, x_1, IndexedGrammar.Aho.WorkPhase.suffixMinus1) :: IndexedGrammar.Aho.minus1ShiftRows g x_1 xs

@[simp]

theorem IndexedGrammar.Aho.minus1ShiftRows_old {T : Type} (g : IndexedGrammar T) (prev : Option (WorkSlot g)) (xs : List (Option (WorkSlot g))) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) (minus1ShiftRows g prev xs) = prev :: xs

@[simp]

theorem IndexedGrammar.Aho.minus1ShiftRows_new {T : Type} (g : IndexedGrammar T) (prev : Option (WorkSlot g)) (xs : List (Option (WorkSlot g))) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) (minus1ShiftRows g prev xs) = xs ++ [none]

def IndexedGrammar.Aho.minus1FromRows {T : Type} (g : IndexedGrammar T) (nextFocus : WorkSym g) : List (Option (WorkSlot g)) → List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)

Equations

• One or more equations did not get rendered due to their size.
• IndexedGrammar.Aho.minus1FromRows g nextFocus [] = [(IndexedGrammar.Aho.inactive nextFocus, none, IndexedGrammar.Aho.WorkPhase.suffixMinus1)]

@[simp]

theorem IndexedGrammar.Aho.minus1FromRows_old {T : Type} (g : IndexedGrammar T) (nextFocus : WorkSym g) (xs : List (Option (WorkSlot g))) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) (minus1FromRows g nextFocus xs) = inactive nextFocus :: xs

@[simp]

theorem IndexedGrammar.Aho.minus1FromRows_new {T : Type} (g : IndexedGrammar T) (nextFocus : WorkSym g) (xs : List (Option (WorkSlot g))) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) (minus1FromRows g nextFocus xs) = xs ++ [none]

theorem IndexedGrammar.Aho.accepts_replace_delete_next {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (alpha beta : List (WorkSym g)) (oldFocus newFocus deletedNext : WorkSym g) (k : ℕ) (henabled : CertEnabled g cert) (hproductive : cert.productive = false) (hfocus : ∀ (h : WorkHistory g), WorkEdge g cert WorkPhase.stage1 WorkPhase.minus1First h (active oldFocus) (active newFocus)) (hfirst : ∀ (h : WorkHistory g), WorkEdge g cert WorkPhase.minus1First WorkPhase.suffixMinus1 h (inactive deletedNext) (firstPad (List.map inactive beta ++ List.replicate k none))) (hloop : ∀ (h : WorkHistory g) (old new : Option (WorkSlot g)), minus1Suffix h old new → WorkEdge g cert WorkPhase.suffixMinus1 WorkPhase.suffixMinus1 h old new) : WorkTraceAccepts g cert (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active oldFocus, inactive deletedNext] ++ List.map inactive beta ++ List.replicate k none) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active newFocus] ++ List.map inactive beta ++ List.replicate (k + 1) none)

Replace the active task and delete its immediately adjacent index in the same certified scan. This is the row-level implementation of unframed pop-and-erase.

theorem IndexedGrammar.Aho.accepts_popPlainErase {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {R : CFlag g} {d : IndexMark} {A B : g.nt} {alpha gamma : List (WorkSym g)} (k : ℕ) (hrule : R A B = true) : WorkTraceAccepts g (CompositeCert.popPlain R d A B) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.live A), inactive (WorkSym.index R d)] ++ List.map inactive gamma ++ List.replicate k none) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.plain B)] ++ List.map inactive gamma ++ List.replicate (k + 1) none)

Certified adjacent pop-and-erase trace for a plain residual task.

theorem IndexedGrammar.Aho.accepts_popLiveErase {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {R : CFlag g} {d : IndexMark} {A B : g.nt} {alpha gamma : List (WorkSym g)} (k : ℕ) (hrule : R A B = true) (hlater : d.later = true) : WorkTraceAccepts g (CompositeCert.popLive R d A B) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.live A), inactive (WorkSym.index R d)] ++ List.map inactive gamma ++ List.replicate k none) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.live B)] ++ List.map inactive gamma ++ List.replicate (k + 1) none)

Certified adjacent pop-and-erase trace for a live residual task.

theorem IndexedGrammar.Aho.accepts_delete_one {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (cert : CompositeCert g) (prefixRows : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)) (h : WorkHistory g) (hprefix : WorkTrace g cert (initialWorkScan g) prefixRows { phase := WorkPhase.stage1, history := h, oldEnded := false, newEnded := false }) (deleted nextFocus : WorkSym g) (beta : List (WorkSym g)) (k : ℕ) (hfocus : ∀ (h : WorkHistory g), WorkEdge g cert WorkPhase.stage1 WorkPhase.minus1First h (active deleted) (active nextFocus)) (hfirst : ∀ (h : WorkHistory g), h.new1 = some (active nextFocus) → WorkEdge g cert WorkPhase.minus1First WorkPhase.suffixMinus1 h (inactive nextFocus) (firstPad (List.map inactive beta ++ List.replicate k none))) (hloop : ∀ (h : WorkHistory g) (old new : Option (WorkSlot g)), minus1Suffix h old new → WorkEdge g cert WorkPhase.suffixMinus1 WorkPhase.suffixMinus1 h old new) : WorkTraceAccepts g cert (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) prefixRows ++ [active deleted, inactive nextFocus] ++ List.map inactive beta ++ List.replicate k none) (List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) prefixRows ++ [active nextFocus] ++ List.map inactive beta ++ List.replicate (k + 1) none)

theorem IndexedGrammar.Aho.accepts_matchTerminal {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {a : T} {alpha beta : List (WorkSym g)} {Z : WorkSym g} (k : ℕ) : WorkTraceAccepts g (CompositeCert.matchTerminal a) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.terminal a), inactive Z] ++ List.map inactive beta ++ List.replicate k none) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active Z] ++ List.map inactive beta ++ List.replicate (k + 1) none)

theorem IndexedGrammar.Aho.accepts_eraseIndex {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {R : CFlag g} {d : IndexMark} {alpha beta : List (WorkSym g)} {Z : WorkSym g} (k : ℕ) (herase : d.erasable = true) : WorkTraceAccepts g (CompositeCert.eraseIndex R d) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active (WorkSym.index R d), inactive Z] ++ List.map inactive beta ++ List.replicate k none) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active Z] ++ List.map inactive beta ++ List.replicate (k + 1) none)

def IndexedGrammar.Aho.minus2ShiftRows {T : Type} (g : IndexedGrammar T) (prev2 prev1 : Option (WorkSlot g)) : List (Option (WorkSlot g)) → List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)

Equations

• IndexedGrammar.Aho.minus2ShiftRows g prev2 prev1 [] = [(prev2, none, IndexedGrammar.Aho.WorkPhase.suffixMinus2), (prev1, none, IndexedGrammar.Aho.WorkPhase.suffixMinus2)]
• IndexedGrammar.Aho.minus2ShiftRows g prev2 prev1 (x_1 :: xs) = (prev2, x_1, IndexedGrammar.Aho.WorkPhase.suffixMinus2) :: IndexedGrammar.Aho.minus2ShiftRows g prev1 x_1 xs

@[simp]

theorem IndexedGrammar.Aho.minus2ShiftRows_old {T : Type} (g : IndexedGrammar T) (prev2 prev1 : Option (WorkSlot g)) (xs : List (Option (WorkSlot g))) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) (minus2ShiftRows g prev2 prev1 xs) = prev2 :: prev1 :: xs

@[simp]

theorem IndexedGrammar.Aho.minus2ShiftRows_new {T : Type} (g : IndexedGrammar T) (prev2 prev1 : Option (WorkSlot g)) (xs : List (Option (WorkSlot g))) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) (minus2ShiftRows g prev2 prev1 xs) = xs ++ [none, none]

def IndexedGrammar.Aho.minus2FromRows {T : Type} (g : IndexedGrammar T) : List (Option (WorkSlot g)) → List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)

Equations

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

@[simp]

theorem IndexedGrammar.Aho.minus2FromRows_old {T : Type} (g : IndexedGrammar T) (xs : List (Option (WorkSlot g))) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) (minus2FromRows g xs) = inactive WorkSym.dollar :: active WorkSym.close :: xs

@[simp]

theorem IndexedGrammar.Aho.minus2FromRows_new {T : Type} (g : IndexedGrammar T) (xs : List (Option (WorkSlot g))) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) (minus2FromRows g xs) = xs ++ [none, none]

def IndexedGrammar.Aho.returnBetaRows {T : Type} (g : IndexedGrammar T) (xs : List (WorkSym g)) : List (Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase)

Equations

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

@[simp]

theorem IndexedGrammar.Aho.returnBetaRows_old {T : Type} (g : IndexedGrammar T) (xs : List (WorkSym g)) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.1) (returnBetaRows g xs) = List.map inactive xs

@[simp]

theorem IndexedGrammar.Aho.returnBetaRows_new {T : Type} (g : IndexedGrammar T) (xs : List (WorkSym g)) : List.map (fun (r : Option (WorkSlot g) × Option (WorkSlot g) × WorkPhase) => r.2.1) (returnBetaRows g xs) = List.map inactive xs

theorem IndexedGrammar.Aho.accepts_returnFrame {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {alpha beta gamma : List (WorkSym g)} {Z : WorkSym g} (k : ℕ) (hZ : Z ≠ WorkSym.dollar) (hfree : DollarFree beta) : WorkTraceAccepts g CompositeCert.returnFrame (List.map inactive (alpha ++ [WorkSym.dollar, Z] ++ beta ++ [WorkSym.dollar]) ++ [active WorkSym.close] ++ List.map inactive gamma ++ List.replicate k none) (List.map inactive (alpha ++ [WorkSym.dollar]) ++ [active Z] ++ List.map inactive (beta ++ gamma) ++ List.replicate (k + 2) none)

theorem IndexedGrammar.Aho.accepts_padded_plainBinary_of_step {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) {A B C : g.nt} {c c' : Config g} (n : ℕ) (hstep : CertStep g input (CompositeCert.plainBinary A B C) c c') (hold : c.work.word.length ≤ n * workWidth) (hnew : c'.work.word.length ≤ n * workWidth) : WorkTraceAccepts g (CompositeCert.plainBinary A B C) (paddedWork n c.work.slots) (paddedWork n c'.work.slots)

theorem IndexedGrammar.Aho.accepts_padded_plainTerminal_of_step {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) {A : g.nt} {a : T} {c c' : Config g} (n : ℕ) (hstep : CertStep g input (CompositeCert.plainTerminal A a) c c') (hold : c.work.word.length ≤ n * workWidth) (hnew : c'.work.word.length ≤ n * workWidth) : WorkTraceAccepts g (CompositeCert.plainTerminal A a) (paddedWork n c.work.slots) (paddedWork n c'.work.slots)

theorem IndexedGrammar.Aho.accepts_padded_plainPushSkip_of_step {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) {A B : g.nt} {f : g.flag} {c c' : Config g} (n : ℕ) (hstep : CertStep g input (CompositeCert.plainPushSkip A B f) c c') (hold : c.work.word.length ≤ n * workWidth) (hnew : c'.work.word.length ≤ n * workWidth) : WorkTraceAccepts g (CompositeCert.plainPushSkip A B f) (paddedWork n c.work.slots) (paddedWork n c'.work.slots)

theorem IndexedGrammar.Aho.accepts_padded_livePushCompress_of_step {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) {A B : g.nt} {f : g.flag} {R : CFlag g} {d : IndexMark} {c c' : Config g} (n : ℕ) (hstep : CertStep g input (CompositeCert.livePushCompress A B f R d) c c') (hold : c.work.word.length ≤ n * workWidth) (hnew : c'.work.word.length ≤ n * workWidth) : WorkTraceAccepts g (CompositeCert.livePushCompress A B f R d) (paddedWork n c.work.slots) (paddedWork n c'.work.slots)

theorem IndexedGrammar.Aho.accepts_padded_plainPushUse_of_step {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) {A B : g.nt} {f : g.flag} {c c' : Config g} (n : ℕ) (hstep : CertStep g input (CompositeCert.plainPushUse A B f) c c') (hold : c.work.word.length ≤ n * workWidth) (hnew : c'.work.word.length ≤ n * workWidth) : WorkTraceAccepts g (CompositeCert.plainPushUse A B f) (paddedWork n c.work.slots) (paddedWork n c'.work.slots)

theorem IndexedGrammar.Aho.accepts_padded_liveBinaryBoth_of_step {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) {A B C : g.nt} {c c' : Config g} (n : ℕ) (hstep : CertStep g input (CompositeCert.liveBinaryBoth A B C) c c') (hold : c.work.word.length ≤ n * workWidth) (hnew : c'.work.word.length ≤ n * workWidth) : WorkTraceAccepts g (CompositeCert.liveBinaryBoth A B C) (paddedWork n c.work.slots) (paddedWork n c'.work.slots)

theorem IndexedGrammar.Aho.accepts_padded_liveBinaryLeft_of_step {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) {A B C : g.nt} {c c' : Config g} (n : ℕ) (hstep : CertStep g input (CompositeCert.liveBinaryLeft A B C) c c') (hold : c.work.word.length ≤ n * workWidth) (hnew : c'.work.word.length ≤ n * workWidth) : WorkTraceAccepts g (CompositeCert.liveBinaryLeft A B C) (paddedWork n c.work.slots) (paddedWork n c'.work.slots)

theorem IndexedGrammar.Aho.accepts_padded_liveBinaryRight_of_step {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) {A B C : g.nt} {c c' : Config g} (n : ℕ) (hstep : CertStep g input (CompositeCert.liveBinaryRight A B C) c c') (hold : c.work.word.length ≤ n * workWidth) (hnew : c'.work.word.length ≤ n * workWidth) : WorkTraceAccepts g (CompositeCert.liveBinaryRight A B C) (paddedWork n c.work.slots) (paddedWork n c'.work.slots)

theorem IndexedGrammar.Aho.accepts_padded_livePushFresh_of_step {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) {A B : g.nt} {f : g.flag} {c c' : Config g} (n : ℕ) (hstep : CertStep g input (CompositeCert.livePushFresh A B f) c c') (hold : c.work.word.length ≤ n * workWidth) (hnew : c'.work.word.length ≤ n * workWidth) : WorkTraceAccepts g (CompositeCert.livePushFresh A B f) (paddedWork n c.work.slots) (paddedWork n c'.work.slots)

theorem IndexedGrammar.Aho.accepts_padded_popPlain_of_step {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) {R : CFlag g} {d : IndexMark} {A B : g.nt} {c c' : Config g} (n : ℕ) (hstep : CertStep g input (CompositeCert.popPlain R d A B) c c') (hold : c.work.word.length ≤ n * workWidth) (hnew : c'.work.word.length ≤ n * workWidth) : WorkTraceAccepts g (CompositeCert.popPlain R d A B) (paddedWork n c.work.slots) (paddedWork n c'.work.slots)

theorem IndexedGrammar.Aho.accepts_padded_popLive_of_step {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) {R : CFlag g} {d : IndexMark} {A B : g.nt} {c c' : Config g} (n : ℕ) (hstep : CertStep g input (CompositeCert.popLive R d A B) c c') (hold : c.work.word.length ≤ n * workWidth) (hnew : c'.work.word.length ≤ n * workWidth) : WorkTraceAccepts g (CompositeCert.popLive R d A B) (paddedWork n c.work.slots) (paddedWork n c'.work.slots)

theorem IndexedGrammar.Aho.accepts_padded_matchTerminal_of_step {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) {a : T} {c c' : Config g} (n : ℕ) (hstep : CertStep g input (CompositeCert.matchTerminal a) c c') (hold : c.work.word.length ≤ n * workWidth) (hnew : c'.work.word.length ≤ n * workWidth) : WorkTraceAccepts g (CompositeCert.matchTerminal a) (paddedWork n c.work.slots) (paddedWork n c'.work.slots)

theorem IndexedGrammar.Aho.accepts_padded_eraseIndex_of_step {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) {R : CFlag g} {d : IndexMark} {c c' : Config g} (n : ℕ) (hstep : CertStep g input (CompositeCert.eraseIndex R d) c c') (hold : c.work.word.length ≤ n * workWidth) (hnew : c'.work.word.length ≤ n * workWidth) : WorkTraceAccepts g (CompositeCert.eraseIndex R d) (paddedWork n c.work.slots) (paddedWork n c'.work.slots)

theorem IndexedGrammar.Aho.accepts_padded_returnFrame_of_step {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) {c c' : Config g} (n : ℕ) (hstep : CertStep g input CompositeCert.returnFrame c c') (hold : c.work.word.length ≤ n * workWidth) (hnew : c'.work.word.length ≤ n * workWidth) : WorkTraceAccepts g CompositeCert.returnFrame (paddedWork n c.work.slots) (paddedWork n c'.work.slots)

theorem IndexedGrammar.Aho.workTraceAccepts_of_certStep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) (cert : CompositeCert g) {c c' : Config g} (n : ℕ) (hstep : CertStep g input cert c c') (hold : c.work.word.length ≤ n * workWidth) (hnew : c'.work.word.length ≤ n * workWidth) : WorkTraceAccepts g cert (paddedWork n c.work.slots) (paddedWork n c'.work.slots)

Every bounded machine certificate has an accepting synchronized logical-slot trace.