include "joint/Joint.ma".

definition lin_params: params ≝
 mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) unit.

definition lin_statement ≝ joint_statement lin_params.

definition well_formed_P ≝
  λA, B: Type[0].
  λcode: list (option A × B).
    match code with
    [ nil ⇒ False
    | cons hd tl ⇒
      match \fst hd with
      [ Some lbl ⇒ False
      | None ⇒ True]].

(*
definition lin_sem_params_: ∀globals. sem_params_ lin_params globals ≝
 λglobals.
  mk_sem_params_ lin_params globals (Σcode:list (lin_statement globals). well_formed_P … code) ?.
(*CSC: lookup function to be implemented *)
cases daemon
qed.
*)

definition lin_program ≝ joint_program lin_params.