include "LIN/JointLTLLIN.ma".
  
definition PreLINStatement ≝ JointStatement unit.

definition LINStatement ≝
  λglobals.
    option Identifier × (PreLINStatement globals).

definition WellFormedP ≝
  λ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
      ]
    ].
    
inductive LINFunctionDefinition (globals: list Identifier): Type[0] ≝
  LIN_Fu_Internal: ∀code: list (LINStatement globals). WellFormedP ? ? code → LINFunctionDefinition globals
| LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals.

record LINProgram: Type[0] ≝
{
  LIN_Pr_vars: list (Identifier × nat);
  LIN_Pr_funs: list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) LIN_Pr_vars)));
  LIN_Pr_main: option Identifier
}.

definition LIN_Pr_vars:
    LINProgram → list (Identifier × nat).
  # r
  cases r
  # H1 # H2 #H3
  @ H1
qed.

definition LIN_Pr_funs:
  ∀p: LINProgram.
    list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) (LIN_Pr_vars p)))).
  # r
  cases r
  # H1 # H2 #H3
  @ H2
qed.