Certificate soundness for Aho's machine

Every certified composite step has its stated grammar or input-consumption effect.

Every finite certificate is denotationally sound

def IndexedGrammar.Aho.ControlDenotation.StepEffect {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) (c c' : Config g) (form form' : List g.ISym) : Prop

Equations

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

theorem IndexedGrammar.Aho.ControlDenotation.certStep_preserves_represents {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (input : List T) (cert : CompositeCert g) {c c' : Config g} {form : List g.ISym} (hstep : CertStep g input cert c c') (hrep : Config.Represents c form) : ∃ (form' : List g.ISym), Config.Represents c' form' ∧ StepEffect g input c c' form form'