Documentation

Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame.Basic

Pure framed words #

The original framing definitions and laws are moved unchanged below encoding-machine capabilities so their machine implementations do not create an import cycle.

Framed words #

source
def Turing.MultiTapeTM.frame (w : List Bool) :
List Bool

Each symbol b of w as [true, b], followed by [false].

Instances For
    source
    def Turing.MultiTapeTM.unframe :
    List Bool → List Bool

    The word framed at the start of v, see Turing.MultiTapeTM.frame.

    Instances For
      source
      def Turing.MultiTapeTM.dropFrame :
      List Bool → List Bool

      What follows the frame at the start of v, see Turing.MultiTapeTM.frame.

      Instances For
        source
        @[simp]
        theorem Turing.MultiTapeTM.frame_nil :
        frame [] = [false]
        source
        @[simp]
        theorem Turing.MultiTapeTM.frame_cons (b : Bool) (w : List Bool) :
        frame (b :: w) = true :: b :: frame w
        source
        @[simp]
        theorem Turing.MultiTapeTM.length_frame (w : List Bool) :
        (frame w).length = 2 * w.length + 1
        source
        @[simp]
        theorem Turing.MultiTapeTM.unframe_frame_append (w u : List Bool) :
        unframe (frame w ++ u) = w
        source
        @[simp]
        theorem Turing.MultiTapeTM.unframe_frame (w : List Bool) :
        unframe (frame w) = w
        source
        @[simp]
        theorem Turing.MultiTapeTM.dropFrame_frame_append (w u : List Bool) :
        dropFrame (frame w ++ u) = u
        source
        theorem Turing.MultiTapeTM.frame_append_inj {w w' u u' : List Bool} (h : frame w ++ u = frame w' ++ u') :
        w = w' ∧ u = u'

        A framed word followed by another word determines both.

        source
        theorem Turing.MultiTapeTM.frame_injective :
        Function.Injective frame

        Framing is injective.

        source
        @[simp]
        theorem Turing.MultiTapeTM.frame_ne_nil (w : List Bool) :
        frame w ≠ []