Linear RAM sparse-entry decoder -- proof internals

The address and value words are decoded by the linear unary-marker decoder. The established counter tapes become markers, while the width tapes remain framed for compatibility with the existing sparse-store work-tape layout.

theorem Complexity.RAM.RegisterStore.Machine.entryDecodeLinearTM_reachesIn_frame_internal {n : ℕ} (tapes : EntryDecodeTapes n) (entry : Entry) (rest : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsource : (work₀ tapes.source).HasBinarySuffix (entry.encode ++ rest)) (haddress : (work₀ tapes.address).HasBinaryPrefix []) (hvalue : (work₀ tapes.value).HasBinaryPrefix []) (haddressStart : (work₀ tapes.address).cells 0 = Γ.start) (hvalueStart : (work₀ tapes.value).cells 0 = Γ.start) (haddressMarker : (work₀ tapes.addressCounter).HasBinaryPrefix []) (haddressMarkerStart : (work₀ tapes.addressCounter).cells 0 = Γ.start) (hvalueMarker : (work₀ tapes.valueCounter).HasBinaryPrefix []) (hvalueMarkerStart : (work₀ tapes.valueCounter).cells 0 = Γ.start) (hinput : inp₀.read ≠ Γ.start) (hreads : ∀ (i : Fin n), (work₀ i).read ≠ Γ.start) (houtput : out₀.read ≠ Γ.start) : ∃ (c' : Complexity.Cfg n (entryDecodeLinearTM tapes).Q), (entryDecodeLinearTM tapes).reachesIn (entryDecodeLinearTime entry.1 entry.2) { state := (entryDecodeLinearTM tapes).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (entryDecodeLinearTM tapes).halted c' ∧ c'.input = inp₀ ∧ (c'.work tapes.source).HasBinarySuffix rest ∧ (c'.work tapes.address).HasBinaryPrefix entry.1.bits ∧ (c'.work tapes.address).cells 0 = Γ.start ∧ (c'.work tapes.value).HasBinaryPrefix entry.2.bits ∧ (c'.work tapes.value).cells 0 = Γ.start ∧ (c'.work tapes.addressCounter).HasBinaryPrefix (List.replicate (bitlen entry.1) true) ∧ (c'.work tapes.valueCounter).HasBinaryPrefix (List.replicate (bitlen entry.2) true) ∧ (∀ (i : Fin n), i ≠ tapes.source → i ≠ tapes.address → i ≠ tapes.value → i ≠ tapes.addressCounter → i ≠ tapes.valueCounter → c'.work i = work₀ i) ∧ c'.output = out₀