(* space complexity *)
definition size_of_tape ≝ λsig.λtp: tape sig.|left sig tp|+|right sig tp|.
definition size_of_tapes ≝ λsig.λn.λtps: Vector (tape sig) n.
foldr ?? (λtp.λacc.max (size_of_tape sig tp) acc) 0 tps.
(* space complexity *)
definition size_of_tape ≝ λsig.λtp: tape sig.|left sig tp|+|right sig tp|.
definition size_of_tapes ≝ λsig.λn.λtps: Vector (tape sig) n.
foldr ?? (λtp.λacc.max (size_of_tape sig tp) acc) 0 tps.