Self-delimiting word emission — proof internals

theorem Complexity.RAM.RegisterStore.Machine.workEmitTM_reachesIn_frame_internal {n : ℕ} (idx : Fin n) (mode : WorkEmitMode) (bits emitted : List Bool) (c : Complexity.Cfg n (workEmitTM idx mode).Q) : c.state = WorkEmitPhase.scan → (c.work idx).HasBinarySuffix bits → TM.Parked c.input → (∀ (i : Fin n), i ≠ idx → TM.Parked (c.work i)) → c.output.HasBinaryPrefix emitted → ∃ (c' : Complexity.Cfg n (workEmitTM idx mode).Q), (workEmitTM idx mode).reachesIn (workEmitTime bits) c c' ∧ (workEmitTM idx mode).halted c' ∧ c'.input = c.input ∧ (c'.work idx).HasBinarySuffix [] ∧ (c'.work idx).cells = (c.work idx).cells ∧ (c'.work idx).head = (c.work idx).head + bits.length ∧ (∀ (i : Fin n), i ≠ idx → c'.work i = c.work i) ∧ c'.output.HasBinaryPrefix (emitted ++ workEmitBits mode bits)

theorem Complexity.RAM.RegisterStore.Machine.workEmitTM_hoareTime_frame_internal {n : ℕ} (idx : Fin n) (mode : WorkEmitMode) (bits emitted : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsource : (work₀ idx).HasBinarySuffix bits) (hinput : TM.Parked inp₀) (hother : ∀ (i : Fin n), i ≠ idx → TM.Parked (work₀ i)) (houtput : out₀.HasBinaryPrefix emitted) : (workEmitTM idx mode).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 idx).HasBinarySuffix [] ∧ (work idx).cells = (work₀ idx).cells ∧ (work idx).head = (work₀ idx).head + bits.length ∧ (∀ (i : Fin n), i ≠ idx → work i = work₀ i) ∧ out.HasBinaryPrefix (emitted ++ workEmitBits mode bits)) (workEmitTime bits)

theorem Complexity.RAM.RegisterStore.Machine.wordEncodeTM_hoareTime_frame_internal {n : ℕ} (idx : Fin n) (value : ℕ) (emitted : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hvalue : (work₀ idx).HasBinaryNat value) (hinput : TM.Parked inp₀) (hother : ∀ (i : Fin n), i ≠ idx → TM.Parked (work₀ i)) (houtput : out₀.HasBinaryPrefix emitted) : (wordEncodeTM idx).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 idx).HasBinarySuffix [] ∧ (work idx).cells = (work₀ idx).cells ∧ (work idx).head = value.bits.length + 1 ∧ (∀ (i : Fin n), i ≠ idx → work i = work₀ i) ∧ out.HasBinaryPrefix (emitted ++ WordCode.encode value)) (wordEncodeTime value)

theorem Complexity.RAM.RegisterStore.Machine.rewindWordEncodeTM_hoareTime_frame_internal {n : ℕ} (idx : Fin n) (value headBound : ℕ) (emitted : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hcontent : (work₀ idx).HasBinaryContent value.bits) (hstart : (work₀ idx).cells 0 = Γ.start) (hhead : 1 ≤ (work₀ idx).head ∧ (work₀ idx).head ≤ headBound) (hinput : TM.Parked inp₀) (hother : ∀ (i : Fin n), i ≠ idx → TM.Parked (work₀ i)) (houtput : out₀.HasBinaryPrefix emitted) : (rewindWordEncodeTM idx).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 idx).HasBinarySuffix [] ∧ (work idx).cells = (work₀ idx).cells ∧ (work idx).head = value.bits.length + 1 ∧ (∀ (i : Fin n), i ≠ idx → work i = work₀ i) ∧ out.HasBinaryPrefix (emitted ++ WordCode.encode value)) (rewindWordEncodeTime value headBound)