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.
unification hint 0 ≔ ⊢ lin_program ≡ joint_program LIN.

definition LIN_premain : ∀p : lin_program.
  joint_closed_internal_function LIN (prog_names … p) ≝
λp.
let l3 : label ≝ an_identifier … (p1 one) in
let code ≝
  [〈None ?, sequential … (COST_LABEL LIN ? (init_cost_label … p)) it〉 ;
   〈None ?, sequential … (CALL LIN ? (inl … (prog_main … p)) 0 it) it〉 ;
   〈Some ? l3, GOTO ? l3〉 ] in
mk_joint_internal_function LIN (prog_names … p)
  (mk_universe … (p0 (p0 one)))
  (mk_universe … one)
  it it 0 0 0 code 0.
%
[ * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%?→?); #EQ destruct
  % try @I
  [ %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct
  |*: % whd in ⊢ (??%%→?); #EQ destruct
  ]
| * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I}
| ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); //
| * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%%→?); #EQ destruct @I
| %{it} %{(init_cost_label … p)} %
]
qed.