include "LIN/joint_LTL_LIN.ma".

definition ltl_params_ : params_ ≝ graph_params_ ltl_lin_params__.
definition ltl_params: ∀globals. params globals ≝ graph_params ltl_lin_params1.

definition ltl_statement ≝ joint_statement ltl_params_.
definition ltl_program ≝ joint_program ltl_params.

definition ltl_internal_function ≝
 λglobals. joint_internal_function … (ltl_params globals).