include "LIN/joint_LTL_LIN.ma".

definition LIN ≝ mk_lin_params LTL_LIN.

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

definition lin_program ≝ joint_program LIN.