Module GlobSim

Require Import Values.

Require Import Blockset Footprint GMemory InteractionSemantics GAST
        GlobDefs ETrace NPSemantics
        Injections GSimDefs GlobDSim GlobUSim NPSemantics GDefLemmas NPDet.

Require Import Arith Wf Classical_Prop FunctionalExtensionality.
Module GlobSim.

  Notation "{ A , B , C , D } " := {|thread_pool:=A;cur_tid:=B;gm:=C;atom_bit:=D|} (at level 70,right associativity).
  Notation "{'FP'| A , B , C , D } " := {|FP.cmps:=A;FP.reads:=B;FP.writes:=C;FP.frees:=D|} (at level 70,right associativity).
  Local Notation "{-| PC , T }" :=
  ({|thread_pool := thread_pool PC; cur_tid := T;gm := gm PC; atom_bit := atom_bit PC |}) (at level 70,right associativity).
  Ltac clearfp:=
    repeat rewrite FP.fp_union_emp in *;
    repeat rewrite FP.emp_union_fp in *;
    repeat rewrite FP.fp_union_assoc in *.

  Definition inv {ge}(pc:@ProgConfig ge):= ThreadPool.inv pc.(thread_pool).
  Lemma init_config_inv_thp:
    forall NL L p gm ge pc t,
      @init_config NL L p gm ge pc t->
      inv pc.
  Lemma thp_inv_preservation:
    forall ge pc o fp pc',
      GlobEnv.wd ge ->
      @np_step ge pc o fp pc' ->
      inv pc ->
      inv pc'.
  Lemma thp_inv_tau_star_preservation:
    forall ge pc fp pc',
      GlobEnv.wd ge ->
      tau_star (@np_step ge) pc fp pc' ->
      inv pc ->
      inv pc'.
  Lemma thrddom_eq'_thrd_valid_tid_preservation {sge tge}:
    forall spc tpc,
      @inv sge spc -> @inv tge tpc -> thrddom_eq' spc tpc ->
      forall id, ThreadPool.valid_tid spc.(thread_pool) id ->
            ThreadPool.valid_tid tpc.(thread_pool) id.
  Lemma thrddom_eq'_final_state_preservation {sge tge}:
    forall spc tpc,
      @inv sge spc -> @inv tge tpc -> thrddom_eq' spc tpc ->
      final_state tpc ->final_state spc.
  Lemma thrddom_eq'_valid_tid_preservation{sge tge}:
    forall spc tpc,
      inv spc -> inv tpc -> thrddom_eq' spc tpc ->
      forall id, @pc_valid_tid sge spc id ->
            @pc_valid_tid tge tpc id.

  Section Lemmas.
    Lemma sw_step_det{ge}:
      forall pc pc1 o fp pc2 fp2,
        @np_step ge pc o fp pc1 ->
        np_step pc o fp2 pc2 ->
        o<> tau ->
        fp = FP.emp /\ fp2 = FP.emp /\
        pc1.(thread_pool) = pc2.(thread_pool) /\
        pc1.(gm) = pc2.(gm) /\
        pc1.(atom_bit) = pc2.(atom_bit).
    Lemma switch_any : forall(ges:GlobEnv.t) (spc spc1:@ProgConfig ges)o fpS ,
        np_step spc o fpS spc1 ->
        o <> tau ->
        forall t,
          pc_valid_tid spc1 t->
          np_step spc o fpS ({-|spc1,t}).
    Definition language_det (ge:GlobEnv.t): Prop := @NPDet.language_det ge.
    Lemma np_step_det: forall(ge:GlobEnv.t)(pc pc' pc'':@ProgConfig ge) fp fp' l1 l2,
        language_det ge->
        np_step pc l1 fp pc' -> np_step pc l2 fp' pc'' ->
        l1 = l2 /\ fp = fp' /\
        pc'.(thread_pool) = pc''.(thread_pool) /\
        pc'.(gm) = pc''.(gm) /\
        pc'.(atom_bit) = pc''.(atom_bit) /\
        (l1=tau->pc'.(cur_tid)=pc''.(cur_tid)).
    Lemma tau_step_det: forall(ge:GlobEnv.t)(pc pc' pc'':@ProgConfig ge) fp fp' l,
        language_det ge->
        np_step pc tau fp pc' -> np_step pc l fp' pc'' ->
        l = tau /\ fp = fp' /\ pc'=pc''.

    Lemma tau_step_bit_rule:
      forall (ge:GlobEnv.t)(pc pc':@ProgConfig ge) fp label,
        np_step pc label fp pc' ->
        label = tau ->
        (atom_bit pc = O /\ atom_bit pc' = O) \/
        (atom_bit pc = O /\ atom_bit pc' = I) \/
        (atom_bit pc = I /\ atom_bit pc' = I).
    Corollary EntAx_bit_rule:
      forall (ge:GlobEnv.t)(pc pc':@ProgConfig ge) fp,
        np_step pc tau fp pc' ->
        atom_bit pc <> atom_bit pc' ->
        (atom_bit pc = O /\ atom_bit pc' = I).
    Corollary tau_step_bit_backwards_preservation :
       forall (ge:GlobEnv.t)(pc pc':@ProgConfig ge) fp label,
         np_step pc label fp pc' -> label=tau ->atom_bit pc' = O -> atom_bit pc' = O.
    Corollary tau_step_bit_I_preservation :
       forall (ge:GlobEnv.t)(pc pc':@ProgConfig ge) fp label,
         np_step pc label fp pc' -> label=tau ->atom_bit pc = I -> atom_bit pc' = I.
    Lemma tau_N_bit_rule:
      forall i (ge:GlobEnv.t)(pc pc':@ProgConfig ge) fp,
        tau_N np_step i pc fp pc'->
        (atom_bit pc = O /\ atom_bit pc' = O) \/
        (atom_bit pc = O /\ atom_bit pc' = I) \/
        (atom_bit pc = I /\ atom_bit pc' = I).
    Lemma tau_N_tau_step_bit_rule:
      forall i (ge:GlobEnv.t)(pc pc' pce:@ProgConfig ge) fp1 fp2,
        np_step pc tau fp1 pc' ->
        tau_N np_step i pc' fp2 pce ->
        atom_bit pc = atom_bit pce ->
        atom_bit pc = atom_bit pc'.
    Lemma tau_N_bit_backwards_preservation:
       forall i (ge:GlobEnv.t)(pc pc':@ProgConfig ge) fp,
        tau_N np_step i pc fp pc'->
        atom_bit pc' = O ->
        atom_bit pc = O.
    Lemma tau_N_bit_I_preservation:
      forall i (ge:GlobEnv.t)(pc pc':@ProgConfig ge) fp,
        tau_N np_step i pc fp pc'->
        atom_bit pc = I ->
        atom_bit pc' = I.
    Lemma inv_thdp_gettop_valid_tid:
    forall ge pc c,
      ThreadPool.inv pc.(thread_pool) ->
      ThreadPool.get_top pc.(thread_pool) pc.(cur_tid) = Some c->
      @pc_valid_tid ge pc pc.(cur_tid).
    Lemma inv_step_valid_tid:
      forall ge pc fp pc1 o,
        (@np_step ge) pc o fp pc1->
        ThreadPool.inv pc.(thread_pool) ->
        pc_valid_tid pc pc.(cur_tid).
    Lemma step_no_final:forall ge pc pc1 fp o,
        @np_step ge pc o fp pc1 ->
        inv pc ->
        ~final_state pc.

    Lemma safe_rule: forall(ge:GlobEnv.t) (pc:@ProgConfig ge),
      ~ np_abort pc -> final_state pc \/(exists gl fp pc',np_step pc gl fp pc').
    Lemma safe_succession: forall sge (spc:@ProgConfig sge) (spc':@ProgConfig sge) (fpS:FP.t),
        tau_star np_step spc fpS spc' ->
        np_safe_config spc ->
        np_safe_config spc'.
    Lemma tau_step_tid_preservation:forall(ge:GlobEnv.t)(pc pc':@ProgConfig ge)(fp:FP.t),
        np_step pc tau fp pc' ->
        cur_tid pc = cur_tid pc'.
    Lemma tau_star_tid_preservation: forall(ge:GlobEnv.t)(pc pc':@ProgConfig ge)(fp:FP.t),
        tau_star np_step pc fp pc' ->
        cur_tid pc = cur_tid pc'.
    Corollary tau_star_tideq_preservation :forall (ges get:GlobEnv.t)(spc spc1:@ProgConfig ges)(tpc tpc1:@ProgConfig get)(fpS fpT:FP.t),
        tau_star np_step spc fpS spc1 ->
        tau_star np_step tpc fpT tpc1 ->
        ( tid_eq spc tpc <-> tid_eq spc1 tpc1).
    Lemma cs_match_comm: forall G1 G2 A B,
        @cs_match' G1 G2 A B -> cs_match' B A.
    Lemma ocs_match_comm : forall G1 G2 A B,
        @ocs_match' G1 G2 A B -> ocs_match' B A.
    Lemma thrddom_eq_comm: forall sge tge (spc:@ProgConfig sge)(tpc:@ProgConfig tge),
        thrddom_eq' spc tpc -> thrddom_eq' tpc spc.

    Lemma scs_upd_cs_match':
      forall SGE TGE (scs: @CallStack.t SGE) (tcs: @CallStack.t TGE),
        cs_match' scs tcs ->
        forall c' scs',
          CallStack.update scs c' scs' ->
          cs_match' scs' tcs.
    Lemma stp_upd_ocs_match':
      forall SGE TGE (sthdp: @ThreadPool.t SGE) (tthdp:@ThreadPool.t TGE) i,
        ocs_match' (ThreadPool.get_cs sthdp i) (ThreadPool.get_cs tthdp i) ->
        (forall i' c' sthdp',
            ThreadPool.update sthdp i' c' sthdp' ->
            ocs_match' (ThreadPool.get_cs sthdp' i) (ThreadPool.get_cs tthdp i)).
    Lemma tcs_upd_cs_match:
      forall SGE TGE (scs: @CallStack.t SGE) (tcs: @CallStack.t TGE),
        cs_match' scs tcs ->
        forall c' tcs',
          CallStack.update tcs c' tcs' ->
          cs_match' scs tcs'.
    Lemma ttp_upd_ocs_match':
      forall SGE TGE (sthdp: @ThreadPool.t SGE) (tthdp:@ThreadPool.t TGE) i,
        ocs_match' (ThreadPool.get_cs sthdp i) (ThreadPool.get_cs tthdp i) ->
        (forall i' c' tthdp',
            ThreadPool.update tthdp i' c' tthdp' ->
            ocs_match' (ThreadPool.get_cs sthdp i) (ThreadPool.get_cs tthdp' i)).
    Lemma call_ocs_match':
      forall SGE TGE sthdp thdp i,
        @ocs_match' SGE TGE (ThreadPool.get_cs sthdp i)(ThreadPool.get_cs thdp i) ->
        forall t c funid sg args new_ix cc' thdp',
          let: cc := Core.c c in
          let: c_ix := Core.i c in
          let: c_mod := GlobEnv.modules TGE c_ix in
          let: c_lang := ModSem.lang c_mod in
          let: Ge := ModSem.Ge c_mod in
          forall
            (H_tp_core: ThreadPool.get_top thdp t = Some c)
            (H_core_atext: at_external c_lang Ge cc = Some (funid, sg, args))
            (H_mod_id: GlobEnv.get_mod TGE funid = Some new_ix),
            let: new_mod := GlobEnv.modules TGE new_ix in
            let: new_lang := ModSem.lang new_mod in
            let: new_Ge := ModSem.Ge new_mod in
            forall
              (H_new_core: init_core new_lang new_Ge funid args = Some cc')
              (H_tp_push: ThreadPool.push thdp t new_ix cc' sg = Some thdp'),
              ocs_match' (ThreadPool.get_cs sthdp i)(ThreadPool.get_cs thdp' i).
    Lemma return_ocs_match':
      forall SGE GE sthdp thdp i,
        @ocs_match' SGE GE (ThreadPool.get_cs sthdp i)(ThreadPool.get_cs thdp i) ->
        forall t c res thdp' c' cc'' c'' thdp'',
          let: cc := Core.c c in
          let: c_ix := Core.i c in
          let: c_sg := Core.sg c in
          let: c_mod := GlobEnv.modules GE c_ix in
          let: c_lang := ModSem.lang c_mod in
          let: Ge := ModSem.Ge c_mod in
          forall
            (H_tp_core: ThreadPool.get_top thdp t = Some c)
            (H_core_halt: halt c_lang cc = Some res)
            (H_tp_pop: ThreadPool.pop thdp t = Some thdp')
            (H_tp_caller: ThreadPool.get_top thdp' t = Some c'),
            let: cc' := Core.c c' in
            let: c'_ix := Core.i c' in
            let: c'_mod := GlobEnv.modules GE c'_ix in
            let: c'_lang := ModSem.lang c'_mod in
            let: Ge' := ModSem.Ge c'_mod in
            forall
              (H_core_aftext: after_external c'_lang cc' (res_sg c_sg res) = Some cc'')
              (H_core_upd: Core.update c' cc'' c'')
              (H_tp_upd: ThreadPool.update thdp' t c'' thdp''),
              @ocs_match' SGE GE (ThreadPool.get_cs sthdp i)(ThreadPool.get_cs thdp'' i).
    Definition final_pool {ge}(thdp:ThreadPool.t):=
      forall i, @ThreadPool.valid_tid ge thdp i -> ThreadPool.halted thdp i.
    Lemma final_state_rule1:
      forall ge p1 t c p2,
        @final_pool ge p2->
        ThreadPool.update p1 t c p2 ->
        final_pool p1.

    Lemma final_state_rule2:
      forall ge p t ix cc sg p',
        @final_pool ge p'->
        ThreadPool.push p t ix cc sg = Some p' ->
        final_pool p.

    Lemma final_state_rule3:
      forall ge p t p' c p'',
        @final_pool ge p''->
        ThreadPool.pop p t = Some p' ->
        ThreadPool.update p' t c p'' ->
        final_pool p.

    Lemma tau_step_thrddom_eq_preservation: forall sge tge (spc:@ProgConfig sge) tpc tpc1 fp,
        @np_step tge tpc tau fp tpc1 -> ~final_state tpc1 ->
        thrddom_eq' spc tpc ->
        thrddom_eq' spc tpc1.

    Corollary final_pool_final_state_equiv :
      forall ge pc,
        @final_state ge pc <-> final_pool pc.(thread_pool).

    Lemma halt_step_thrddom_eq_preservation: forall sge tge spc spc1 tpc tpc1 fp1 fp2,
        @np_step sge spc tau fp1 spc1 -> final_state spc1 -> inv spc ->
        @np_step tge tpc tau fp2 tpc1 -> final_state tpc1 -> inv tpc ->
        spc.(cur_tid) = tpc.(cur_tid) ->
        thrddom_eq' spc tpc ->
        thrddom_eq' spc1 tpc1.

    Lemma tau_star_thrddom_eq_preservation: forall sge tge (spc:@ProgConfig sge) tpc tpc1 fp,
        GlobEnv.wd tge -> inv tpc ->
        tau_star (@np_step tge) tpc fp tpc1 -> ~ final_state tpc1 ->
        thrddom_eq' spc tpc ->
        thrddom_eq' spc tpc1.
    Lemma tau_star_finalstate_thrddom_eq_preservation : forall sge tge spc tpc spc1 tpc1 fp1 fp2,
        cur_tid spc = cur_tid tpc ->
        GlobEnv.wd sge -> GlobEnv.wd tge ->
        tau_star (@np_step sge) spc fp1 spc1 ->
        tau_star (@np_step tge) tpc fp2 tpc1 ->
        inv spc -> inv tpc ->
        final_state spc1 -> final_state tpc1 ->
        thrddom_eq' spc tpc -> thrddom_eq' spc1 tpc1.
    Definition valid_tid {ge}(pc:@ProgConfig ge)(t:tid) :Prop:=
      ThreadPool.valid_tid pc.(thread_pool) t /\ ~ThreadPool.halted pc.(thread_pool) t .
    Lemma match_tp_one' : forall sge tge(spc:@ProgConfig sge)( tpc:@ProgConfig tge) (t:tid),
        inv spc -> inv tpc ->thrddom_eq' spc tpc -> valid_tid spc t -> valid_tid tpc t.
    Lemma match_tp_ano' :forall sge tge(spc:@ProgConfig sge)( tpc:@ProgConfig tge) (t:tid),
        inv spc -> inv tpc -> thrddom_eq' spc tpc -> valid_tid tpc t -> valid_tid spc t.
    Lemma non_tau_step_tid_rule: forall ge pc pc1 o fp,
        @np_step ge pc o fp pc1 -> o <> tau ->
        valid_tid pc1 pc1.(cur_tid).
  End Lemmas.
  Section Simulation.
    Definition Sim_tau_step_case (sge tge:GlobEnv.t)(match_state:Mu->FP.t -> FP.t -> @ProgConfig sge -> @ProgConfig tge -> Prop) (mu:Mu)(fpS fpT:FP.t)(spc tpc:ProgConfig):Prop:=
        exists fpS1 fpT1 spc1 tpc1,
          tau_plus np_step spc fpS1 spc1 /\ tau_plus np_step tpc fpT1 tpc1 /\
          atom_bit spc = atom_bit spc1 /\
          LFPG mu tge tpc.(cur_tid) (FP.union fpS fpS1) (FP.union fpT fpT1) /\
          match_state mu (FP.union fpS fpS1)(FP.union fpT fpT1) spc1 tpc1.
    Definition Sim_EntAtom_case (sge tge:GlobEnv.t)(match_state:Mu->FP.t -> FP.t -> @ProgConfig sge -> @ProgConfig tge -> Prop) (mu:Mu)(fpS fpT:FP.t)(spc tpc:ProgConfig):Prop:=
        exists fpS' fpT' fpS'' fpT'' spc' tpc' spc'' tpc'',
          tau_star np_step spc fpS' spc' /\ np_step spc' tau fpS'' spc'' /\
          tau_star np_step tpc fpT' tpc' /\ np_step tpc' tau fpT'' tpc'' /\
          atom_bit spc' <> atom_bit spc'' /\ atom_bit spc = atom_bit spc' /\
          atom_bit tpc' <> atom_bit tpc'' /\ atom_bit tpc = atom_bit tpc' /\
          LFPG mu tge tpc.(cur_tid) (FP.union fpS (FP.union fpS' fpS'')) (FP.union fpT (FP.union fpT' fpT'')) /\
          match_state mu FP.emp FP.emp spc'' tpc''.
    Definition Sim_final_case (sge tge:GlobEnv.t)(match_state:Mu->FP.t -> FP.t -> @ProgConfig sge -> @ProgConfig tge -> Prop) (mu:Mu)(fpS fpT:FP.t)(spc:@ProgConfig sge)( tpc:@ProgConfig tge):Prop:=
        exists fpS' fpT' spc' tpc',
                tau_star np_step spc fpS' spc' /\ final_state spc' /\
                tau_star np_step tpc fpT' tpc' /\ final_state tpc' /\
                atom_bit spc = atom_bit spc' /\ atom_bit tpc = atom_bit tpc' /\
                LFPG mu tge tpc.(cur_tid) (FP.union fpS fpS') (FP.union fpT fpT').
    
    Definition Sim_npsw_case (sge tge:GlobEnv.t)(match_state:Mu->FP.t -> FP.t -> @ProgConfig sge -> @ProgConfig tge -> Prop) (mu:Mu)(fpS fpT:FP.t)(spc tpc:ProgConfig):Prop:=
      exists spc' fpS' tpc' fpT',
        tau_star np_step spc fpS' spc' /\ atom_bit spc = atom_bit spc' /\
        tau_star np_step tpc fpT' tpc' /\ atom_bit tpc = atom_bit tpc' /\
        exists o t spc'' tpc'',
            valid_tid spc'' t /\
          forall id, valid_tid spc'' id ->
                 o <> tau /\
                 match_state mu FP.emp FP.emp ({-|spc'',id})({-|tpc'',id}) /\
                 np_step spc' o FP.emp ({-|spc'',id})/\
                 np_step tpc' o FP.emp ({-|tpc'',id})/\
                 LFPG mu tge tpc.(cur_tid) (FP.union fpS fpS') (FP.union fpT fpT').
    Record GSim
           {sge tge:GlobEnv.t}
           (match_state:Mu->FP.t -> FP.t ->
                        @ProgConfig sge -> @ProgConfig tge -> Prop)
    : Prop :=
      {
        match_tp:
          forall mu fpS fpT spc tpc ,
            match_state mu fpS fpT spc tpc->
            Bset.inj_inject (inj mu) /\ GlobEnv.wd tge /\ GlobEnv.wd sge /\
            np_safe_config spc /\
            language_det tge /\
            inv spc /\ inv tpc /\thrddom_eq' spc tpc /\
            atombit_eq spc tpc /\
            tid_eq spc tpc;

        match_step:
          forall mu fpS fpT spc tpc,
            match_state mu fpS fpT spc tpc ->
            Sim_final_case sge tge match_state mu fpS fpT spc tpc \/
            Sim_npsw_case sge tge match_state mu fpS fpT spc tpc \/
            Sim_tau_step_case sge tge match_state mu fpS fpT spc tpc\/
            Sim_EntAtom_case sge tge match_state mu fpS fpT spc tpc
      }.

    Definition d2s_match{sge tge}(mu:Mu)(fpS fpT:FP.t)(spc:@ProgConfig sge)(tpc:@ProgConfig tge):Prop:=
      exists I order i match_state,
        @GConfigDSim sge tge I order match_state /\
        match_state i mu fpS fpT spc tpc /\
        np_safe_config spc /\ language_det tge /\
        inv spc /\ inv tpc /\ GlobEnv.wd tge/\ GlobEnv.wd sge.

    Lemma GSim_d2s_match{sge tge}:
      @GSim sge tge d2s_match.
  End Simulation.
  Section GlobIndexSim.
    Definition ISim_tau_step_case (sge tge:GlobEnv.t)(match_state:nat->Mu->FP.t -> FP.t -> @ProgConfig sge -> @ProgConfig tge -> Prop)(i:nat) (mu:Mu)(fpS fpT:FP.t)(spc tpc:ProgConfig):Prop:=
        exists fpS1 fpT1 spc1 tpc1 j,
          tau_plus np_step spc fpS1 spc1 /\ tau_N np_step (S i) tpc fpT1 tpc1 /\
          atom_bit spc = atom_bit spc1 /\
          LFPG mu tge tpc.(cur_tid) (FP.union fpS fpS1) (FP.union fpT fpT1) /\
          match_state j mu (FP.union fpS fpS1)(FP.union fpT fpT1) spc1 tpc1.
    Definition ISim_EntAtom_case (sge tge:GlobEnv.t)(match_state:nat->Mu->FP.t -> FP.t -> @ProgConfig sge -> @ProgConfig tge -> Prop)(i:nat) (mu:Mu)(fpS fpT:FP.t)(spc tpc:ProgConfig):Prop:=
        exists fpS' fpT' fpS'' fpT'' spc' tpc' spc'' tpc'' j,
          tau_star np_step spc fpS' spc' /\ np_step spc' tau fpS'' spc'' /\
          tau_N np_step i tpc fpT' tpc' /\ np_step tpc' tau fpT'' tpc'' /\
          atom_bit spc' <> atom_bit spc'' /\ atom_bit spc = atom_bit spc' /\
          atom_bit tpc' <> atom_bit tpc'' /\ atom_bit tpc = atom_bit tpc' /\
          LFPG mu tge tpc.(cur_tid) (FP.union fpS (FP.union fpS' fpS'')) (FP.union fpT (FP.union fpT' fpT'')) /\
          match_state j mu FP.emp FP.emp spc'' tpc''.
    Definition ISim_final_case (sge tge:GlobEnv.t)(match_state:nat->Mu->FP.t -> FP.t -> @ProgConfig sge -> @ProgConfig tge -> Prop) (i:nat)(mu:Mu)(fpS fpT:FP.t)(spc:@ProgConfig sge)( tpc:@ProgConfig tge):Prop:=
        exists fpS' fpT' spc' tpc',
                tau_star np_step spc fpS' spc' /\ final_state spc' /\
                tau_N np_step i tpc fpT' tpc' /\ final_state tpc' /\
                atom_bit spc = atom_bit spc' /\ atom_bit tpc = atom_bit tpc' /\
                LFPG mu tge tpc.(cur_tid) (FP.union fpS fpS') (FP.union fpT fpT').
    
    Definition ISim_npsw_case (sge tge:GlobEnv.t)(match_state:nat->Mu->FP.t -> FP.t -> @ProgConfig sge -> @ProgConfig tge -> Prop)(i:nat) (mu:Mu)(fpS fpT:FP.t)(spc tpc:ProgConfig):Prop:=
      exists spc' fpS' tpc' fpT',
        tau_star np_step spc fpS' spc' /\ atom_bit spc = atom_bit spc' /\
        tau_N np_step i tpc fpT' tpc' /\ atom_bit tpc = atom_bit tpc' /\
        exists o t spc'' tpc'',
          valid_tid spc'' t/\
          forall id, valid_tid spc'' id ->
                 o <> tau /\
                 exists j,match_state j mu FP.emp FP.emp ({-|spc'',id})({-|tpc'',id}) /\
                 np_step spc' o FP.emp ({-|spc'',id})/\
                 np_step tpc' o FP.emp ({-|tpc'',id})/\
                 LFPG mu tge tpc.(cur_tid) (FP.union fpS fpS') (FP.union fpT fpT').
    Definition d2s_match_index {sge tge}(i:nat):= @d2s_match sge tge.
      
    Record index_match {sge tge} (i:nat)(mu:Mu)(fpS fpT:FP.t)(spc:@ProgConfig sge)(tpc:@ProgConfig tge):Prop:=
      {
        match_tp':
           Bset.inj_inject (inj mu) /\ GlobEnv.wd tge /\ GlobEnv.wd sge /\
           np_safe_config spc /\
           language_det tge /\
           inv spc /\ inv tpc /\thrddom_eq' spc tpc /\
           atombit_eq spc tpc /\
           tid_eq spc tpc;
        match_step':
          ISim_final_case sge tge d2s_match_index i mu fpS fpT spc tpc \/
          ISim_npsw_case sge tge d2s_match_index i mu fpS fpT spc tpc \/
          ISim_tau_step_case sge tge d2s_match_index i mu fpS fpT spc tpc \/
          ISim_EntAtom_case sge tge d2s_match_index i mu fpS fpT spc tpc
      }.

 
    Lemma d2s_match_index_exists :
      forall (sge tge:GlobEnv.t)(spc:@ProgConfig sge)(tpc:@ProgConfig tge) fpS fpT mu,
        d2s_match mu fpS fpT spc tpc ->
        exists i, index_match i mu fpS fpT spc tpc.


    Lemma GUSim_index_match{sge tge}:
      @GConfigUSim sge tge nat lt index_match.
  End GlobIndexSim.
  Section Flip.
    Lemma Language_Det: forall NL (L:@langs NL)(tp:prog L),
      det_langs (fst tp) ->
      wd_langs (fst tp) ->
      forall gm ge pc t,
        init_config tp gm ge pc t->
        language_det ge.
    Lemma flipping':
      forall NL (L: @langs NL) (sprog tprog: prog L),
        GlobDSim sprog tprog ->
        det_langs (fst tprog) ->
        wd_langs (fst tprog) ->
        np_safe_prog sprog ->
        GlobUSim sprog tprog.
  End Flip.
End GlobSim.