include "joint/Joint.ma".

definition ltl_params_: params_ ≝
 label_params__of_params__
  (mk_params__ unit unit unit unit registers_move Register nat unit False unit
    unit unit).

definition ltl_statement ≝ joint_statement ltl_params_.

definition ltl_params: ∀globals. params globals ≝ graph_params ltl_params_.

definition ltl_program ≝ joint_program ltl_params.

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