RAM sparse-entry decoder — proof internals

theorem Complexity.RAM.RegisterStore.Machine.entryDecodeTM_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) (haddressCounter : (work₀ tapes.addressCounter).HasBinaryNat 0) (haddressWidth : (work₀ tapes.addressWidth).HasBinaryNat 0) (hvalueCounter : (work₀ tapes.valueCounter).HasBinaryNat 0) (hvalueWidth : (work₀ tapes.valueWidth).HasBinaryNat 0) (hinput : inp₀.read ≠ Γ.start) (hreads : ∀ (i : Fin n), (work₀ i).read ≠ Γ.start) (houtput : out₀.read ≠ Γ.start) : ∃ (c' : Complexity.Cfg n (entryDecodeTM tapes).Q), (entryDecodeTM tapes).reachesIn (entryDecodeTime entry.1 entry.2) { state := (entryDecodeTM tapes).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (entryDecodeTM 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).HasBinaryNat (bitlen entry.1) ∧ (c'.work tapes.addressWidth).HasBinaryNat (bitlen entry.1) ∧ (c'.work tapes.valueCounter).HasBinaryNat (bitlen entry.2) ∧ (c'.work tapes.valueWidth).HasBinaryNat (bitlen entry.2) ∧ (∀ (i : Fin n), i ≠ tapes.source → i ≠ tapes.address → i ≠ tapes.value → i ≠ tapes.addressCounter → i ≠ tapes.addressWidth → i ≠ tapes.valueCounter → i ≠ tapes.valueWidth → c'.work i = work₀ i) ∧ c'.output = out₀