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).