(* PATH-LABELED SEQUENTIAL COMPUTATION (MULTISTEP) *******************************)
(* Note: lstar shuld be replaced by l_sreds *)
(* PATH-LABELED SEQUENTIAL COMPUTATION (MULTISTEP) *******************************)
(* Note: lstar shuld be replaced by l_sreds *)