Documentation

Complexity.Computability.Machines.Turing.MultiTape.Internal.FrameMachines

Shared machines for reading framed words #

These original finite-state machines and run laws preserve all-word behavior, including empty and incomplete frames. Their source is moved unchanged from Encodings.Basic.

source
inductive Turing.MultiTapeTM.Internal.FrameMachines.FrameState :
Type

The states of a transducer reading a framed word: expecting a marker, expecting a symbol, or past the frame.

Instances For
    source
    instance Turing.MultiTapeTM.Internal.FrameMachines.instFiniteFrameState :
    Finite FrameState
    source
    def Turing.MultiTapeTM.Internal.FrameMachines.readFrameT (keep : Bool) :
    Transducer Bool FrameState

    Emits the word framed at the start of its input (keep = true), or what follows the frame (keep = false).

    Instances For
      source
      @[simp]
      theorem Turing.MultiTapeTM.Internal.FrameMachines.readFrameT_q₀ (keep : Bool) :
      (readFrameT keep).q₀ = FrameState.marker
      source
      @[simp]
      theorem Turing.MultiTapeTM.Internal.FrameMachines.readFrameT_final (keep : Bool) (x✝ : FrameState) :
      (readFrameT keep).final x✝ = []
      source
      @[simp]
      theorem Turing.MultiTapeTM.Internal.FrameMachines.readFrameT_step (keep : Bool) (x✝ : FrameState) (x✝¹ : Bool) :
      (readFrameT keep).step x✝ x✝¹ = match x✝, x✝¹ with | FrameState.marker, true => (FrameState.bit, []) | FrameState.marker, false => (FrameState.done, []) | FrameState.bit, b => (FrameState.marker, if keep = true then [b] else []) | FrameState.done, b => (FrameState.done, if keep = true then [] else [b])
      source
      theorem Turing.MultiTapeTM.Internal.FrameMachines.readFrameT_run_done (keep : Bool) (v : List Bool) :
      (readFrameT keep).run FrameState.done v = if keep = true then [] else v
      source
      theorem Turing.MultiTapeTM.Internal.FrameMachines.readFrameT_run_true (v : List Bool) :
      (readFrameT true).run FrameState.marker v = unframe v
      source
      theorem Turing.MultiTapeTM.Internal.FrameMachines.readFrameT_run_false (v : List Bool) :
      (readFrameT false).run FrameState.marker v = dropFrame v
      source
      def Turing.MultiTapeTM.Encodings.frameT :
      Transducer Bool Unit

      Frames its input.

      Instances For
        source
        @[simp]
        theorem Turing.MultiTapeTM.Encodings.frameT_final (x✝ : Unit) :
        frameT.final x✝ = [false]
        source
        @[simp]
        theorem Turing.MultiTapeTM.Encodings.frameT_step (x✝ : Unit) (b : Bool) :
        frameT.step x✝ b = ((), [true, b])
        source
        @[simp]
        theorem Turing.MultiTapeTM.Encodings.frameT_q₀ :
        frameT.q₀ = ()
        source
        theorem Turing.MultiTapeTM.Encodings.frameT_run (v : List Bool) :
        frameT.run () v = frame v