Finite composition of proof-carrying binary routines -- proof internals

theorem Complexity.BinaryRoutine.seqList_sound_internal {n : ℕ} (routines : List (BinaryRoutine n)) (hsound : ∀ routine ∈ routines, routine.Sound) : (seqList routines).Sound

theorem Complexity.BinaryRoutine.repeatRoutine_sound_internal {n : ℕ} (count : ℕ) (routine : BinaryRoutine n) (hsound : routine.Sound) : (repeatRoutine count routine).Sound

theorem Complexity.BinaryRoutine.seqList_append_effect_internal {n : ℕ} (first second : List (BinaryRoutine n)) (values : BinaryValues n) : (seqList (first ++ second)).effect values = (seqList second).effect ((seqList first).effect values)

theorem Complexity.BinaryRoutine.seqList_ofFn_effect_eq_trajectory_internal {n : ℕ} (count : ℕ) (routineAt : Fin count → BinaryRoutine n) (initial : BinaryValues n) (trajectory : ℕ → BinaryValues n) (hzero : trajectory 0 = initial) (hstep : ∀ (index : Fin count), (routineAt index).effect (trajectory ↑index) = trajectory (↑index + 1)) : (seqList (List.ofFn routineAt)).effect initial = trajectory count