Reading a configuration graph's input symbol

readSymbolCode is the five-instruction block used by the STCON reduction to obtain the ternary code of one original input bit. It checks the query against the stored input length, reads position 2 * query + 1 of the framed input when in range, and stores zero otherwise. The block changes only its destination register and emits no output.

The query is a zero-based position in the original word. Configuration-head boundary conventions are handled separately by the compact graph's edge test: this block returns the actual optional word symbol, not the symbol after that boundary correction.

Main definitions

• Turing.MultiTapeNTM.ConfigurationGraph.readSymbolCode: the relocatable input-reading block.

Main results

• Turing.MultiTapeNTM.ConfigurationGraph.reachesOut_readSymbolCode: the actual block reads w[query]? from frame w, preserving the bound on every pre-exit register state.

def Turing.MultiTapeNTM.ConfigurationGraph.readSymbolCode (b dst exit : ℕ) (len query : CounterProgram.Expr) : List CounterProgram.Instr

Read one original input symbol from a framed word into dst, then continue at exit. The five instructions start at b; len is the original word length and query its zero-based index. The result is symbolCode: zero for no symbol, one for false, and two for true.

@[simp]

theorem Turing.MultiTapeNTM.ConfigurationGraph.length_readSymbolCode (b dst exit : ℕ) (len query : CounterProgram.Expr) : (readSymbolCode b dst exit len query).length = 5

The reader occupies five consecutive instruction labels.

theorem Turing.MultiTapeNTM.ConfigurationGraph.reachesOut_readSymbolCode {P : CounterProgram} {b dst exit S : ℕ} {len query : CounterProgram.Expr} {regs : List ℕ} {w : List Bool} (hcode : P.CodeAt b (readSymbolCode b dst exit len query)) (hlen : CounterProgram.Expr.eval regs len = w.length) (hS : ∀ r ∈ regs, r ≤ S) : P.ReachesOut (MultiTapeTM.frame w) (P.Active S) (b, regs) (exit, regs.set dst (symbolCode w[CounterProgram.Expr.eval regs query]?)) []

The placed block reads the original word's optional symbol, changes only dst, and emits nothing. All states before the exit have the original registers, so their bound needs no extra assumption. The final destination is at most two by symbolCode_lt.