Lookup in a framed word followed by a suffix

These pure list laws are shared by the unary take/drop and zip-transducer machine proofs. They depend only on the framing format, independently of either machine construction.

Main results

• Turing.MultiTapeTM.getElem?_frame_append: the marker and data bit at each framed position.
• Turing.MultiTapeTM.getElem?_frame_append_length: the terminator after the framed pairs.
• Turing.MultiTapeTM.getElem?_frame_append_boundary: every bit of the suffix beyond the frame.
• Turing.MultiTapeTM.length_frame_append: the length of a frame followed by a suffix.

theorem Turing.MultiTapeTM.getElem?_frame_append (u v : List Bool) {i : ℕ} (hi : i < u.length) : (frame u ++ v)[2 * i]? = some true ∧ (frame u ++ v)[2 * i + 1]? = some u[i]

The marker and data bit of u[i] in a frame followed by any suffix.

theorem Turing.MultiTapeTM.length_flatMap_pair (u : List Bool) : (List.flatMap (fun (b : Bool) => [true, b]) u).length = 2 * u.length

The pairs of a frame have twice the length of the word.

theorem Turing.MultiTapeTM.getElem?_frame_append_length (u v : List Bool) : (frame u ++ v)[2 * u.length]? = some false

After the pairs of a frame comes its terminator false.

theorem Turing.MultiTapeTM.getElem?_frame_append_boundary (u v : List Bool) (j : ℕ) : (frame u ++ v)[2 * u.length + 1 + j]? = v[j]?

Lookup beyond the frame reads the suffix, including out of bounds.

theorem Turing.MultiTapeTM.length_frame_append (u v : List Bool) : (frame u ++ v).length = 2 * u.length + 1 + v.length

A frame followed by a suffix has length 2 |u| + 1 + |v|.