include "LIN/joint_LTL_LIN_semantics.ma".
include "LTL/LTL.ma". (* CSC: syntax.ma in RTLabs *)

definition ltl_fullexec ≝
 ltl_lin_fullexec … (graph_succ_p …) … (graph_fetch_statement … (ltl_lin_sem_params …)).