The simp set of cp_step

The simp set used by cp_step in CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram.Step, declared in a file of its own because an attribute cannot be used in the file declaring it. A simp set is indexed once, when its lemmas are tagged, so a call that uses it does not elaborate and index its lemmas again; cp_step runs once per instruction of a straight-line proof.

Main definitions

• cp_simps: evaluation of counter-program expressions and of the label a read jumps to.

def Parser.Attr.cp_simps : Lean.ParserDescr

The simp set cp_simps evaluates counter-program expressions (Turing.CounterProgram.Expr.eval) and the label a read jumps to (Turing.CounterProgram.readLabel), for cp_step.

def Parser.Attr.cp_simps_proc : Lean.ParserDescr

Simplification procedure