The bits of a framed word

frame w doubles every bit b of w into true, b and ends with false (Turing.MultiTapeTM.frame). Its bits are therefore constants or bits of w (Turing.MultiTapeTM.getElem_frame), which is what makes framed inputs easy to feed to circuits.

A frame followed by a word, as written on a work tape, splits at each framed bit into the pairs before it, the pair true, c of the bit c, and the frame of the rest (Turing.MultiTapeTM.frame_append_cons), so a machine can locate the tag and the bit of each pair and overwrite the bit in place (Turing.MultiTapeTM.set_frame_append_cons).

Main results

• Turing.MultiTapeTM.getElem_frame: the bit at each position of frame w.
• Turing.MultiTapeTM.getElem?_frame_two_mul, Turing.MultiTapeTM.getElem?_frame_two_mul_add_one, Turing.MultiTapeTM.getElem?_frame_two_mul_length: the marker, data, and terminator bits of frame w by position.
• Turing.MultiTapeTM.forall_getElem?_frame_iff: a predicate agrees with frame w placed at offset base iff it agrees with the markers, the bits of w, and the terminator.
• Turing.MultiTapeTM.forall_getElem?_append_iff: a predicate agrees with the bits of u ++ w iff it agrees with u and with w shifted by u.length.
• Turing.MultiTapeTM.getD_frame_two_mul, Turing.MultiTapeTM.getD_frame_two_mul_add_one: indexed access to markers and input bits with default false.
• Turing.MultiTapeTM.length_flatMap_frame: the length of a list of framed words.
• Turing.MultiTapeTM.length_unframe_le: the word framed at the start of a word is no longer than the word.
• Turing.MultiTapeTM.frame_append_cons: a frame split at a framed bit.
• Turing.MultiTapeTM.getElem?_frame_append_length, Turing.MultiTapeTM.getElem?_frame_append_cons: the terminator and the tags of a frame followed by a word.
• Turing.MultiTapeTM.lt_length_frame_append_cons, Turing.MultiTapeTM.two_mul_length_le_length_frame_append: positions within a frame followed by a word.
• Turing.MultiTapeTM.set_frame_append_cons: overwriting a framed bit in place.

theorem Turing.MultiTapeTM.getElem_frame (w : List Bool) (j : ℕ) (hj : j < (frame w).length) : (frame w)[j] = if h : j < 2 * w.length then if j % 2 = 0 then true else w[j / 2] else false

The bit at position j of frame w: true at even positions below 2 |w|, the bit w[j / 2] at odd ones, and the final false.

Indexed bit access

theorem Turing.MultiTapeTM.getElem?_frame_two_mul_length (w : List Bool) : (frame w)[2 * w.length]? = some false

The terminator of frame w sits at position 2 * w.length.

theorem Turing.MultiTapeTM.getElem?_frame_two_mul {w : List Bool} {j : ℕ} (hj : j < w.length) : (frame w)[2 * j]? = some true

Each bit of w is preceded in frame w by a true marker at an even position.

theorem Turing.MultiTapeTM.getElem?_frame_two_mul_add_one {w : List Bool} {j : ℕ} (hj : j < w.length) : (frame w)[2 * j + 1]? = w[j]?

The bit w[j] sits at the odd position 2 * j + 1 of frame w.

theorem Turing.MultiTapeTM.forall_getElem?_frame_iff (w : List Bool) (base : ℕ) (P : ℕ → Prop) : (∀ (p : ℕ), base ≤ p → p < base + (frame w).length → (P p ↔ (frame w)[p - base]? = some true)) ↔ ¬P (base + 2 * w.length) ∧ ∀ j < w.length, P (base + 2 * j) ∧ (P (base + 2 * j + 1) ↔ w[j]? = some true)

A predicate P : ℕ → Prop agrees with frame w shifted by base on [base, base + (frame w).length) iff it is false at base + 2 * w.length and, for each j < w.length, is true at base + 2 * j and agrees with w[j] at base + 2 * j + 1.

theorem Turing.MultiTapeTM.forall_getElem?_append_iff (u w : List Bool) (P : ℕ → Prop) : (∀ p < (u ++ w).length, P p ↔ (u ++ w)[p]? = some true) ↔ (∀ p < u.length, P p ↔ u[p]? = some true) ∧ ∀ (p : ℕ), u.length ≤ p → p < u.length + w.length → (P p ↔ w[p - u.length]? = some true)

A predicate P : ℕ → Prop agrees with the bits of u ++ w iff it agrees with u below u.length and with w shifted by u.length on [u.length, u.length + w.length).

theorem Turing.MultiTapeTM.length_flatMap_frame (l : List (List Bool)) : (List.flatMap frame l).length = (List.map (fun (t : List Bool) => 2 * t.length + 1) l).sum

A list of framed words spends 2 * |t| + 1 bits on each word t.

theorem Turing.MultiTapeTM.getD_frame_two_mul (w : List Bool) (i : ℕ) : (frame w).getD (2 * i) false = decide (i < w.length)

With default false, the even marker bit tests whether the input index is in bounds.

theorem Turing.MultiTapeTM.getD_frame_two_mul_add_one (w : List Bool) (i : ℕ) : (frame w).getD (2 * i + 1) false = w.getD i false

With default false, the odd frame positions contain exactly the input bits.

theorem Turing.MultiTapeTM.length_unframe_le (w : List Bool) : (unframe w).length ≤ w.length

The word framed at the start of a word is no longer than the word.

Frames followed by a word

theorem Turing.MultiTapeTM.frame_append_cons (w v : List Bool) (c : Bool) : frame (w ++ c :: v) = List.flatMap (fun (b : Bool) => [true, b]) w ++ true :: c :: frame v

A frame split at a symbol.

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

After the pairs of a frame comes its terminator false.

theorem Turing.MultiTapeTM.getElem?_frame_append_cons (w v x : List Bool) (c : Bool) : (frame (w ++ c :: v) ++ x)[2 * w.length]? = some true

Each pair of a frame starts with the tag true.

theorem Turing.MultiTapeTM.lt_length_frame_append_cons (w v x : List Bool) (c : Bool) : 2 * w.length + 1 < (frame (w ++ c :: v) ++ x).length

The second cell of a pair of a frame lies within the word.

theorem Turing.MultiTapeTM.set_frame_append_cons (w v x : List Bool) (c b : Bool) : (frame (w ++ c :: v) ++ x).set (2 * w.length + 1) b = frame (w ++ b :: v) ++ x

Setting the second cell of a pair of a frame replaces the framed symbol.

theorem Turing.MultiTapeTM.two_mul_length_le_length_frame_append (w x : List Bool) : 2 * w.length ≤ (frame w ++ x).length

The pairs of a frame fit in the word.