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.