Decoded sparse-address equality — proof internals

theorem Complexity.RAM.RegisterStore.Machine.decodedAddressEqTM_reachesIn_frame_internal {n : ℕ} (addressIdx queryIdx resultIdx : Fin n) (hdistinct : TM.BinaryEqDistinct addressIdx queryIdx resultIdx) (addressBits queryBits : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (haddress : (work₀ addressIdx).HasBinaryPrefix addressBits) (haddressStart : (work₀ addressIdx).cells 0 = Γ.start) (hquery : (work₀ queryIdx).HasBinaryString queryBits) (hqueryStart : (work₀ queryIdx).cells 0 = Γ.start) (hresult : (work₀ resultIdx).HasBinaryPrefix []) (hinput : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ addressIdx → i ≠ queryIdx → i ≠ resultIdx → (work₀ i).read ≠ Γ.start ∧ 1 ≤ (work₀ i).head) (houtput : out₀.read ≠ Γ.start) (houtputHead : 1 ≤ out₀.head) : ∃ (c' : Complexity.Cfg n (decodedAddressEqTM addressIdx queryIdx resultIdx).Q), ∃ t ≤ decodedAddressEqTime addressBits queryBits, (decodedAddressEqTM addressIdx queryIdx resultIdx).reachesIn t { state := (decodedAddressEqTM addressIdx queryIdx resultIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (decodedAddressEqTM addressIdx queryIdx resultIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work resultIdx).HasBinaryPrefix [decide (addressBits = queryBits)] ∧ (c'.work addressIdx).HasBinaryContent addressBits ∧ 1 ≤ (c'.work addressIdx).head ∧ (c'.work addressIdx).cells 0 = Γ.start ∧ (c'.work queryIdx).HasBinaryContent queryBits ∧ 1 ≤ (c'.work queryIdx).head ∧ (c'.work queryIdx).cells 0 = Γ.start ∧ (∀ (i : Fin n), i ≠ addressIdx → i ≠ queryIdx → i ≠ resultIdx → c'.work i = work₀ i) ∧ c'.output = out₀