Sparse entry emission — proof internals

theorem Complexity.RAM.RegisterStore.Machine.entryEncodeTM_hoareTime_frame_internal {n : ℕ} (tapes : EntryEncodeTapes n) (entry : Entry) (emitted : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (haddress : (work₀ tapes.address).HasBinaryNat entry.1) (hvalue : (work₀ tapes.value).HasBinaryNat entry.2) (hinput : TM.Parked inp₀) (hother : ∀ (i : Fin n), i ≠ tapes.address → i ≠ tapes.value → TM.Parked (work₀ i)) (houtput : out₀.HasBinaryPrefix emitted) : (entryEncodeTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ (work tapes.address).HasBinarySuffix [] ∧ (work tapes.address).cells = (work₀ tapes.address).cells ∧ (work tapes.address).head = entry.1.bits.length + 1 ∧ (work tapes.value).HasBinarySuffix [] ∧ (work tapes.value).cells = (work₀ tapes.value).cells ∧ (work tapes.value).head = entry.2.bits.length + 1 ∧ (∀ (i : Fin n), i ≠ tapes.address → i ≠ tapes.value → work i = work₀ i) ∧ out.HasBinaryPrefix (emitted ++ entry.encode)) (entryEncodeTime entry)

theorem Complexity.RAM.RegisterStore.Machine.rewindEntryEncodeTM_hoareTime_frame_internal {n : ℕ} (tapes : EntryEncodeTapes n) (entry : Entry) (addressHeadBound valueHeadBound : ℕ) (emitted : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (haddress : (work₀ tapes.address).HasBinaryContent entry.1.bits) (haddressStart : (work₀ tapes.address).cells 0 = Γ.start) (haddressHead : 1 ≤ (work₀ tapes.address).head ∧ (work₀ tapes.address).head ≤ addressHeadBound) (hvalue : (work₀ tapes.value).HasBinaryContent entry.2.bits) (hvalueStart : (work₀ tapes.value).cells 0 = Γ.start) (hvalueHead : 1 ≤ (work₀ tapes.value).head ∧ (work₀ tapes.value).head ≤ valueHeadBound) (hinput : TM.Parked inp₀) (hother : ∀ (i : Fin n), i ≠ tapes.address → i ≠ tapes.value → TM.Parked (work₀ i)) (houtput : out₀.HasBinaryPrefix emitted) : (rewindEntryEncodeTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ (work tapes.address).HasBinarySuffix [] ∧ (work tapes.address).cells = (work₀ tapes.address).cells ∧ (work tapes.address).head = entry.1.bits.length + 1 ∧ (work tapes.value).HasBinarySuffix [] ∧ (work tapes.value).cells = (work₀ tapes.value).cells ∧ (work tapes.value).head = entry.2.bits.length + 1 ∧ (∀ (i : Fin n), i ≠ tapes.address → i ≠ tapes.value → work i = work₀ i) ∧ out.HasBinaryPrefix (emitted ++ entry.encode)) (rewindEntryEncodeTime entry addressHeadBound valueHeadBound)

theorem Complexity.RAM.RegisterStore.Machine.rewindEntryEncodeRestoreTM_hoareTime_frame_internal {n : ℕ} (tapes : EntryEncodeTapes n) (entry : Entry) (emitted : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (haddress : (work₀ tapes.address).HasBinaryNat entry.1) (hvalue : (work₀ tapes.value).HasBinaryNat entry.2) (hinput : TM.Parked inp₀) (hother : ∀ (i : Fin n), i ≠ tapes.address → i ≠ tapes.value → TM.Parked (work₀ i)) (houtput : out₀.HasBinaryPrefix emitted) : (rewindEntryEncodeRestoreTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out.HasBinaryPrefix (emitted ++ entry.encode)) (rewindEntryEncodeRestoreTime entry)