include "joint/Joint.ma".
include "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_sem_params_: ∀globals. sem_params_ ltl_params globals ≝
 λglobals.
  mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …).*)

definition ltl_program ≝ joint_program ltl_params.