include "joint/Joint.ma".
include alias "common/Graphs.ma".

definition ltl_params_: params_ ≝
 mk_params_ (mk_params__ unit unit unit unit registers_move Register False unit unit unit) label.

definition ltl_statement ≝ joint_statement ltl_params_.

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

definition ltl_program ≝ joint_program ltl_params.