Input framing for the Tseitin streaming controller

The streaming controller never rewinds while reading a valid token stream. framedTokenInput pre rest fixes the original cells for pre ++ rest and places the head immediately after the encoded prefix. These lemmas identify the next two cells with the next token and normalize the frame after those two cells have been consumed.

def Complexity.SAT.ThreeSAT.Machine.framedTokenInput (pre rest : List EncToken) : Tape

Original token-stream cells with the head immediately after pre.

Equations

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

theorem Complexity.SAT.ThreeSAT.Machine.framedTokenInput_parked (pre rest : List EncToken) : TM.Parked (framedTokenInput pre rest)

Every framed token input is parked.

theorem Complexity.SAT.ThreeSAT.Machine.framedTokenInput_tokenAt (pre rest : List EncToken) (tok : EncToken) : InputTokenAt (framedTokenInput pre (tok :: rest)) tok

The next two cells of a nonempty remainder are exactly its first token.

theorem Complexity.SAT.ThreeSAT.Machine.controllerScheduledCfg_framedTokenInput (mode : StreamMode) (pre rest : List EncToken) (tok : EncToken) {Q : Type} (c : Cfg workTapeCount Q) (hinput : c.input = framedTokenInput pre (tok :: rest)) : (controllerScheduledCfg mode tok c).input = framedTokenInput (pre ++ [tok]) rest

Consuming the next token advances the framing prefix by that token.

theorem Complexity.SAT.ThreeSAT.Machine.framedTokenInput_nil_read (pre : List EncToken) : (framedTokenInput pre []).read = Γ.blank

With no tokens remaining, the framed input head reads the first trailing blank.

theorem Complexity.SAT.ThreeSAT.Machine.framedTokenInput_nil_prefix (toks : List EncToken) : framedTokenInput [] toks = { head := 1, cells := (Tape.init (List.map Γ.ofBool (encodeTokens toks))).cells }

The empty-prefix frame is the input tape handed to the controller after rewind.