include "joint/Joint.ma".

definition ltl_params__: params__ ≝
 (mk_params__ unit unit unit unit registers_move Register nat unit False).
definition ltl_params_ : params_ ≝ graph_params_ ltl_params__.
definition ltl_params0 : params0 ≝ mk_params0 ltl_params__ unit unit.
definition ltl_params1 : params1 ≝ mk_params1 ltl_params0 unit.
definition ltl_params: ∀globals. params globals ≝ graph_params ltl_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).