Description-tape layout

Positional facts about a tape holding a description string l = qsF □ qhF □ R (the takeField split): where the two header fields end, and what the cells of the entry region are. Everything is derived from a single normalization: the getElem?-with-blank-default view of l agrees with its canonical three-part layout even when trailing separators are missing (takeField treats end-of-list like □ — by design, matching the tape's blank fill).

These feed the seek phase (two scanRight_loop instances land the desc head at the entry region) and the match loop (entry-region cells).

theorem Complexity.TM.UTMBody.getD_append_blank (l : List Γw) (i : ℕ) : (l ++ [Γw.blank])[i]?.getD Γw.blank = l[i]?.getD Γw.blank

getElem?-with-blank-default is insensitive to a trailing blank.

def Complexity.TM.UTMBody.canonical (l : List Γw) : List Γw

The canonical three-part layout of a description string.

Equations

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

theorem Complexity.TM.UTMBody.getD_canonical (l : List Γw) (i : ℕ) : l[i]?.getD Γw.blank = (canonical l)[i]?.getD Γw.blank

Blank-default cell access agrees with the canonical layout, whether or not the trailing separators are present in l.

theorem Complexity.TM.UTMBody.holdsExact_cells_getD {t : Tape} {l : List Γw} (h : t.HoldsExact l) (i : ℕ) : t.cells (i + 1) = (l[i]?.getD Γw.blank).toΓ

Cell contents of a HoldsExact tape, in blank-default form.

theorem Complexity.TM.UTMBody.descLayout_field1 {t : Tape} {l : List Γw} (h : t.HoldsExact l) (j : ℕ) : j < (takeField l).1.length → t.cells (1 + j) ≠ Γ.blank

Field-1 cells are non-blank.

theorem Complexity.TM.UTMBody.descLayout_sep1 {t : Tape} {l : List Γw} (h : t.HoldsExact l) : t.cells (1 + (takeField l).1.length) = Γ.blank

The separator after field 1.

theorem Complexity.TM.UTMBody.descLayout_field2 {t : Tape} {l : List Γw} (h : t.HoldsExact l) (j : ℕ) : j < (takeField (takeField l).2).1.length → t.cells ((takeField l).1.length + 2 + j) ≠ Γ.blank

Field-2 cells are non-blank.

theorem Complexity.TM.UTMBody.descLayout_sep2 {t : Tape} {l : List Γw} (h : t.HoldsExact l) : t.cells ((takeField l).1.length + 2 + (takeField (takeField l).2).1.length) = Γ.blank

The separator after field 2.

theorem Complexity.TM.UTMBody.descLayout_entries {t : Tape} {l : List Γw} (h : t.HoldsExact l) (j : ℕ) : t.cells ((takeField l).1.length + (takeField (takeField l).2).1.length + 3 + j) = ((takeField (takeField l).2).2[j]?.getD Γw.blank).toΓ

Entry-region cells: cell |F1| + |F2| + 3 + j holds the j-th symbol of the entry region R := (takeField (takeField l).2).2 (blank beyond).

theorem Complexity.TM.UTMBody.descLayout_field1_val {t : Tape} {l : List Γw} (h : t.HoldsExact l) (j : ℕ) (hj : j < (takeField l).1.length) : t.cells (1 + j) = (takeField l).1[j].toΓ

Field-1 cell values.

theorem Complexity.TM.UTMBody.descLayout_field2_val {t : Tape} {l : List Γw} (h : t.HoldsExact l) (j : ℕ) (hj : j < (takeField (takeField l).2).1.length) : t.cells ((takeField l).1.length + 2 + j) = (takeField (takeField l).2).1[j].toΓ

Field-2 cell values.

theorem Complexity.TM.UTMBody.descLayout_field2_getD {t : Tape} {l : List Γw} (h : t.HoldsExact l) (j : ℕ) (hj : j ≤ (takeField (takeField l).2).1.length) : t.cells ((takeField l).1.length + 2 + j) = ((takeField (takeField l).2).1[j]?.getD Γw.blank).toΓ

Field-2 cell values, blank-default form (covers positions beyond the field: the separator/beyond reads □).

theorem Complexity.TM.UTMBody.exists_first_mismatch {A B : List Γw} (hA : ∀ s ∈ A, s ≠ Γw.blank) (hB : ∀ s ∈ B, s ≠ Γw.blank) (hne : A ≠ B) : ∃ n ≤ A.length, n ≤ B.length ∧ (∀ j < n, A[j]?.getD Γw.blank = B[j]?.getD Γw.blank ∧ A[j]?.getD Γw.blank ≠ Γw.blank) ∧ A[n]?.getD Γw.blank ≠ B[n]?.getD Γw.blank

First mismatch extraction: two different blank-free lists, viewed as blank-padded infinite sequences, have a least disagreement index; below it they agree on non-blank symbols, and at it the hc1-style mismatch conditions hold.