include "joint/Joint.ma".

inductive registers_move: Type[0] ≝
 | from_acc: Register → registers_move
 | to_acc: Register → registers_move.

definition ltl_lin_params__: params__ ≝
 mk_params__ unit unit unit unit registers_move Register nat unit False.
definition ltl_lin_params0 : params0 ≝ mk_params0 ltl_lin_params__ unit unit.
definition ltl_lin_params1 : params1 ≝ mk_params1 ltl_lin_params0 unit.