include "LIN/joint_LTL_LIN_paolo.ma".

definition lin_params ≝ mk_lin_params ltl_lin_params.

(* aid unification *)
unification hint 0 ≔
(*---------------*) ⊢
acc_a_reg lin_params ≡ unit.
unification hint 0 ≔
(*---------------*) ⊢
acc_a_arg lin_params ≡ unit.
unification hint 0 ≔
(*---------------*) ⊢
acc_b_reg lin_params ≡ unit.
unification hint 0 ≔
(*---------------*) ⊢
acc_a_arg lin_params ≡ unit.
unification hint 0 ≔
(*---------------*) ⊢
snd_arg lin_params ≡ ltl_argument.
unification hint 0 ≔
(*---------------*) ⊢
ext_seq lin_params ≡ ltl_lin_seq.
unification hint 0 ≔
(*---------------*) ⊢
pair_move lin_params ≡ registers_move.

definition lin_program ≝ joint_program lin_params.