Sequential tape safety: proof internals

The standard finite-run decomposition transports arbitrary tape predicates, including projected resource bounds, without another control-flow hierarchy.

theorem Complexity.TM.seqTM_hoareSafety_internal {n : ℕ} (tm₁ tm₂ : TM n) {pre mid mid' post safe : TapePred n} {b₁ b₂ : ℕ} (h₁ : tm₁.HoareTime pre mid b₁) (htrans : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), mid inp work out → mid' (transitionInput inp) (fun (i : Fin n) => transitionTape (work i)) (transitionTape out)) (h₂ : tm₂.HoareTime mid' post b₂) (hs₁ : tm₁.HoareSafety pre safe) (hs₂ : tm₂.HoareSafety mid' safe) : (tm₁.seqTM tm₂).HoareSafety pre safe

Sequential composition preserves any common tape safety predicate. The second contract covers the boundary configuration itself.