Module LSemDeterminism

From Coq Require Import String.
From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.

From Velus Require Import Common.
From Velus Require Import CommonList.
From Velus Require Import FunctionalEnvironment.
From Velus Require Import Operators.
From Velus Require Import CoindStreams.
From Velus Require Import Clocks.
From Velus Require Import Lustre.StaticEnv.
From Velus Require Import Lustre.LSyntax Lustre.LTyping Lustre.LCausality Lustre.LOrdered Lustre.LSemantics.

Proof of the determinism of the coinductive semantics We can proove that the semantics of a causal program are deterministic: That is, a node always return the same output for a given input.

Module Type LSEMDETERMINISM
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Ids Op)
       (Import Cks : CLOCKS Ids Op OpAux)
       (Import Senv : STATICENV Ids Op OpAux Cks)
       (Import Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Import Typ : LTYPING Ids Op OpAux Cks Senv Syn)
       (Import LCA : LCAUSALITY Ids Op OpAux Cks Senv Syn)
       (Import Lord : LORDERED Ids Op OpAux Cks Senv Syn)
       (Import CStr : COINDSTREAMS Ids Op OpAux Cks)
       (Import Sem : LSEMANTICS Ids Op OpAux Cks Senv Syn Lord CStr).

  Import List.

  Definition det_nodes {PSyn prefs} (G : @global PSyn prefs) := forall f n ins1 ins2 outs1 outs2,
      Forall2 (EqStN n) ins1 ins2 ->
      sem_node G f ins1 outs1 ->
      sem_node G f ins2 outs2 ->
      Forall2 (EqStN n) outs1 outs2.

  Lemma det_nodes_ins {PSyn prefs} : forall (G : @global PSyn prefs) f ins outs1 outs2,
      det_nodes G ->
      sem_node G f ins outs1 ->
      sem_node G f ins outs2 ->
      EqSts outs1 outs2.

  Lemma EqStN_mask {A} (absent : A) : forall n rs1 rs2 xs1 xs2,
      EqStN n rs1 rs2 ->
      EqStN n xs1 xs2 ->
      forall k, EqStN n (mask absent k rs1 xs1) (mask absent k rs2 xs2).

  Corollary EqStNs_mask {A} (absent : A) : forall n rs1 rs2 xs1 xs2,
      EqStN n rs1 rs2 ->
      Forall2 (EqStN n) xs1 xs2 ->
      forall k, Forall2 (EqStN n) (List.map (mask absent k rs1) xs1) (List.map (mask absent k rs2) xs2).

  Global Hint Resolve EqStN_mask EqStNs_mask : coindstreams.

  Lemma EqStN_unmask {A} (absent : A) : forall n rs1 rs2 xs1 xs2,
      EqStN n rs1 rs2 ->
      (forall k, EqStN n (mask absent k rs1 xs1) (mask absent k rs2 xs2)) ->
      EqStN n xs1 xs2.

  Corollary EqStNs_unmask {A} (absent : A) : forall n rs1 rs2 xs1 xs2,
      EqStN n rs1 rs2 ->
      (forall k, Forall2 (EqStN n) (List.map (mask absent k rs1) xs1) (List.map (mask absent k rs2) xs2)) ->
      Forall2 (EqStN n) xs1 xs2.

  Global Hint Resolve EqStN_unmask EqStNs_unmask : coindstreams.

  Section sem_equation_det.
    Context {PSyn : list decl -> block -> Prop}.
    Context {prefs : PS.t}.
    Variable (G : @global PSyn prefs).

    Hypothesis HdetG : det_nodes G.

    Variable Γ : static_env.

    Definition det_var n (Hi1 Hi2 : history) x :=
      forall vs1 vs2,
        sem_var Hi1 x vs1 ->
        sem_var Hi2 x vs2 ->
        EqStN n vs1 vs2.

    Definition det_var_inv n (Hi1 Hi2 : history) : ident -> Prop :=
      fun cx => (forall x, HasCaus Γ x cx -> det_var n Hi1 Hi2 (Var x))
             /\ (forall x, HasLastCaus Γ x cx -> det_var n Hi1 Hi2 (Last x)).

    Definition def_stream := Streams.const (@absent value).

    Definition det_exp_inv n H1 H2 bs1 bs2 : exp -> nat -> Prop :=
      fun e k => forall ss1 ss2,
          wt_exp G Γ e ->
          sem_exp G H1 bs1 e ss1 ->
          sem_exp G H2 bs2 e ss2 ->
          EqStN n (nth k ss1 def_stream) (nth k ss2 def_stream).

    Lemma P_exps_det_exp_inv : forall n H1 H2 bs1 bs2 es k ss1 ss2,
        Forall (wt_exp G Γ) es ->
        P_exps (det_exp_inv n H1 H2 bs1 bs2) es k ->
        Forall2 (sem_exp G H1 bs1) es ss1 ->
        Forall2 (sem_exp G H2 bs2) es ss2 ->
        EqStN n (nth k (concat ss1) def_stream) (nth k (concat ss2) def_stream).

    Lemma Forall2Brs_det_exp_inv : forall n H1 H2 bs1 bs2 es k ss1 ss2,
        k < length ss1 ->
        Forall (fun es => Forall (wt_exp G Γ) (snd es)) es ->
        Forall (fun es => P_exps (det_exp_inv n H1 H2 bs1 bs2) (snd es) k) es ->
        Forall2Brs (sem_exp G H1 bs1) es ss1 ->
        Forall2Brs (sem_exp G H2 bs2) es ss2 ->
        Forall2 (fun xs1 xs2 => EqStN n (snd xs1) (snd xs2)) (nth k ss1 []) (nth k ss2 []).

    Lemma P_exps_det_exp_inv_all : forall n H1 H2 bs1 bs2 es ss1 ss2,
        Forall (wt_exp G Γ) es ->
        (forall k, k < length (annots es) -> P_exps (det_exp_inv n H1 H2 bs1 bs2) es k) ->
        Forall2 (sem_exp G H1 bs1) es ss1 ->
        Forall2 (sem_exp G H2 bs2) es ss2 ->
        Forall2 (EqStN n) (concat ss1) (concat ss2).


    Hint Constructors EqStN : core.

    Lemma const_detn : forall n bs1 bs2 c,
        EqStN n bs1 bs2 ->
        EqStN n (const bs1 c) (const bs2 c).

    Lemma enum_detn : forall n bs1 bs2 c,
        EqStN n bs1 bs2 ->
        EqStN n (enum bs1 c) (enum bs2 c).

    Lemma lift1_detn : forall n op ty xs1 xs2 ys1 ys2,
        EqStN n xs1 xs2 ->
        lift1 op ty xs1 ys1 ->
        lift1 op ty xs2 ys2 ->
        EqStN n ys1 ys2.

    Lemma lift2_detn : forall n op ty1 ty2 xs11 xs12 xs21 xs22 ys1 ys2,
        EqStN n xs11 xs21 ->
        EqStN n xs12 xs22 ->
        lift2 op ty1 ty2 xs11 xs12 ys1 ->
        lift2 op ty1 ty2 xs21 xs22 ys2 ->
        EqStN n ys1 ys2.

    Lemma liftn_detn : forall n f tyins tyout xss1 xss2 ys1 ys2,
        xss1 <> [] ->
        Forall2 (EqStN n) xss1 xss2 ->
        liftn (fun vs v => sem_extern f tyins vs tyout v) xss1 ys1 ->
        liftn (fun vs v => sem_extern f tyins vs tyout v) xss2 ys2 ->
        EqStN n ys1 ys2.

    Corollary fby_detn {A} : forall n (xs1 xs2 ys1 ys2 zs1 zs2 : Stream (synchronous A)),
        EqStN n xs1 xs2 ->
        EqStN n ys1 ys2 ->
        fby xs1 ys1 zs1 ->
        fby xs2 ys2 zs2 ->
        EqStN n zs1 zs2.

    Lemma arrow_detn : forall n xs1 xs2 ys1 ys2 zs1 zs2,
        EqStN n xs1 xs2 ->
        EqStN n ys1 ys2 ->
        arrow xs1 ys1 zs1 ->
        arrow xs2 ys2 zs2 ->
        EqStN n zs1 zs2.

    Lemma when_detn : forall n k xs1 xs2 ys1 ys2 zs1 zs2,
        EqStN n xs1 xs2 ->
        EqStN n ys1 ys2 ->
        when k xs1 ys1 zs1 ->
        when k xs2 ys2 zs2 ->
        EqStN n zs1 zs2.

    Lemma merge_detn : forall n cs1 cs2 xss1 xss2 ys1 ys2,
        map fst xss1 = map fst xss2 ->
        NoDupMembers xss1 ->
        EqStN n cs1 cs2 ->
        Forall2 (fun xs1 xs2 => EqStN n (snd xs1) (snd xs2)) xss1 xss2 ->
        merge cs1 xss1 ys1 ->
        merge cs2 xss2 ys2 ->
        EqStN n ys1 ys2.

    Lemma case_detn : forall n cs1 cs2 xss1 xss2 ys1 ys2 ds1 ds2,
        map fst xss1 = map fst xss2 ->
        NoDupMembers xss1 ->
        EqStN n cs1 cs2 ->
        Forall2 (fun xs1 xs2 => EqStN n (snd xs1) (snd xs2)) xss1 xss2 ->
        (forall d1 d2, ds1 = Some d1 -> ds2 = Some d2 -> EqStN n d1 d2) ->
        case cs1 xss1 ds1 ys1 ->
        case cs2 xss2 ds2 ys2 ->
        EqStN n ys1 ys2.

    Lemma bools_of_detn : forall n xs1 xs2 bs1 bs2,
        EqStN n xs1 xs2 ->
        bools_of xs1 bs1 ->
        bools_of xs2 bs2 ->
        EqStN n bs1 bs2.

    Lemma disj_str_detn : forall n xss1 xss2 bs1 bs2,
        Forall2 (EqStN n) xss1 xss2 ->
        bs1 ≡ disj_str xss1 ->
        bs2 ≡ disj_str xss2 ->
        EqStN n bs1 bs2.

    Corollary bools_ofs_detn : forall n xss1 xss2 bs1 bs2,
        Forall2 (EqStN n) xss1 xss2 ->
        bools_ofs xss1 bs1 ->
        bools_ofs xss2 bs2 ->
        EqStN n bs1 bs2.

    Fact det_exps_n' : forall n Hi1 Hi2 bs1 bs2 es ss1 ss2,
        Forall (fun e => forall ss1 ss2,
                    wt_exp G Γ e ->
                    sem_exp G Hi1 bs1 e ss1 ->
                    sem_exp G Hi2 bs2 e ss2 ->
                    Forall2 (EqStN n) ss1 ss2) es ->
        Forall (wt_exp G Γ) es->
        Forall2 (sem_exp G Hi1 bs1) es ss1 ->
        Forall2 (sem_exp G Hi2 bs2) es ss2 ->
        Forall2 (EqStN n) (concat ss1) (concat ss2).

    Lemma Forall2Brs_det_exp_n' : forall n H1 H2 bs1 bs2 es ss1 ss2,
        Forall
          (fun es =>
             Forall
               (fun e =>
                  forall ss1 ss2,
                    wt_exp G Γ e ->
                    sem_exp G H1 bs1 e ss1 -> sem_exp G H2 bs2 e ss2 -> Forall2 (EqStN n) ss1 ss2)
               (snd es)) es ->
        length ss1 = length ss2 ->
        Forall (fun es => Forall (wt_exp G Γ) (snd es)) es ->
        Forall2Brs (sem_exp G H1 bs1) es ss1 ->
        Forall2Brs (sem_exp G H2 bs2) es ss2 ->
        Forall2 (Forall2 (fun xs1 xs2 => EqStN n (snd xs1) (snd xs2))) ss1 ss2.

    Lemma det_exp_n : forall n Hi1 Hi2 bs1 bs2 e ss1 ss2,
        (forall x cx, HasCaus Γ x cx \/ HasLastCaus Γ x cx -> det_var_inv n Hi1 Hi2 cx) ->
        EqStN n bs1 bs2 ->
        wt_exp G Γ e ->
        sem_exp G Hi1 bs1 e ss1 ->
        sem_exp G Hi2 bs2 e ss2 ->
        Forall2 (EqStN n) ss1 ss2.

    Corollary det_exps_n : forall n Hi1 Hi2 bs1 bs2 es ss1 ss2,
        (forall x cx, HasCaus Γ x cx \/ HasLastCaus Γ x cx -> det_var_inv n Hi1 Hi2 cx) ->
        EqStN n bs1 bs2 ->
        Forall (wt_exp G Γ) es ->
        Forall2 (sem_exp G Hi1 bs1) es ss1 ->
        Forall2 (sem_exp G Hi2 bs2) es ss2 ->
        Forall2 (EqStN n) (concat ss1) (concat ss2).

    Corollary det_exp : forall Hi bs e ss1 ss2,
        wt_exp G Γ e ->
        sem_exp G Hi bs e ss1 ->
        sem_exp G Hi bs e ss2 ->
        EqSts ss1 ss2.

    Corollary det_exps : forall Hi bs es ss1 ss2,
        Forall (wt_exp G Γ) es ->
        Forall2 (sem_exp G Hi bs) es ss1 ->
        Forall2 (sem_exp G Hi bs) es ss2 ->
        EqSts (concat ss1) (concat ss2).


    Lemma fby_det_Sn {A} : forall n (xs1 xs2 ys1 ys2 zs1 zs2 : Stream (synchronous A)),
        EqStN (S n) xs1 xs2 ->
        EqStN n ys1 ys2 ->
        fby xs1 ys1 zs1 ->
        fby xs2 ys2 zs2 ->
        EqStN (S n) zs1 zs2.

    Lemma det_exp_S : forall n Hi1 Hi2 bs1 bs2 e k,
        (forall x cx, HasCaus Γ x cx \/ HasLastCaus Γ x cx -> det_var_inv n Hi1 Hi2 cx) ->
        wt_exp G Γ e ->
        k < numstreams e ->
        EqStN (S n) bs1 bs2 ->
        (forall x, Is_used_inst Γ x k e -> det_var_inv (S n) Hi1 Hi2 x) ->
        det_exp_inv (S n) Hi1 Hi2 bs1 bs2 e k.

    Hypothesis Hnd : NoDup (map snd (idcaus_of_senv Γ)).

    Lemma det_equation_S : forall n Hi1 Hi2 bs1 bs2 xs es k cx,
        wt_equation G Γ (xs, es) ->
        Sem.sem_equation G Hi1 bs1 (xs, es) ->
        Sem.sem_equation G Hi2 bs2 (xs, es) ->
        k < length xs ->
        P_exps (det_exp_inv (S n) Hi1 Hi2 bs1 bs2) es k ->
        HasCaus Γ (nth k xs xH) cx ->
        det_var_inv (S n) Hi1 Hi2 cx.

  End sem_equation_det.

  Lemma sem_clock_detN n Γ : forall ck bs1 bs2 Hi1 Hi2 bs1' bs2',
      EqStN n bs1 bs2 ->
      wx_clock Γ ck ->
      (forall x cx, Is_free_in_clock x ck -> HasCaus Γ x cx -> det_var_inv Γ n Hi1 Hi2 cx) ->
      sem_clock (var_history Hi1) bs1 ck bs1' ->
      sem_clock (var_history Hi2) bs2 ck bs2' ->
      EqStN n bs1' bs2'.

  Lemma det_var_inv_mask : forall Γ n rs1 rs2 Hi1 Hi2 x,
      EqStN n rs1 rs2 ->
      det_var_inv Γ n Hi1 Hi2 x ->
      forall k, det_var_inv Γ n (mask_hist k rs1 Hi1) (mask_hist k rs2 Hi2) x.

  Lemma det_var_unmask : forall n rs1 rs2 Hi1 Hi2 x,
      EqStN n rs1 rs2 ->
      (forall k, det_var n (mask_hist k rs1 Hi1) (mask_hist k rs2 Hi2) x) ->
      det_var n Hi1 Hi2 x.

  Corollary det_var_inv_unmask : forall Γ n rs1 rs2 Hi1 Hi2 x,
      EqStN n rs1 rs2 ->
      (forall k, det_var_inv Γ n (mask_hist k rs1 Hi1) (mask_hist k rs2 Hi2) x) ->
      det_var_inv Γ n Hi1 Hi2 x.

  Lemma EqStN_fwhen {A} (absent : A) : forall n sc1 sc2 xs1 xs2,
      EqStN n sc1 sc2 ->
      EqStN n xs1 xs2 ->
      forall c, EqStN n (fwhen absent c xs1 sc1) (fwhen absent c xs2 sc2).

  Lemma EqStN_unwhen : forall n tx tn sc1 sc2 xs1 xs2,
      0 < length tn ->
      wt_stream sc1 (Tenum tx tn) ->
      wt_stream sc2 (Tenum tx tn) ->
      EqStN n sc1 sc2 ->
      (forall sel, In sel (seq 0 (length tn)) ->
              exists xs1' xs2',
                when sel xs1 sc1 xs1'
                /\ when sel xs2 sc2 xs2'
                /\ EqStN n xs1' xs2') ->
      EqStN n xs1 xs2.

  Lemma det_var_inv_when : forall Γ n sc1 sc2 Hi1 Hi2 Hi1' Hi2' x,
      EqStN n sc1 sc2 ->
      det_var_inv Γ n Hi1 Hi2 x ->
      forall c, when_hist c Hi1 sc1 Hi1' ->
           when_hist c Hi2 sc2 Hi2' ->
           det_var_inv Γ n Hi1' Hi2' x.

  Lemma det_var_unwhen : forall tx tn n sc1 sc2 Hi1 Hi2 x,
      0 < length tn ->
      wt_stream sc1 (Tenum tx tn) ->
      wt_stream sc2 (Tenum tx tn) ->
      EqStN n sc1 sc2 ->
      (forall c, In c (seq 0 (length tn)) ->
            exists Hi1' Hi2',
              (FEnv.In (Var x) Hi1' /\ FEnv.In (Var x) Hi2')
              /\ when_hist c Hi1 sc1 Hi1'
              /\ when_hist c Hi2 sc2 Hi2'
              /\ det_var n Hi1' Hi2' (Var x)) ->
      det_var n Hi1 Hi2 (Var x).

  Fact det_var_inv_weaken Γ n : forall Hi1 Hi2 x,
      det_var_inv Γ (S n) Hi1 Hi2 x ->
      det_var_inv Γ n Hi1 Hi2 x.

  Lemma EqStN_fselect {A} (absent : A) : forall n sc1 sc2 xs1 xs2,
      EqStN n sc1 sc2 ->
      EqStN n xs1 xs2 ->
      forall c k, EqStN n (fselect absent c k sc1 xs1) (fselect absent c k sc2 xs2).

  Lemma EqStN_unselect : forall n tn sc1 sc2 xs1 xs2,
      0 < tn ->
      EqStN n sc1 sc2 ->
      SForall (fun v => match v with present (e, _) => e < tn | _ => True end) sc1 ->
      SForall (fun v => match v with present (e, _) => e < tn | _ => True end) sc2 ->
      (forall sel k, In sel (seq 0 tn) ->
                exists xs1' xs2',
                  select sel k sc1 xs1 xs1'
                  /\ select sel k sc2 xs2 xs2'
                  /\ EqStN n xs1' xs2') ->
      EqStN n xs1 xs2.

  Lemma EqStN_unfselect {A} : forall n tn sc1 sc2 xs1 xs2,
      0 < tn ->
      EqStN n sc1 sc2 ->
      SForall (fun v => match v with present (e, _) => e < tn | _ => True end) sc1 ->
      SForall (fun v => match v with present (e, _) => e < tn | _ => True end) sc2 ->
      slower xs1 (abstract_clock sc1) ->
      slower xs2 (abstract_clock sc2) ->
      (forall sel k, In sel (seq 0 tn) ->
                EqStN n (fselect (@absent A) sel k sc1 xs1) (fselect (@absent A) sel k sc2 xs2)) ->
      EqStN n xs1 xs2.

  Lemma det_var_inv_select : forall Γ n sc1 sc2 Hi1 Hi2 Hi1' Hi2' x,
      EqStN n sc1 sc2 ->
      det_var_inv Γ n Hi1 Hi2 x ->
      forall c k, select_hist c k sc1 Hi1 Hi1' ->
             select_hist c k sc2 Hi2 Hi2' ->
             det_var_inv Γ n Hi1' Hi2' x.

  Lemma det_var_unselect : forall tn n sc1 sc2 Hi1 Hi2 x,
      0 < tn ->
      EqStN n sc1 sc2 ->
      SForall (fun v => match v with present (e, _) => e < tn | _ => True end) sc1 ->
      SForall (fun v => match v with present (e, _) => e < tn | _ => True end) sc2 ->
      (forall c k, In c (seq 0 tn) ->
              exists Hi1' Hi2',
                (FEnv.In (Var x) Hi1' /\ FEnv.In (Var x) Hi2')
                /\ select_hist c k sc1 Hi1 Hi1'
                /\ select_hist c k sc2 Hi2 Hi2'
                /\ det_var n Hi1' Hi2' (Var x)) ->
      det_var n Hi1 Hi2 (Var x).

  Lemma const_stres_detn {A} n : forall (x : A) bs1 bs2,
      EqStN n bs1 bs2 ->
      EqStN n (const_stres bs1 x) (const_stres bs2 x).

  Lemma first_of_detn {A} n : forall (v : A) bs1 bs2 ys1 ys2,
      EqStN n bs1 bs2 ->
      EqStN n ys1 ys2 ->
      EqStN n (first_of v bs1 ys1) (first_of v bs2 ys2).

  Lemma sem_transitions_detn {PSyn prefs} (G: @global PSyn prefs) Γ n :
    forall Hi1 Hi2 bs1 bs2 trans def stres1 stres2,
      det_nodes G ->
      Forall (fun '(e, (t, _)) => wt_exp G Γ e) trans ->
      (forall x cx, HasCaus Γ x cx \/ HasLastCaus Γ x cx -> det_var_inv Γ n Hi1 Hi2 cx) ->
      EqStN n bs1 bs2 ->
      sem_transitions G Hi1 bs1 trans def stres1 ->
      sem_transitions G Hi2 bs2 trans def stres2 ->
      EqStN n stres1 stres2.

  Lemma sem_transitions_detS {PSyn prefs} (G: @global PSyn prefs) Γ n :
    forall Hi1 Hi2 bs1 bs2 trans def stres1 stres2,
      det_nodes G ->
      Forall (fun '(e, (t, _)) => wt_exp G Γ e /\ typeof e = [bool_velus_type]) trans ->
      (forall x cx, HasCaus Γ x cx \/ HasLastCaus Γ x cx -> det_var_inv Γ n Hi1 Hi2 cx) ->
      (forall x cx, HasCaus Γ x cx \/ HasLastCaus Γ x cx -> Exists (fun '(e, _) => Is_used_inst Γ cx 0 e) trans -> det_var_inv Γ (S n) Hi1 Hi2 cx) ->
      EqStN (S n) bs1 bs2 ->
      sem_transitions G Hi1 bs1 trans def stres1 ->
      sem_transitions G Hi2 bs2 trans def stres2 ->
      EqStN (S n) stres1 stres2.

  Fact det_var_inv_local :
    forall Γ (locs : list decl) Hi1 Hi2 Hi1' Hi2' n cx,
      (forall x : ident, InMembers x locs -> ~ In x (map fst Γ)) ->
      dom Hi1' (senv_of_decls locs) ->
      dom Hi2' (senv_of_decls locs) ->
      det_var_inv Γ n Hi1 Hi2 cx ->
      det_var_inv (senv_of_decls locs) n Hi1' Hi2' cx ->
      det_var_inv (Γ ++ senv_of_decls locs) n (Hi1 + Hi1') (Hi2 + Hi2') cx.

  Fact det_var_inv_branch :
    forall Γ caus Hi1 Hi2 n cx,
      (forall x, HasCaus Γ x cx \/ HasLastCaus Γ x cx -> det_var_inv Γ n Hi1 Hi2 cx) ->
      (forall x vs1 vs2, In (x, cx) caus -> sem_var Hi1 (Var x) vs1 -> sem_var Hi2 (Var x) vs2 -> EqStN n vs1 vs2) ->
      det_var_inv (replace_idcaus caus Γ) n Hi1 Hi2 cx.

  Section sem_block_det.
    Context {prefs : PS.t}.
    Variable (G: @global complete prefs).

    Section sem_scope.

      Context {A : Type}.

      Variable sem_block : history -> history -> A -> Prop.

      Inductive sem_scope_det (n : nat) (envS : list ident) : history -> history -> scope A -> Prop :=
      | Sscope : forall Hi1 Hi2 Hi1' Hi2' locs blks,
          dom Hi1' (senv_of_decls locs) ->
          dom Hi2' (senv_of_decls locs) ->

          sem_block (Hi1 + Hi1') (Hi2 + Hi2') blks ->

          (forall cx, det_var_inv (senv_of_decls locs) n Hi1' Hi2' cx) ->
          (forall cx, In cx envS -> det_var_inv (senv_of_decls locs) (S n) Hi1' Hi2' cx) ->
          sem_scope_det n envS Hi1 Hi2 (Scope locs blks).
    End sem_scope.

    Section sem_branch.

      Context {A : Type}.

      Variable sem_block : A -> Prop.

      Variable must_def : ident -> Prop.
      Variable is_def : ident -> A -> Prop.

      Inductive sem_branch_det (n : nat) (envS : list ident) : history -> history -> branch A -> Prop :=
      | Sbranch : forall Hi1 Hi2 caus blks,
          sem_block blks ->
          (forall x, must_def x -> ~is_def x blks -> exists vs, sem_var Hi1 (Last x) vs /\ sem_var Hi1 (Var x) vs) ->
          (forall x, must_def x -> ~is_def x blks -> exists vs, sem_var Hi2 (Last x) vs /\ sem_var Hi2 (Var x) vs) ->

          Forall (fun '(x, _) => det_var n Hi1 Hi2 (Var x)) caus ->
          Forall (fun '(x, cx) => In cx envS -> det_var (S n) Hi1 Hi2 (Var x)) caus ->
          sem_branch_det n envS Hi1 Hi2 (Branch caus blks).

      Inductive sem_branch_det' : history -> history -> branch A -> Prop :=
      | Sbranch' : forall Hi1 Hi2 caus blks,
          sem_block blks ->
          (forall x, must_def x -> ~is_def x blks -> exists vs, sem_var Hi1 (Last x) vs /\ sem_var Hi1 (Var x) vs) ->
          (forall x, must_def x -> ~is_def x blks -> exists vs, sem_var Hi2 (Last x) vs /\ sem_var Hi2 (Var x) vs) ->
          sem_branch_det' Hi1 Hi2 (Branch caus blks).
    End sem_branch.

    Inductive sem_block_det (n : nat) (envS : list ident) : history -> history -> Stream bool -> Stream bool -> block -> Prop :=
    | Sdetbeq : forall Hi1 Hi2 bs1 bs2 eq,
        sem_equation G Hi1 bs1 eq ->
        sem_equation G Hi2 bs2 eq ->
        sem_block_det n envS Hi1 Hi2 bs1 bs2 (Beq eq)

    | Sdetlast : forall Hi1 Hi2 bs1 bs2 x e vs01 vs02 vs11 vs12 vs1 vs2,
        sem_exp G Hi1 bs1 e [vs01] -> sem_var Hi1 (Var x) vs11 -> fby vs01 vs11 vs1 -> sem_var Hi1 (Last x) vs1 ->
        sem_exp G Hi2 bs2 e [vs02] -> sem_var Hi2 (Var x) vs12 -> fby vs02 vs12 vs2 -> sem_var Hi2 (Last x) vs2 ->
        sem_block_det n envS Hi1 Hi2 bs1 bs2 (Blast x e)

    | Sdetreset : forall Hi1 Hi2 bs1 bs2 blocks er sr1 sr2 r1 r2,
        sem_exp G Hi1 bs1 er [sr1] ->
        sem_exp G Hi2 bs2 er [sr2] ->
        bools_of sr1 r1 ->
        bools_of sr2 r2 ->
        (forall k, Forall (sem_block_det n envS (mask_hist k r1 Hi1) (mask_hist k r2 Hi2) (maskb k r1 bs1) (maskb k r2 bs2)) blocks) ->
        sem_block_det n envS Hi1 Hi2 bs1 bs2 (Breset blocks er)

    | Sdetswitch : forall Hi1 Hi2 bs1 bs2 branches ec sc1 sc2,
        sem_exp G Hi1 bs1 ec [sc1] ->
        sem_exp G Hi2 bs2 ec [sc2] ->
        wt_streams [sc1] (typeof ec) ->
        wt_streams [sc2] (typeof ec) ->
        Forall (fun blks => exists Hi1' Hi2',
                    when_hist (fst blks) Hi1 sc1 Hi1'
                    /\ when_hist (fst blks) Hi2 sc2 Hi2'
                    /\ let bi1 := fwhenb (fst blks) bs1 sc1 in
                      let bi2 := fwhenb (fst blks) bs2 sc2 in
                      sem_branch_det (Forall (sem_block_det n envS Hi1' Hi2' bi1 bi2))
                        (fun x => Syn.Is_defined_in (Var x) (Bswitch ec branches))
                        (fun x => List.Exists (Syn.Is_defined_in (Var x)))
                        n envS Hi1' Hi2' (snd blks)) branches ->
        sem_block_det n envS Hi1 Hi2 bs1 bs2 (Bswitch ec branches)

    | SdetautoWeak:
      forall Hi1 Hi2 bs1 bs2 ini oth states ck bs'1 bs'2 stres01 stres11 stres1 stres02 stres12 stres2,
        sem_clock (var_history Hi1) bs1 ck bs'1 ->
        sem_clock (var_history Hi2) bs2 ck bs'2 ->
        sem_transitions G Hi1 bs'1 (List.map (fun '(e, t) => (e, (t, false))) ini) (oth, false) stres01 ->
        sem_transitions G Hi2 bs'2 (List.map (fun '(e, t) => (e, (t, false))) ini) (oth, false) stres02 ->
        fby stres01 stres11 stres1 ->
        fby stres02 stres12 stres2 ->
        EqStN n stres11 stres12 ->
        Forall (fun state =>
                  let tag := fst (fst state) in
                  forall k, exists Hik1 Hik2,
                    select_hist tag k stres1 Hi1 Hik1
                    /\ select_hist tag k stres2 Hi2 Hik2
                    /\ let bik1 := fselectb tag k stres1 bs1 in
                      let bik2 := fselectb tag k stres2 bs2 in
                      sem_branch_det
                        (fun blks =>
                           sem_scope_det (fun Hi1 Hi2 blks =>
                                            Forall (sem_block_det n envS Hi1 Hi2 bik1 bik2) (fst blks)
                                            /\ sem_transitions G Hi1 bik1 (snd blks) (tag, false) (fselect absent tag k stres1 stres11)
                                            /\ sem_transitions G Hi2 bik2 (snd blks) (tag, false) (fselect absent tag k stres2 stres12))
                             n envS Hik1 Hik2 (snd blks))
                        (fun x => Syn.Is_defined_in (Var x) (Bauto Weak ck (ini, oth) states))
                        (fun x '(_, s) => Syn.Is_defined_in_scope (fun '(blks, _) => List.Exists (Syn.Is_defined_in (Var x)) blks) (Var x) s)
                        n envS Hik1 Hik2 (snd state)) states ->
        sem_block_det n envS Hi1 Hi2 bs1 bs2 (Bauto Weak ck (ini, oth) states)

    | SdetautoStrong:
      forall Hi1 Hi2 bs1 bs2 ini states ck bs'1 bs'2 stres11 stres1 stres12 stres2,
        sem_clock (var_history Hi1) bs1 ck bs'1 ->
        sem_clock (var_history Hi2) bs2 ck bs'2 ->
        fby (const_stres bs'1 (ini, false)) stres11 stres1 ->
        fby (const_stres bs'2 (ini, false)) stres12 stres2 ->
        Forall (fun state =>
                  let tag := fst (fst state) in
                  forall k, exists Hik1 Hik2,
                    select_hist tag k stres1 Hi1 Hik1
                    /\ select_hist tag k stres2 Hi2 Hik2
                    /\ let bik1 := fselectb tag k stres1 bs1 in
                      let bik2 := fselectb tag k stres2 bs2 in
                      sem_branch_det'
                        (fun blks =>
                           sem_transitions G Hik1 bik1 (fst blks) (tag, false) (fselect absent (tag) k stres1 stres11)
                           /\ sem_transitions G Hik2 bik2 (fst blks) (tag, false) (fselect absent (tag) k stres2 stres12))
                        (fun x => Syn.Is_defined_in (Var x) (Bauto Strong ck ([], ini) states))
                        (fun x '(_, s) => Syn.Is_defined_in_scope (fun '(blks, _) => List.Exists (Syn.Is_defined_in (Var x)) blks) (Var x) s)
                        Hik1 Hik2 (snd state)) states ->
        EqStN n stres11 stres12 ->
        Forall (fun state =>
                  let tag := fst (fst state) in
                  forall k, exists Hik1 Hik2,
                    select_hist tag k stres11 Hi1 Hik1
                    /\ select_hist tag k stres12 Hi2 Hik2
                    /\ let bik1 := fselectb tag k stres11 bs1 in
                      let bik2 := fselectb tag k stres12 bs2 in
                      sem_branch_det
                        (fun blks =>
                           sem_scope_det (fun Hi1 Hi2 blks => Forall (sem_block_det n envS Hi1 Hi2 bik1 bik2) (fst blks))
                             n envS Hik1 Hik2 (snd blks))
                        (fun x => Syn.Is_defined_in (Var x) (Bauto Strong ck ([], ini) states))
                        (fun x '(_, s) => Syn.Is_defined_in_scope (fun '(blks, _) => List.Exists (Syn.Is_defined_in (Var x)) blks) (Var x) s)
                        n envS Hik1 Hik2 (snd state)) states ->
        sem_block_det n envS Hi1 Hi2 bs1 bs2 (Bauto Strong ck ([], ini) states)

    | Sdetlocal : forall Hi1 Hi2 bs1 bs2 s,
        sem_scope_det (fun Hi1 Hi2 => Forall (sem_block_det n envS Hi1 Hi2 bs1 bs2)) n envS Hi1 Hi2 s ->
        sem_block_det n envS Hi1 Hi2 bs1 bs2 (Blocal s).

    Ltac inv_branch :=
      match goal with
      | H:sem_branch_det _ _ _ _ _ _ _ _ |- _ => inv H; destruct_conjs; subst
      | H:sem_branch_det' _ _ _ _ _ _ |- _ => inv H; destruct_conjs; subst
      | _ => (Syn.inv_branch || Typ.inv_branch || Sem.inv_branch)
      end.

    Ltac inv_scope :=
      match goal with
      | H:sem_scope_det _ _ _ _ _ _ |- _ => inv H; destruct_conjs; subst
      | _ => (Syn.inv_scope || Typ.inv_scope || Sem.inv_scope)
      end.

    Ltac inv_block :=
      match goal with
      | H:sem_block_det _ _ _ _ _ _ _ |- _ => inv H
      | _ => (Syn.inv_block || Typ.inv_block || Sem.inv_block)
      end.

    Lemma sem_scope_det_0 {A} P_blk1 P_blk2 (P_blk3: _ -> _ -> _ -> Prop) :
      forall locs (blks: A) Hi1 Hi2,
        sem_scope P_blk1 Hi1 (Scope locs blks) ->
        sem_scope P_blk2 Hi2 (Scope locs blks) ->
        (forall Hi1 Hi2, P_blk1 Hi1 blks -> P_blk2 Hi2 blks -> P_blk3 Hi1 Hi2 blks) ->
        sem_scope_det P_blk3 0 [] Hi1 Hi2 (Scope locs blks).

    Lemma sem_branch_det_0 {A} must_def is_def P_blk1 P_blk2 (P_blk3: _ -> Prop) :
      forall caus (blks: A) Hi1 Hi2,
        sem_branch P_blk1 must_def is_def Hi1 (Branch caus blks) ->
        sem_branch P_blk2 must_def is_def Hi2 (Branch caus blks) ->
        (P_blk1 blks -> P_blk2 blks -> P_blk3 blks) ->
        sem_branch_det P_blk3 must_def is_def 0 [] Hi1 Hi2 (Branch caus blks).

    Lemma sem_block_det_0 : forall blk Hi1 Hi2 bs1 bs2,
        sem_block G Hi1 bs1 blk ->
        sem_block G Hi2 bs2 blk ->
        sem_block_det 0 [] Hi1 Hi2 bs1 bs2 blk.

    Lemma det_scope_S {A} P_nd P_wt f_idcaus P_blk1 (P_blk2: _ -> _ -> _ -> Prop) :
      forall Γ n envS locs (blks: A) Hi1 Hi2,
        det_nodes G ->
        NoDupScope P_nd (map fst Γ) (Scope locs blks) ->
        wt_scope P_wt G Γ (Scope locs blks) ->
        (forall cx, det_var_inv Γ (S n) Hi1 Hi2 cx) ->
        incl (map snd (idcaus_of_scope f_idcaus (Scope locs blks))) envS ->
        sem_scope_det P_blk1 n envS Hi1 Hi2 (Scope locs blks) ->
        (forall Γ Hi1 Hi2,
            P_nd (map fst Γ) blks ->
            P_wt Γ blks ->
            (forall cx, det_var_inv Γ (S n) Hi1 Hi2 cx) ->
            incl (map snd (f_idcaus blks)) envS ->
            P_blk1 Hi1 Hi2 blks ->
            P_blk2 Hi1 Hi2 blks) ->
        sem_scope_det P_blk2 (S n) [] Hi1 Hi2 (Scope locs blks).

    Lemma det_branch_S {A} P_nd P_wt f_idcaus P_blk1 (P_blk2: _ -> Prop) must_def is_def :
      forall Γ n envS locs (blks: A) Hi1 Hi2,
        det_nodes G ->
        NoDupBranch P_nd (Branch locs blks) ->
        wt_branch P_wt (Branch locs blks) ->
        (forall cx, det_var_inv Γ (S n) Hi1 Hi2 cx) ->
        incl (map snd (idcaus_of_branch f_idcaus (Branch locs blks))) envS ->
        sem_branch_det P_blk1 must_def is_def n envS Hi1 Hi2 (Branch locs blks) ->
        (P_nd blks ->
         P_wt blks ->
         (forall cx, det_var_inv Γ (S n) Hi1 Hi2 cx) ->
         incl (map snd (f_idcaus blks)) envS ->
         P_blk1 blks ->
         P_blk2 blks) ->
        sem_branch_det P_blk2 must_def is_def (S n) [] Hi1 Hi2 (Branch locs blks).

    Lemma det_block_S : forall n envS blk Γ Hi1 Hi2 bs1 bs2,
        det_nodes G ->
        NoDupLocals (map fst Γ) blk ->
        wt_block G Γ blk ->
        EqStN (S n) bs1 bs2 ->
        (forall cx, det_var_inv Γ (S n) Hi1 Hi2 cx) ->
        incl (map snd (idcaus_of_locals blk)) envS ->
        sem_block_det n envS Hi1 Hi2 bs1 bs2 blk ->
        sem_block_det (S n) [] Hi1 Hi2 bs1 bs2 blk.

    Fact sem_block_det_sem_block1 : forall n envS blk Hi1 Hi2 bs1 bs2,
        sem_block_det n envS Hi1 Hi2 bs1 bs2 blk ->
        sem_block G Hi1 bs1 blk.

    Fact sem_block_det_sem_block2 : forall n envS blk Hi1 Hi2 bs1 bs2,
        sem_block_det n envS Hi1 Hi2 bs1 bs2 blk ->
        sem_block G Hi2 bs2 blk.


    Lemma det_var_inv_incl : forall Γ Γ' n Hi1 Hi2 x,
        incl Γ Γ' ->
        det_var_inv Γ' n Hi1 Hi2 x ->
        det_var_inv Γ n Hi1 Hi2 x.

    Import Permutation.

    Lemma sem_block_det_Perm : forall n xs ys blk Hi1 Hi2 bs1 bs2,
        Permutation xs ys ->
        sem_block_det n xs Hi1 Hi2 bs1 bs2 blk ->
        sem_block_det n ys Hi1 Hi2 bs1 bs2 blk.

    Lemma det_scope_cons {A} f_idcaus P_nd P_wt (P_blk1 P_blk2 : _ -> _ -> _ -> Prop) P_vd P_ld P_def P_dep :
      forall n envS locs (blks: A) Γ xs ls Hi1 Hi2 (bs1 bs2 : Stream bool) cy,
        det_nodes G ->
        NoDupMembers Γ ->
        NoDup (map snd (idcaus_of_senv Γ ++ idcaus_of_scope f_idcaus (Scope locs blks))) ->
        NoDupScope P_nd (map fst Γ) (Scope locs blks) ->
        VarsDefinedCompScope P_vd (Scope locs blks) xs ->
        incl xs (map fst Γ) ->
        LastsDefinedScope P_ld (Scope locs blks) ls ->
        incl ls (map fst Γ) ->
        (forall cx, det_var_inv Γ n Hi1 Hi2 cx) ->
        wt_scope P_wt G Γ (Scope locs blks) ->
        sem_scope_det P_blk1 n envS Hi1 Hi2 (Scope locs blks) ->
        EqStN n bs1 bs2 ->
        (Is_defined_in_scope P_def Γ cy (Scope locs blks) -> EqStN (S n) bs1 bs2) ->
        (forall cx, depends_on_scope P_dep Γ cy cx (Scope locs blks) -> det_var_inv Γ (S n) Hi1 Hi2 cx) ->
        (forall cx, In cx (map snd (idcaus_of_scope f_idcaus (Scope locs blks))) ->
               depends_on_scope P_dep Γ cy cx (Scope locs blks) -> In cx envS) ->
        (forall Γ xs ls Hi1 Hi2,
            NoDupMembers Γ ->
            NoDup (map snd (idcaus_of_senv Γ ++ f_idcaus blks)) ->
            P_nd (map fst Γ) blks ->
            P_vd blks xs ->
            incl xs (map fst Γ) ->
            P_ld blks ls ->
            incl ls (map fst Γ) ->
            (forall cx, det_var_inv Γ n Hi1 Hi2 cx) ->
            P_wt Γ blks ->
            P_blk1 Hi1 Hi2 blks ->
            (P_def Γ blks -> EqStN (S n) bs1 bs2) ->
            (forall cx, P_dep Γ cy cx blks -> det_var_inv Γ (S n) Hi1 Hi2 cx) ->
            (forall cx, In cx (map snd (f_idcaus blks)) ->
                   P_dep Γ cy cx blks -> In cx envS) ->
            (forall y, In y xs -> HasCaus Γ y cy -> det_var (S n) Hi1 Hi2 (Var y))
            /\ (forall y, In y ls -> HasLastCaus Γ y cy -> det_var (S n) Hi1 Hi2 (Last y))
            /\ P_blk2 Hi1 Hi2 blks) ->
        (forall y, In y xs -> HasCaus Γ y cy -> det_var (S n) Hi1 Hi2 (Var y))
        /\ (forall y, In y ls -> HasLastCaus Γ y cy -> det_var (S n) Hi1 Hi2 (Last y))
        /\ sem_scope_det P_blk2 n (cy::envS) Hi1 Hi2 (Scope locs blks).

    Lemma det_branch_cons {A} f_idcaus P_nd P_vd P_ld P_wt (P_blk1 P_blk2 : _ -> Prop) P_dep must_def is_def :
      forall n envS caus (blks: A) Γ xs Hi1 Hi2 cy,
        det_nodes G ->
        NoDupMembers Γ ->
        NoDup (map snd (idcaus_of_senv Γ ++ idcaus_of_branch f_idcaus (Branch caus blks))) ->
        NoDupBranch P_nd (Branch caus blks) ->
        VarsDefinedCompBranch P_vd (Branch caus blks) xs ->
        incl xs (map fst Γ) ->
        LastsDefinedBranch P_ld (Branch caus blks) ->
        (forall cx, det_var_inv Γ n Hi1 Hi2 cx) ->
        wt_branch P_wt (Branch caus blks) ->
        sem_branch_det P_blk1 must_def is_def n envS Hi1 Hi2 (Branch caus blks) ->
        (forall cx, depends_on_branch P_dep Γ cy cx (Branch caus blks) -> det_var_inv Γ (S n) Hi1 Hi2 cx) ->
        (forall cx, In cx (map snd (idcaus_of_branch f_idcaus (Branch caus blks))) ->
               depends_on_branch P_dep Γ cy cx (Branch caus blks) -> In cx envS) ->
        (let Γ := replace_idcaus caus Γ in
         NoDupMembers Γ ->
         NoDup (map snd (idcaus_of_senv Γ ++ f_idcaus blks)) ->
         P_nd blks ->
         P_vd blks xs ->
         incl xs (map fst Γ) ->
         P_ld blks ->
         (forall cx, det_var_inv Γ n Hi1 Hi2 cx) ->
         P_wt blks ->
         P_blk1 blks ->
         (forall cx, P_dep Γ cy cx blks -> det_var_inv Γ (S n) Hi1 Hi2 cx) ->
         (forall cx, In cx (map snd (f_idcaus blks)) ->
                P_dep Γ cy cx blks -> In cx envS) ->
         (forall y, In y xs -> HasCaus Γ y cy -> det_var (S n) Hi1 Hi2 (Var y))
         /\ P_blk2 blks) ->
        (forall y, In y xs -> HasCaus Γ y cy -> det_var (S n) Hi1 Hi2 (Var y))
        /\ sem_branch_det P_blk2 must_def is_def n (cy::envS) Hi1 Hi2 (Branch caus blks).

    Lemma det_block_cons : forall n envS blk Γ xs ls Hi1 Hi2 bs1 bs2 cy,
        det_nodes G ->
        NoDupMembers Γ ->
        NoDup (map snd (idcaus_of_senv Γ ++ idcaus_of_locals blk)) ->
        NoDupLocals (map fst Γ) blk ->
        VarsDefinedComp blk xs ->
        incl xs (map fst Γ) ->
        LastsDefined blk ls ->
        incl ls (map fst Γ) ->
        (forall cx, det_var_inv Γ n Hi1 Hi2 cx) ->
        wt_block G Γ blk ->
        sem_block_det n envS Hi1 Hi2 bs1 bs2 blk ->
        EqStN n bs1 bs2 ->
        (Is_defined_in Γ cy blk -> EqStN (S n) bs1 bs2) ->
        (forall cx, depends_on Γ cy cx blk -> det_var_inv Γ (S n) Hi1 Hi2 cx) ->
        (forall cx, In cx (map snd (idcaus_of_locals blk)) ->
               depends_on Γ cy cx blk -> In cx envS) ->
        (forall y, In y xs -> HasCaus Γ y cy -> det_var (S n) Hi1 Hi2 (Var y))
        /\ (forall y, In y ls -> HasLastCaus Γ y cy -> det_var (S n) Hi1 Hi2 (Last y))
        /\ sem_block_det n (cy::envS) Hi1 Hi2 bs1 bs2 blk.

    Lemma det_vars_n : forall nd n Hi1 Hi2 bs1 bs2,
        det_nodes G ->
        wt_node G nd ->
        node_causal nd ->
        let Γ := senv_of_ins (n_in nd) ++ senv_of_decls (n_out nd) in
        let caus := idcaus (n_in nd) ++ idcaus_of_decls (n_out nd) in
        Forall (fun x => det_var (S n) Hi1 Hi2 (Var x)) (map fst (n_in nd)) ->
        EqStN (S n) bs1 bs2 ->
        (forall x, det_var_inv Γ n Hi1 Hi2 x) ->
        sem_block_det n [] Hi1 Hi2 bs1 bs2 (n_block nd) ->
        Forall (fun x => det_var_inv Γ (S n) Hi1 Hi2 x) (map snd (caus ++ idcaus_of_locals (n_block nd)))
        /\ sem_block_det n (map snd (caus ++ idcaus_of_locals (n_block nd))) Hi1 Hi2 bs1 bs2 (n_block nd).

    Lemma det_vars :
      forall nd n Hi1 Hi2 bs1 bs2,
        det_nodes G ->
        wt_node G nd ->
        node_causal nd ->
        EqStN n bs1 bs2 ->
        sem_block G Hi1 bs1 (n_block nd) ->
        sem_block G Hi2 bs2 (n_block nd) ->
        Forall (fun x => det_var n Hi1 Hi2 (Var x)) (map fst (n_in nd)) ->
        Forall (det_var_inv (senv_of_ins (n_in nd) ++ senv_of_decls (n_out nd)) n Hi1 Hi2) (map snd (idcaus (n_in nd) ++ idcaus_of_decls (n_out nd))).

  End sem_block_det.


  Lemma det_global_n {prefs} : forall (G : @global complete prefs),
      wt_global G ->
      Forall node_causal (nodes G) ->
      det_nodes G.

  Theorem det_global {prefs} : forall (G: @global complete prefs) f ins outs1 outs2,
      wt_global G ->
      Forall node_causal (nodes G) ->
      sem_node G f ins outs1 ->
      sem_node G f ins outs2 ->
      EqSts outs1 outs2.

End LSEMDETERMINISM.

Module LSemDeterminismFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Cks : CLOCKS Ids Op OpAux)
       (Senv : STATICENV Ids Op OpAux Cks)
       (Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Typ : LTYPING Ids Op OpAux Cks Senv Syn)
       (LCA : LCAUSALITY Ids Op OpAux Cks Senv Syn)
       (Lord : LORDERED Ids Op OpAux Cks Senv Syn)
       (CStr : COINDSTREAMS Ids Op OpAux Cks)
       (Sem : LSEMANTICS Ids Op OpAux Cks Senv Syn Lord CStr)
<: LSEMDETERMINISM Ids Op OpAux Cks Senv Syn Typ LCA Lord CStr Sem.
  Include LSEMDETERMINISM Ids Op OpAux Cks Senv Syn Typ LCA Lord CStr Sem.
End LSemDeterminismFun.