include "LIN/JointLTLLIN.ma". definition pre_lin_statement ≝ joint_statement unit. definition lin_statement ≝ λglobals. option ident × (pre_lin_statement globals). 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 ] ]. inductive lin_function_definition (globals: list ident): Type[0] ≝ lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals | lin_fu_external: external_function → lin_function_definition globals. record lin_program: Type[0] ≝ { lin_pr_vars: list (ident × nat); lin_pr_funcs: list (ident × (lin_function_definition (map ? ? (fst ? ?) lin_pr_vars))); lin_pr_main: option ident }.