Hoare contracts for output redirection

This module lifts a framed contract through TM.retargetOutput, exposing the source output as the fresh last work tape while pinning the real output to the standard parked blank tape.

theorem Complexity.TM.retargetOutput_hoareTime {n : ℕ} {pre post : TapePred n} {bound : ℕ} (tm : TM n) (h : tm.HoareTime pre post bound) : tm.retargetOutput.HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => pre inp (fun (i : Fin n) => work i.castSucc) (work (Fin.last n)) ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => post inp (fun (i : Fin n) => work i.castSucc) (work (Fin.last n)) ∧ out = (Tape.init []).move Dir3.right) bound

Lift a framed time contract while redirecting the source machine's output to the fresh last work tape.