Module SmileReorder

Require Import Footprint InteractionSemantics GAST GMemory
        GlobDefs ETrace GlobSemantics GlobSemantics_Lemmas NPSemantics TypedSemantics .

Require Import DRF USimDRF NPDRF FPLemmas PRaceLemmas.

Require Import Classical Wf Arith.
Local Notation "'<<' i ',' c ',' sg ',' F '>>'" := {|Core.i := i; Core.c := c; Core.sg := sg; Core.F := F|} (at level 60, right associativity).
Local Definition pc_valid_tid {ge}:= @GSimDefs.pc_valid_tid ge.
Local Notation "{ A , B , C , D }" := {|thread_pool:=A;cur_tid:=B;gm:=C;atom_bit:= 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 Hsimpl:=
  repeat match goal with
         | H1:?a,H2:?a->?b|-_=>specialize (H2 H1)
         | H:_/\_|-_=> destruct H
         | H:exists _,_|-_=>destruct H
         end.
Ltac Esimpl:=
  repeat match goal with
         | H:_|-_/\_=>split
         | H:_|-exists _,_=>eexists
         end.
Ltac clear_get:=
  repeat (rewrite Maps.PMap.gsspec in *;(destruct Coqlib.peq;subst;try contradiction; simpl in *; subst)).
Ltac clear_set:=
  repeat (rewrite Maps.PMap.set2 in *;(destruct Coqlib.peq;subst;try contradiction; simpl in *; subst)).
Ltac solv_thread:=
  repeat
    match goal with
    | H:ThreadPool.update _ _ _ _ |- _ => Coqlib.inv H
    | H:CallStack.update _ _ _ |- _ => Coqlib.inv H
    | H:ThreadPool.halted _ _ |- _ => Coqlib.inv H
    end;
  unfold ThreadPool.get_top, ThreadPool.pop, ThreadPool.get_cs, ThreadPool.push,ThreadPool.valid_tid ,
  CallStack.pop, CallStack.top, CallStack.is_emp, CallStack.emp_cs in *; simpl in *; subst;
  repeat (rewrite Maps.PMap.gsspec in *;(destruct Coqlib.peq;subst;try contradiction; simpl in *; subst));
  repeat
  match goal with
    H: context[match ?x with _ => _ end] |- _ => destruct x eqn:?; try (inversion H; fail)
  | H: Some _ = Some _ |- _ => inversion H; clear H; subst
  | H:?P = ?Q, H1:context [ ?P ] |- _ => rewrite H in H1
  | H:?P = ?Q |- context [ ?P ] => rewrite H
  end;
  simpl in *;
  GDefLemmas.solv_eq; eauto;
  clear_set;simpl in *.
Ltac solv_thread_alt:=
  repeat
    match goal with
    | H:ThreadPool.update _ _ _ _ |- _ => Coqlib.inv H
    | H:CallStack.update _ _ _ |- _ => Coqlib.inv H
    | H:ThreadPool.halted _ _ |- _ => Coqlib.inv H
    end;
  unfold ThreadPool.get_top, ThreadPool.pop, ThreadPool.get_cs, ThreadPool.push,ThreadPool.valid_tid ,
  CallStack.pop, CallStack.top, CallStack.is_emp, CallStack.emp_cs in *; subst;
  repeat (rewrite Maps.PMap.gsspec in *;(destruct Coqlib.peq;subst;try contradiction; subst));
  repeat
  match goal with
    H: context[match ?x with _ => _ end] |- _ => destruct x eqn:?; try (inversion H; fail)
  | H: Some _ = Some _ |- _ => inversion H; clear H; subst
  | H:?P = ?Q, H1:context [ ?P ] |- _ => rewrite H in H1
  | H:?P = ?Q |- context [ ?P ] => rewrite H
  end.

Section Reorder.
  Variable GE:GlobEnv.t.
  Hypothesis wdge:forall ix,mod_wd (GlobEnv.modules GE ix).
  Definition changepc (pc:@ProgConfig GE)(t:tid)(b:Bit):ProgConfig:=
    { pc.(thread_pool), t,pc.(gm),b}.
  Definition mem_eq_pc (pc pc':@ProgConfig GE):Prop:=
    thread_pool pc = thread_pool pc' /\
    atom_bit pc = atom_bit pc' /\
    cur_tid pc = cur_tid pc' /\
    GMem.eq' (gm pc)(gm pc').
  Lemma mem_eq_pc_refl:forall p,mem_eq_pc p p.
  Lemma mem_eq_pc_sym:forall p p',mem_eq_pc p p'->mem_eq_pc p' p.
  Lemma mem_eq_pc_trans:forall p1 p2 p3,mem_eq_pc p1 p2 ->mem_eq_pc p2 p3->mem_eq_pc p1 p3.


  Lemma Memperm_validblock:
    forall m b ofs k p,
      GMemory.GMem.perm m b ofs k p ->
      GMemory.GMem.valid_block m b.

  Lemma localstep_memeff:
    forall i_x F cc m fp cc' m',
      step (ModSem.lang (GlobEnv.modules GE i_x)) (ModSem.Ge (GlobEnv.modules GE i_x)) (FLists.get_fl (GlobEnv.freelists GE) F) cc m fp cc' m' ->
      LEffect m m' fp (FLists.get_fl (GlobEnv.freelists GE) F).
  Function getcurcore (pc:@ProgConfig GE):= ThreadPool.get_top pc.(thread_pool) pc.(cur_tid).
  Function getfl (c:@Core.t GE) := FLists.get_fl (GlobEnv.freelists GE) (Core.F c).
  Function getcurcs (pc:@ProgConfig GE):= ThreadPool.get_cs pc.(thread_pool) pc.(cur_tid).

  Lemma gettop_getcs_exists:
    forall thdp i c,
      @ThreadPool.get_top GE thdp i = Some c ->
      exists c',ThreadPool.get_cs thdp i = Some c'.
  Lemma gettop_push_exists:
    forall thdp i c,@ThreadPool.get_top GE thdp i = Some c->
               forall mid c sg, exists c',ThreadPool.push thdp i mid c sg = Some c'.
  Lemma coreupdate_exists:
    forall c cc,exists c', @Core.update GE c cc c'.
  Lemma gettop_update_exists:
    forall thdp i c,@ThreadPool.get_top GE thdp i = Some c->
               forall cc c', Core.update c cc c' ->exists thdp', ThreadPool.update thdp i c' thdp'.
  Lemma gettop_pop_exists:
    forall thdp i c,@ThreadPool.get_top GE thdp i = Some c->
               exists t,ThreadPool.pop thdp i = Some t.
  Lemma update_gettop_exists:
    forall thdp i c thdp',@ThreadPool.update GE thdp i c thdp'->
                     exists c,ThreadPool.get_top thdp i = Some c.
  Lemma pop_gettop_exists:
    forall thdp i thdp',@ThreadPool.pop GE thdp i = Some thdp'->
                   exists c,ThreadPool.get_top thdp i= Some c.
  Lemma gettop_preserve:
    forall t1 t2, t1<>t2->
             forall thdp1 c,
               @ThreadPool.get_top GE thdp1 t1 = Some c->
               forall thdp2,
                 (exists c',@ThreadPool.update GE thdp1 t2 c' thdp2) \/
                 (ThreadPool.pop thdp1 t2 = Some thdp2)\/
                 (exists mid c' sg,ThreadPool.push thdp1 t2 mid c' sg = Some thdp2)
               ->
               ThreadPool.get_top thdp2 t1 = Some c.

    
  Lemma gettop_backwards_preserve:
    forall t1 t2, t1<>t2->
             forall thdp2 c,
               @ThreadPool.get_top GE thdp2 t1 = Some c->
               forall thdp1,
                 (exists c',@ThreadPool.update GE thdp1 t2 c' thdp2) \/
                 (ThreadPool.pop thdp1 t2 = Some thdp2)\/
                 (exists mid c' sg,ThreadPool.push thdp1 t2 mid c' sg = Some thdp2)
               ->
               ThreadPool.get_top thdp1 t1 = Some c.
  Lemma valid_tid_preserve:
    forall thdp1 i,
      @ThreadPool.valid_tid GE thdp1 i->
      forall thdp2 t,
        (exists c',@ThreadPool.update GE thdp1 t c' thdp2) \/
        (ThreadPool.pop thdp1 t = Some thdp2)\/
        (exists mid c' sg,ThreadPool.push thdp1 t mid c' sg = Some thdp2)->
        ThreadPool.valid_tid thdp2 i.

  Lemma valid_tid_backwards_preserve:
    forall thdp2 i,
      @ThreadPool.valid_tid GE thdp2 i->
      forall thdp1 t,
        (exists c',@ThreadPool.update GE thdp1 t c' thdp2) \/
        (ThreadPool.pop thdp1 t = Some thdp2)\/
        (exists mid c' sg,ThreadPool.push thdp1 t mid c' sg = Some thdp2)->
        ThreadPool.valid_tid thdp1 i.

  Lemma halted_preserve:
    forall thdp1 t,
      @ThreadPool.halted GE thdp1 t->
      forall thdp2 t',
        (exists c',@ThreadPool.update GE thdp1 t' c' thdp2) \/
        (ThreadPool.pop thdp1 t' = Some thdp2)\/
        (exists mid c' sg tp',ThreadPool.push thdp1 t' mid c' sg = Some thdp2 /\ ThreadPool.get_top thdp1 t' = Some tp')->
        ThreadPool.halted thdp2 t.
 
  Lemma halted_preserve_alter:
    forall thdp2 t,
      @ThreadPool.halted GE thdp2 t->
      forall thdp1,ThreadPool.pop thdp1 t = Some thdp2->
              forall thdp t',
                (exists c',@ThreadPool.update GE thdp t' c' thdp1) \/
                (ThreadPool.pop thdp t' = Some thdp1 /\ t <> t')\/
                (exists mid c' sg tp',ThreadPool.push thdp t' mid c' sg = Some thdp1 /\ ThreadPool.get_top thdp1 t' = Some tp')->
                forall thdp',ThreadPool.pop thdp t = Some thdp'->
                        ThreadPool.halted thdp' t.
  Lemma halted_backwards_preserve:
    forall thdp2 t,
      @ThreadPool.halted GE thdp2 t->
      forall thdp1 t',
        (exists c',@ThreadPool.update GE thdp1 t' c' thdp2) \/
        (ThreadPool.pop thdp1 t' = Some thdp2 /\ t <> t')\/
        (exists mid c' sg,ThreadPool.push thdp1 t' mid c' sg = Some thdp2)->
        ThreadPool.halted thdp1 t.
  Lemma thdp_update_unique:
    forall thdp t c thdp',
      @ThreadPool.update GE thdp t c thdp'->
      forall thdp1,ThreadPool.update thdp t c thdp1->
              thdp' = thdp1.
  Lemma thdp_push_unique:
    forall thdp t mid c sg thdp' thdp'',
      @ThreadPool.push GE thdp t mid c sg = Some thdp'->
      ThreadPool.push thdp t mid c sg = Some thdp''->
      thdp'=thdp''.

  Lemma thdp_pop_unique:
    forall thdp t thdp' thdp'',
      @ThreadPool.pop GE thdp t = Some thdp'->
      ThreadPool.pop thdp t = Some thdp''->
      thdp'=thdp''.

  Lemma corestep_eff:
    forall pc l fp pc' c,
      @type_glob_step GE core pc l fp pc' ->
      getcurcore pc = Some c ->
      LEffect pc.(gm) pc'.(gm) fp (getfl c).
  Lemma glob_step_eff:
    forall pc l fp pc' c,
      @glob_step GE pc l fp pc' ->
      getcurcore pc = Some c ->
      LEffect pc.(gm) pc'.(gm) fp (getfl c).
  
  Lemma corestep_aftercore:
    forall pc l fp pc' ,
      @type_glob_step GE core pc l fp pc' ->
      exists c,getcurcore pc' = Some c.
  Lemma globstep_aftercore:
    forall x pc l fp pc',
      @type_glob_step GE x pc l fp pc'-> x <> glob_sw -> x <> glob_halt ->
      exists c,getcurcore pc' = Some c.
  Lemma corestar_aftercore:
    forall pc fp pc',
      tau_star (@type_glob_step GE core) pc fp pc' ->
      forall c0,getcurcore pc = Some c0 ->
      exists c,getcurcore pc' = Some c.
  Lemma core_Fpreservation:
    forall pc l fp pc' c c',
      @type_glob_step GE core pc l fp pc' ->
      getcurcore pc = Some c ->
      getcurcore pc' = Some c' ->
      getfl c = getfl c'.
  
  Lemma corestar_Fpreservation:
    forall pc fp pc' c c',
      tau_star (@type_glob_step GE core) pc fp pc' ->
      getcurcore pc = Some c ->
      getcurcore pc' = Some c' ->
      getfl c = getfl c'.
  Lemma subset_effect:
    forall fp1 fp2,
      FP.subset fp1 fp2 ->
      Locs.subset (effects fp1)(effects fp2).
  Lemma subset_depend:
    forall fp1 fp2,
      FP.subset fp1 fp2 ->
      Locs.subset (depends fp1)(depends fp2).
  Lemma perm_effect_lemma:
    forall m m' b ofs,
      perm_effect m m' b ofs->
      forall m0,
        perm_effect m m0 b ofs \/ perm_effect m0 m' b ofs.

  Lemma localstar_eff:
    forall i_x F cc m fp cc' m',
      InteractionSemantics.star (step (ModSem.lang (GlobEnv.modules GE i_x)) (ModSem.Ge (GlobEnv.modules GE i_x)) (FLists.get_fl (GlobEnv.freelists GE) F)) cc m fp cc' m' ->
      LEffect m m' fp (FLists.get_fl (GlobEnv.freelists GE) F).

  Lemma corestar_eff:
    forall pc fp pc' c,
      tau_star (@type_glob_step GE core) pc fp pc' ->
      getcurcore pc = Some c ->
      LEffect pc.(gm) pc'.(gm) fp (getfl c).

  Corollary localstep_locality1 :
    forall i_x F cc m fp cc' m',
      step (ModSem.lang (GlobEnv.modules GE i_x)) (ModSem.Ge (GlobEnv.modules GE i_x)) (FLists.get_fl (GlobEnv.freelists GE) F) cc m fp cc' m' ->
      forall m1,
        LPre m m1 fp (FLists.get_fl (GlobEnv.freelists GE) F) ->
        exists m1', step (ModSem.lang (GlobEnv.modules GE i_x)) (ModSem.Ge (GlobEnv.modules GE i_x)) (FLists.get_fl (GlobEnv.freelists GE) F) cc m1 fp cc' m1' /\ LPost m' m1' fp (FLists.get_fl (GlobEnv.freelists GE) F).
  
  Corollary corestep_locality1 :
    forall pc l fp pc' c,
      @type_glob_step GE core pc l fp pc' ->
      getcurcore pc = Some c ->
      forall pc1,
        getcurcore pc1 = Some c ->
        LPre pc.(gm) pc1.(gm) fp (getfl c) ->
        exists pc2 c',
          @type_glob_step GE core pc1 l fp pc2 /\ LPost pc'.(gm) pc2.(gm) fp (getfl c) /\ getcurcore pc2 = Some c' /\getcurcore pc' = Some c'.

 

  Definition Freelists := GlobEnv.freelists GE.
  Definition flmap (t:tid):=
    fun i:nat=> Freelists.(FLists.flist_content) (Freelists.(FLists.thread_flmap) t i).

  Definition allocated_block := GMem.valid_block.
  Definition GlobalAlloc (m1 m2:gmem)(t:tid):Prop:=
    forall b,
      ~ allocated_block m1 b ->
      allocated_block m2 b ->
      exists i,
        MemAux.in_fl (flmap t i) b.
  Definition GlobalFreelistEq (m1 m2:gmem)(t:tid):Prop:=
    forall b i,
      MemAux.in_fl (flmap t i) b ->
      allocated_block m1 b <-> allocated_block m2 b.
  Lemma GlobalAlloc_refl: forall m t, GlobalAlloc m m t.
  
  Lemma GlobalFreelistEq_refl: forall m t, GlobalFreelistEq m m t.
  Lemma GlobalFreelistEq_comm: forall m1 m2 t,GlobalFreelistEq m1 m2 t ->GlobalFreelistEq m2 m1 t.
  Lemma LocalAlloc_GlobalAlloc:
    forall m1 m2 t i fl,
      LocalAlloc m1 m2 fl ->
      flmap t i = fl ->
      GlobalAlloc m1 m2 t.
  Lemma GlobalFreelistEq_freelisteq:
    forall m1 m2 t i fl,
      GlobalFreelistEq m1 m2 t->
      flmap t i = fl ->
      FreelistEq m1 m2 fl.
  Definition GEffect (m1 m2:gmem)(fp:FP.t)(t:tid):Prop:=
    MemEffect m1 m2 fp /\ GlobalAlloc m1 m2 t.
  Definition GPre (m1 m2:gmem)(fp:FP.t)(t:tid):Prop:=
    MemPre m1 m2 fp /\ GlobalFreelistEq m1 m2 t.
  Definition GPost (m1 m2:gmem)(fp:FP.t)(t:tid):Prop:=
    MemPost m1 m2 fp /\ GlobalFreelistEq m1 m2 t.
  Lemma GPre_comm:forall m1 m2 fp t, GPre m1 m2 fp t-> GPre m2 m1 fp t.
  Lemma GPre_subset:
    forall m1 m2 fp1 fp2 t,
      GPre m1 m2 fp1 t->
      FP.subset fp2 fp1 ->
      GPre m1 m2 fp2 t.
  Lemma GPost_comm:forall m1 m2 fp t, GPost m1 m2 fp t-> GPost m2 m1 fp t.
  Lemma GPost_union:
    forall m1 m2 m1' m2' fp1 fp2 t,
      GPost m1 m2 fp1 t-> GEffect m1 m1' fp2 t-> GEffect m2 m2' fp2 t->
      GPost m1' m2' fp2 t ->GPost m1' m2' (FP.union fp1 fp2) t.
  Lemma LEffect_GEffect:
    forall t i m1 m2 fl fp,
      LEffect m1 m2 fp fl ->
      flmap t i = fl ->
      GEffect m1 m2 fp t.
 Lemma GPre_LEffect_GPost_Rule:
    forall m0 m1 m0' m1' fp1 fp2 fl t i,
      flmap t i = fl ->
      GPre m0 m0' (FP.union fp1 fp2) t->
      LEffect m0 m1 fp1 fl ->
      LEffect m0' m1' fp1 fl->
      GPost m1 m1' fp1 t ->
      GPre m1 m1' fp2 t.
  Lemma GPost_LEffect_GPost_Rule1:
    forall m0 m1 m0' m1' fp1 fp2 fl t i,
      flmap t i = fl ->
      GPost m0 m1 fp1 t ->
      LEffect m0 m0' fp2 fl ->
      LEffect m1 m1' fp2 fl ->
      GPost m0' m1' fp2 t ->
      GPost m0' m1' (FP.union fp1 fp2) t.

  Lemma GPre_GEffect_GPost_Rule:
    forall m0 m1 m0' m1' fp1 fp2 t ,
      GPre m0 m0' (FP.union fp1 fp2) t->
      GEffect m0 m1 fp1 t ->
      GEffect m0' m1' fp1 t->
      GPost m1 m1' fp1 t ->
      GPre m1 m1' fp2 t.
  Lemma GPost_GEffect_GPost_Rule1:
    forall m0 m1 m0' m1' fp1 fp2 t ,
      GPost m0 m1 fp1 t ->
      GEffect m0 m0' fp2 t ->
      GEffect m1 m1' fp2 t ->
      GPost m0' m1' fp2 t ->
      GPost m0' m1' (FP.union fp1 fp2) t.
    Hypothesis wd_GE:GlobEnv.wd GE.
  Lemma GEffect_fpsmile_disj_GPre_Rule:
    forall m0 m1 fp1 fp2 t1 t2,
      t1 <> t2 ->
      GEffect m0 m1 fp1 t1 ->
      FP.smile fp1 fp2 ->
      GPre m1 m0 fp2 t2.



  Definition thread_sim(pc:@ProgConfig GE)(pc':@ProgConfig GE):Prop:=
    cur_tid pc = cur_tid pc' /\
    atom_bit pc = atom_bit pc' /\
    getcurcs pc = getcurcs pc' /\
    pc.(thread_pool).(ThreadPool.next_fmap) pc.(cur_tid) = pc'.(thread_pool).(ThreadPool.next_fmap) pc'.(cur_tid).
  Lemma curcorefl_flmap_exists:
    forall thdp id c,
      ThreadPool.inv thdp->
      ThreadPool.get_top thdp id= Some c->
      exists i,flmap id i = getfl c.
  Lemma corestep_Glocality:
    forall pc l fp pc' pc1,
      @type_glob_step GE core pc l fp pc' ->
      thread_sim pc pc1 ->
      ThreadPool.inv pc.(thread_pool)->
      GPre pc.(gm) pc1.(gm) fp pc.(cur_tid) ->
      exists pc1',@type_glob_step GE core pc1 l fp pc1' /\ GPost pc'.(gm) pc1'.(gm) fp (cur_tid pc) /\ thread_sim pc' pc1'.



  Lemma callstep_Glocality:
    forall pc l fp pc' pc1,
      @type_glob_step GE call pc l fp pc'->
      thread_sim pc pc1 ->
      ThreadPool.inv pc.(thread_pool)->
      GPre pc.(gm) pc1.(gm) fp (cur_tid pc) ->
      exists pc1',@type_glob_step GE call pc1 l fp pc1' /\ GPost pc'.(gm) pc1'.(gm) fp (cur_tid pc) /\ thread_sim pc' pc1'.
  Lemma retstep_Glocality:
    forall pc l fp pc' pc1,
      @type_glob_step GE ret pc l fp pc'->
      thread_sim pc pc1 ->
      ThreadPool.inv pc.(thread_pool)->
      GPre pc.(gm) pc1.(gm) fp (cur_tid pc) ->
      exists pc1',@type_glob_step GE ret pc1 l fp pc1' /\ GPost pc'.(gm) pc1'.(gm) fp (cur_tid pc) /\ thread_sim pc' pc1'.

  Lemma entatstep_Glocality:
    forall pc l fp pc' pc1,
      @type_glob_step GE entat pc l fp pc' ->
      thread_sim pc pc1 ->
      ThreadPool.inv pc.(thread_pool) ->
      GPre pc.(gm) pc1.(gm) fp (cur_tid pc) ->
      exists pc1',@type_glob_step GE entat pc1 l fp pc1' /\ GPost pc'.(gm) pc1'.(gm) fp (cur_tid pc) /\ thread_sim pc' pc1'.
 Lemma extatstep_Glocality:
    forall pc l fp pc' pc1,
      @type_glob_step GE extat pc l fp pc' ->
      thread_sim pc pc1 ->
      ThreadPool.inv pc.(thread_pool) ->
      GPre pc.(gm) pc1.(gm) fp (cur_tid pc) ->
      exists pc1',@type_glob_step GE extat pc1 l fp pc1' /\ GPost pc'.(gm) pc1'.(gm) fp (cur_tid pc) /\ thread_sim pc' pc1'.

  Lemma efprintstep_Glocality:
    forall pc l fp pc' pc1,
      @type_glob_step GE efprint pc l fp pc' ->
      thread_sim pc pc1 ->
      ThreadPool.inv pc.(thread_pool) ->
      GPre pc.(gm) pc1.(gm) fp (cur_tid pc) ->
      exists pc1',@type_glob_step GE efprint pc1 l fp pc1' /\ GPost pc'.(gm) pc1'.(gm) fp (cur_tid pc) /\ thread_sim pc' pc1'.



  Lemma globhaltstep_Glocality:
    forall pc l fp pc' pc1,
      @type_glob_step GE glob_halt pc l fp pc' ->
      thread_sim pc pc1 ->
      ThreadPool.inv pc.(thread_pool) ->
      GPre pc.(gm) pc1.(gm) fp (cur_tid pc) ->
      exists pc1',@type_glob_step GE glob_halt pc1 l fp pc1' /\ GPost pc'.(gm) pc1'.(gm) fp (cur_tid pc) /\ thread_sim pc' pc1'.



  
 

  Lemma globstep_Glocality:
    forall pc l fp pc' pc1,
      @glob_step GE pc l fp pc'->
      l <> sw ->
      thread_sim pc pc1 ->
      ThreadPool.inv pc.(thread_pool)->
      GPre pc.(gm) pc1.(gm) fp (cur_tid pc)->
      exists pc2,glob_step pc1 l fp pc2 /\ GPost pc'.(gm) pc2.(gm) fp (cur_tid pc) /\ thread_sim pc' pc2.
  Lemma globstep_eff:
    forall pc l fp pc',
      @glob_step GE pc l fp pc'->
      ThreadPool.inv pc.(thread_pool)->
      GEffect pc.(gm) pc'.(gm) fp pc.(cur_tid).

  Lemma taustar_eff:
    forall pc fp pc',
      tau_star (@glob_step GE) pc fp pc'->
      ThreadPool.inv pc.(thread_pool)->
      GEffect pc.(gm) pc'.(gm) fp pc.(cur_tid).

  
  Lemma taustar_Glocality:
    forall pc fp pc' pc1,
      tau_star (@glob_step GE) pc fp pc'->
      ThreadPool.inv pc.(thread_pool)->
      thread_sim pc pc1->
      ThreadPool.inv pc1.(thread_pool)->
      GPre pc.(gm) pc1.(gm) fp (cur_tid pc)->
      exists pc2,tau_star glob_step pc1 fp pc2 /\ GPost pc'.(gm) pc2.(gm) fp (cur_tid pc) /\ thread_sim pc' pc2.

  
  Lemma npnsw_step_Glocality:
    forall pc l fp pc' pc1,
      @glob_npnsw_step GE pc l fp pc'->
      thread_sim pc pc1 ->
      ThreadPool.inv pc.(thread_pool)->
      GPre pc.(gm) pc1.(gm) fp (cur_tid pc) ->
      exists pc1',@glob_npnsw_step GE pc1 l fp pc1' /\ GPost pc'.(gm) pc1'.(gm) fp (cur_tid pc) /\ thread_sim pc' pc1'.
  
  Lemma npnsw_step_eff:
    forall pc l fp pc',
      @glob_npnsw_step GE pc l fp pc' ->
      ThreadPool.inv pc.(thread_pool) ->
      GEffect pc.(gm) pc'.(gm) fp pc.(cur_tid).
  Lemma npnsw_step_thdpinv:
    forall pc l fp pc',
      @glob_npnsw_step GE pc l fp pc'->
      ThreadPool.inv pc.(thread_pool) ->
      ThreadPool.inv pc'.(thread_pool).
  Lemma npnsw_taustar_thdpinv:
    forall pc fp pc',
      tau_star (@glob_npnsw_step GE) pc fp pc'->
      ThreadPool.inv pc.(thread_pool) ->
      ThreadPool.inv pc'.(thread_pool).
  Lemma npnsw_taustar_eff:
    forall pc fp pc',
      tau_star (@glob_npnsw_step GE) pc fp pc'->
      ThreadPool.inv pc.(thread_pool) ->
      GEffect pc.(gm) pc'.(gm) fp pc.(cur_tid).


  Lemma npnsw_taustar_Glocality:
    forall pc fp pc',
      tau_star glob_npnsw_step pc fp pc'->
      forall pc1,
        thread_sim pc pc1 ->
        ThreadPool.inv pc.(thread_pool)->
        ThreadPool.inv pc1.(thread_pool) ->
        GPre pc.(gm) pc1.(gm) fp (cur_tid pc) ->
        exists pc1',tau_star glob_npnsw_step pc1 fp pc1' /\ GPost pc'.(gm) pc1'.(gm) fp (cur_tid pc) /\ thread_sim pc' pc1'.

  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).
  Lemma corestep_getanocore:
    forall pc pc1 fp t c,
      @type_glob_step GE core pc tau fp pc1 ->
      ThreadPool.get_top pc.(thread_pool) t = Some c ->
      t <> cur_tid pc->
      ThreadPool.get_top pc1.(thread_pool) t = Some c.
  Lemma corestar_getanocore:
    forall pc pc1 fp,
      tau_star (@type_glob_step GE core) pc fp pc1 ->
      forall t c,
        ThreadPool.get_top pc.(thread_pool) t = Some c ->
        t <> cur_tid pc->
        ThreadPool.get_top pc1.(thread_pool) t = Some c.
  Lemma dif_thd_disj_fl:
    forall pc t1 t2 c1 c2,
      ThreadPool.get_top pc.(thread_pool) t1 = Some c1 ->
      ThreadPool.get_top pc.(thread_pool) t2 = Some c2 ->
      t1 <> t2 ->
      GlobEnv.wd GE ->
      @ThreadPool.inv GE pc.(thread_pool) ->
      MemAux.disj (FLists.get_fl (GlobEnv.freelists GE) (Core.F c2)) (FLists.get_fl (GlobEnv.freelists GE) (Core.F c1)).
   
  Lemma local_reorder_rule2:
    forall i1 F1 cc1 m1 fp1 cc1' m1' i2 F2 fp2 cc2 cc2' m2,
      let md1:= GlobEnv.modules GE i1 in
      let fl1:= FLists.get_fl (GlobEnv.freelists GE) F1 in
      let md2:= GlobEnv.modules GE i2 in
      let fl2:= FLists.get_fl(GlobEnv.freelists GE) F2 in
      step (ModSem.lang md1)(ModSem.Ge md1) fl1 cc1 m1 fp1 cc1' m1' ->
      step (ModSem.lang md2)(ModSem.Ge md2) fl2 cc2 m1' fp2 cc2' m2 ->
      MemAux.disj fl1 fl2 ->
      FP.smile fp1 fp2 ->
      exists m', step (ModSem.lang md2)(ModSem.Ge md2) fl2 cc2 m1 fp2 cc2' m'/\
            exists m'',step (ModSem.lang md1)(ModSem.Ge md1) fl1 cc1 m' fp1 cc1' m'' /\
                  GMem.eq' m'' m2.
  Lemma ptree_set_sym:
    forall A i j m (v1 v2:A),
      i <> j ->
      Maps.PTree.set i v1 (Maps.PTree.set j v2 m) =
      Maps.PTree.set j v2 (Maps.PTree.set i v1 m).
  Lemma pmap_set_sym:
    forall A i j m (v1 v2:A),
      i <> j ->
      Maps.PMap.set i v1 (Maps.PMap.set j v2 m) =
      Maps.PMap.set j v2 (Maps.PMap.set i v1 m).
  Lemma thdp_upd_dif_eq:
    forall thdp thdp1 thdp1' thdp2 thdp2' t1 t2 c1 c2,
      @ThreadPool.update GE thdp t1 c1 thdp1 ->
      ThreadPool.update thdp1 t2 c2 thdp2 ->
      ThreadPool.update thdp t2 c2 thdp1'->
      ThreadPool.update thdp1' t1 c1 thdp2' ->
      t1 <> t2 ->
      thdp2 = thdp2'.
 
  Lemma corestep_reorder_rule:
    forall t1 t2 pc pc1 pc2 fp1 fp2,
      @type_glob_step GE core ({-|pc,t1}) tau fp1 pc1 ->
      @type_glob_step GE core ({-|pc1,t2}) tau fp2 pc2 ->
      t1 <> t2 ->
      FP.smile fp1 fp2 ->
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      exists pc1',type_glob_step core ({-|pc,t2}) tau fp2 pc1' /\
             exists pc2', type_glob_step core ({-|pc1',t1}) tau fp1 pc2' /\
                     mem_eq_pc pc2 ({-|pc2',t2}).

  
  Ltac solv_thread_sym:=
    intros;
    solv_thread;
    repeat try (econstructor;simpl;solv_thread;simpl);
    solv_thread;simpl;
    try f_equal;try rewrite pmap_set_sym;auto;
    try f_equal;auto.
  Lemma thdp_update_sym:
    forall t1 t2,
      t1 <> t2->
      forall thdp1 c1' thdp2 c2' thdp3,
        @ThreadPool.update GE thdp1 t1 c1' thdp2 ->
        ThreadPool.update thdp2 t2 c2' thdp3 ->
        exists thdp',ThreadPool.update thdp1 t2 c2' thdp' /\ ThreadPool.update thdp' t1 c1' thdp3.

  Lemma thdp_update_push_sym:
    forall t1 t2,
      t1<>t2->
      forall thdp1 c1 thdp2 mid c sg thdp3,
        @ThreadPool.update GE thdp1 t1 c1 thdp2->
        ThreadPool.push thdp2 t2 mid c sg = Some thdp3->
        exists thdp',ThreadPool.push thdp1 t2 mid c sg = Some thdp'/\ ThreadPool.update thdp' t1 c1 thdp3.
  Lemma thdp_update_pop_sym:
    forall t1 t2,
      t1<>t2->
      forall thdp1 c1 thdp2 thdp3,
        @ThreadPool.update GE thdp1 t1 c1 thdp2->
        ThreadPool.pop thdp2 t2 = Some thdp3->
        exists thdp',ThreadPool.pop thdp1 t2 = Some thdp'/\
                ThreadPool.update thdp' t1 c1 thdp3.
  Lemma thdp_push_sym:
    forall t1 t2,
      t1<>t2->
      forall thdp1 mid1 c1 sg1 thdp2 mid2 c2 sg2 thdp3,
        @ThreadPool.push GE thdp1 t1 mid1 c1 sg1 = Some thdp2->
        ThreadPool.push thdp2 t2 mid2 c2 sg2 = Some thdp3->
        exists thdp',ThreadPool.push thdp1 t2 mid2 c2 sg2 = Some thdp'/\
                ThreadPool.push thdp' t1 mid1 c1 sg1 = Some thdp3.
  Lemma thdp_push_update_sym:
    forall t1 t2,t1<>t2->
            forall thdp1 mid1 c1 sg1 thdp2 c2 thdp3,
              @ThreadPool.push GE thdp1 t1 mid1 c1 sg1 = Some thdp2->
              ThreadPool.update thdp2 t2 c2 thdp3->
              exists thdp',ThreadPool.update thdp1 t2 c2 thdp'/\ ThreadPool.push thdp' t1 mid1 c1 sg1 = Some thdp3.
  Lemma thdp_push_pop_sym:
    forall t1 t2,t1<>t2->
            forall thdp1 mid1 c1 sg1 thdp2 thdp3,
              @ThreadPool.push GE thdp1 t1 mid1 c1 sg1 = Some thdp2->
              ThreadPool.pop thdp2 t2 = Some thdp3->
              exists thdp',ThreadPool.pop thdp1 t2 = Some thdp'/\
                      ThreadPool.push thdp' t1 mid1 c1 sg1=Some thdp3.
  Lemma thdp_pop_sym_weak:
    forall t1 t2,t1<>t2->
            forall thdp1 thdp2 thdp3,
              @ThreadPool.pop GE thdp1 t1 = Some thdp2->
              ThreadPool.pop thdp2 t2 = Some thdp3->
              exists thdp',ThreadPool.pop thdp1 t2 = Some thdp' /\ ThreadPool.pop thdp' t1 = Some thdp3.
  Lemma thdp_pop_sym:
    forall t1 t2,
      t1<>t2->
      forall thdp1 thdp2 c thdp3,
        @ThreadPool.pop GE thdp1 t1 = Some thdp2->
        ThreadPool.update thdp2 t1 c thdp3->
        forall thdp4 c' thdp5,
          ThreadPool.pop thdp3 t2 = Some thdp4->
          ThreadPool.update thdp4 t2 c' thdp5->
          exists tp2 tp3 tp4,
            ThreadPool.pop thdp1 t2 = Some tp2/\
            ThreadPool.update tp2 t2 c' tp3/\
            ThreadPool.pop tp3 t1 = Some tp4/\
            ThreadPool.update tp4 t1 c thdp5.
  Lemma thdp_pop_update_sym_weak:
    forall t1 t2,t1<>t2->
            forall thdp1 thdp2 c thdp3,
              @ThreadPool.pop GE thdp1 t1 = Some thdp2->
              ThreadPool.update thdp2 t2 c thdp3->
              exists thdp' ,
                ThreadPool.update thdp1 t2 c thdp'/\
                ThreadPool.pop thdp' t1 = Some thdp3.
  Lemma thdp_pop_update_sym:
    forall t1 t2,t1<>t2->
            forall thdp1 thdp2 c thdp3 c' thdp4,
              @ThreadPool.pop GE thdp1 t1 = Some thdp2->
              ThreadPool.update thdp2 t1 c thdp3->
              ThreadPool.update thdp3 t2 c' thdp4->
              exists thdp' thdp'',
                ThreadPool.update thdp1 t2 c' thdp'/\
                ThreadPool.pop thdp' t1 = Some thdp''/\
                ThreadPool.update thdp'' t1 c thdp4.
  Lemma thdp_pop_push_sym_weak:
    forall t1 t2,t1<>t2->
            forall thdp1 thdp2 mid c sg thdp3,
              @ThreadPool.pop GE thdp1 t1 = Some thdp2->
              ThreadPool.push thdp2 t2 mid c sg = Some thdp3->
              exists thdp',ThreadPool.push thdp1 t2 mid c sg = Some thdp'/\
                      ThreadPool.pop thdp' t1 = Some thdp3.
  Lemma thdp_pop_push_sym:
    forall t1 t2,t1<>t2->
            forall thdp1 c' thdp2 thdp3 mid c sg thdp4,
              @ThreadPool.pop GE thdp1 t1 = Some thdp2->
              ThreadPool.update thdp2 t1 c' thdp3->
              ThreadPool.push thdp3 t2 mid c sg = Some thdp4->
              exists thdp' thdp'',ThreadPool.push thdp1 t2 mid c sg = Some thdp'/\
                             ThreadPool.pop thdp' t1 = Some thdp'' /\
                             ThreadPool.update thdp'' t1 c' thdp4.
  Lemma gettop_valid_tid:
    forall thdp c t,
      @ThreadPool.get_top GE thdp t = Some c->
      ThreadPool.inv thdp->
      ThreadPool.valid_tid thdp t.
  Lemma step_switchable:
    forall l pc fp pc',
      @glob_step GE pc l fp pc' ->
      l <> sw ->
      atom_bit pc = O->
      ThreadPool.inv pc.(thread_pool)->
      forall t,
        glob_step ({-|pc,t}) sw FP.emp pc.

   Lemma mem_eq_local_step:
    forall m1 m2,
      GMem.eq' m1 m2->
      forall i_x F cc fp cc' m1',
        step (ModSem.lang (GlobEnv.modules GE i_x)) (ModSem.Ge (GlobEnv.modules GE i_x)) (FLists.get_fl (GlobEnv.freelists GE) F) cc m1 fp cc' m1' ->
        exists m2',step (ModSem.lang (GlobEnv.modules GE i_x)) (ModSem.Ge (GlobEnv.modules GE i_x)) (FLists.get_fl (GlobEnv.freelists GE) F) cc m2 fp cc' m2' /\ GMem.eq' m1' m2'.

  Lemma mem_eq_corestep:
    forall pc pc',
      mem_eq_pc pc pc' ->
      forall fp pce,
        @type_glob_step GE core pc tau fp pce ->
        exists pce',@type_glob_step GE core pc' tau fp pce' /\ mem_eq_pc pce pce'.
  Lemma mem_eq_core_star:
    forall pc pc',
      mem_eq_pc pc pc'->
      forall l fp pce,
        star (@type_glob_step GE core) pc l fp pce->
        exists pce',star (type_glob_step core) pc' l fp pce' /\ mem_eq_pc pce pce'.
    
  Lemma mem_eq_coreN:
    forall pc pc',
      mem_eq_pc pc pc' ->
      forall i fp pce,
        tau_N (@type_glob_step GE core) i pc fp pce ->
        exists pce',tau_N (@type_glob_step GE core) i pc' fp pce' /\ mem_eq_pc pce pce'.
  Lemma mem_eq_corestar:
    forall pc pc',
      mem_eq_pc pc pc' ->
      forall fp pce,
        tau_star (@type_glob_step GE core) pc fp pce ->
        exists pce',tau_star (@type_glob_step GE core) pc' fp pce' /\ mem_eq_pc pce pce'.
  Lemma mem_eq_globstep:
    forall pc pc',
      mem_eq_pc pc pc'->
      forall x l fp pce,
        @type_glob_step GE x pc l fp pce ->
        exists pce',type_glob_step x pc' l fp pce' /\ mem_eq_pc pce pce'.
  Lemma mem_eq_non_evt_star:
    forall pc pc',
      mem_eq_pc pc pc'->
      forall fp pc'',
        non_evt_star glob_step pc fp pc''->
        exists pc1,non_evt_star glob_step pc' fp pc1 /\ mem_eq_pc pc'' pc1.
    
  Lemma mem_eq_pc_finalstate:
    forall pc pc',
      mem_eq_pc pc pc'->
      final_state pc->
      final_state pc'.
  Lemma mem_eq_pc_abort:
    forall pc pc',
      mem_eq_pc pc pc'->
      abort pc->
      abort pc'.
  Lemma mem_eq_swstar:
    forall pc pc',
      mem_eq_pc pc pc'->
      forall pc1,
        sw_star glob_step pc pc1 ->
        exists pc1',sw_star glob_step pc' pc1' /\ mem_eq_pc pc1 pc1'.
     
  Lemma mem_eq_pc_silent_diverge:
    forall pc pc',
      mem_eq_pc pc pc'->
      silent_diverge glob_step pc->
      silent_diverge glob_step pc'.
    
  Inductive starN : nat -> @ProgConfig GE->list glabel ->FP.t->@ProgConfig GE ->Prop:=
  | star0:forall s,starN 0 s nil FP.emp s
  | star_step':forall i s1 e fp1 s2 l fp2 s3,
      glob_step s1 e fp1 s2->
      starN i s2 l fp2 s3->
      starN (S i) s1 (cons e l) (FP.union fp1 fp2) s3.

  Lemma star_starN_equiv:
    forall pc pc' l fp,
      star (@glob_step GE) pc l fp pc' <-> exists i,starN i pc l fp pc'.
 
  Lemma mem_eq_globstar:
    forall pc pc',
      mem_eq_pc pc pc'->
      forall l fp pce,
        star (@glob_step GE) pc l fp pce ->
        exists pce',star glob_step pc' l fp pce' /\ mem_eq_pc pce pce'.
    
  Lemma mem_eq_glob_taustar:
    forall pc pc',
      mem_eq_pc pc pc'->
      forall fp pce,
        tau_star (@glob_step GE) pc fp pce ->
        exists pce',tau_star glob_step pc' fp pce' /\ mem_eq_pc pce pce'.
  Lemma mem_eq_glob_tauN:
    forall pc pc',
      mem_eq_pc pc pc'->
      forall i fp pce,
        tau_N (@glob_step GE) i pc fp pce->
        exists pce',tau_N glob_step i pc' fp pce' /\ mem_eq_pc pce pce'.
  Lemma mem_eq_npnsw_step_star:
    forall pc pc',
      mem_eq_pc pc pc'->
      forall fp pce,
        tau_star (@glob_npnsw_step GE) pc fp pce ->
        exists pce',tau_star glob_npnsw_step pc' fp pce' /\ mem_eq_pc pce pce'.

  Lemma mem_eq_npnsw_step_starN:
    forall pc pc',
      mem_eq_pc pc pc'->
      forall i fp pce,
        tau_N (@glob_npnsw_step GE) i pc fp pce ->
        exists pce',tau_N glob_npnsw_step i pc' fp pce' /\ mem_eq_pc pce pce'.


  Lemma np_predict_tau_star:
    forall ge pc fp fp' t,
      @np_predict ge pc t fp fp'->
      exists pc',tau_star np_step ({-|pc,t}) fp pc'.
  Lemma tau_star_glob_star:
    forall ge pc fp pc',
      tau_star (@np_step ge) pc fp pc'->
      tau_star glob_step pc fp pc'.
  Lemma np_step_glob_step:
    forall ge pc l fp pc',
      @np_step ge pc l fp pc'->
      exists l',star (@glob_step ge) pc l' fp pc'.
    
  Lemma np_star_glob_star:
    forall ge pc l fp pc',
      star (@np_step ge) pc l fp pc' ->
      exists l',star (@glob_step ge) pc l' fp pc'.
  Lemma npnsw_step_I_corestep:
    forall ge pc l fp pc',
      @glob_npnsw_step ge pc l fp pc' ->
      atom_bit pc = I ->
      type_glob_step core pc l fp pc'.
  Lemma npnsw_taustar_I_core_taustar:
    forall ge pc fp pc',
      tau_star (@glob_npnsw_step ge) pc fp pc' ->
      atom_bit pc = I ->
      tau_star (type_glob_step core) pc fp pc'.
  Lemma npnsw_step_pc_valid_tid_preservation:
    forall ge pc l fp pc' t,
      @glob_npnsw_step ge pc l fp pc' ->
      GSimDefs.pc_valid_tid pc t ->
      GSimDefs.pc_valid_tid pc' t.

  Lemma npnsw_taustar_pc_valid_tid_preservation:
    forall ge pc fp pc' t,
      tau_star (@glob_npnsw_step ge) pc fp pc'->
      GSimDefs.pc_valid_tid pc t ->
      GSimDefs.pc_valid_tid pc' t.
    
  Lemma npnsw_step_O_preservation:
    forall ge pc l fp pc',
      @glob_npnsw_step ge pc l fp pc'->
      atom_bit pc = O ->
      atom_bit pc' = O.
  Lemma npnsw_taustar_O_preservation:
    forall ge pc fp pc',
      tau_star (@glob_npnsw_step ge) pc fp pc'->
      atom_bit pc = O ->
      atom_bit pc' = O.
  Lemma npnsw_step_tid_preservation:
    forall ge pc l fp pc',
      @glob_npnsw_step ge pc l fp pc'->
      cur_tid pc = cur_tid pc'.
  Lemma npnsw_taustar_tid_preservation:
    forall ge pc fp pc',
      tau_star (@glob_npnsw_step ge) pc fp pc'->
      cur_tid pc = cur_tid pc'.
  Lemma npnsw_step_diff_thread_sim:
    forall pc l fp pc' t,
      glob_npnsw_step pc l fp pc'->
      t <> cur_tid pc ->
      thread_sim ({-|pc,t})({-|pc',t}).
  Lemma npnsw_taustar_diff_thread_sim:
    forall pc fp pc' t,
      tau_star glob_npnsw_step pc fp pc'->
      t <> cur_tid pc ->
      thread_sim ({-|pc,t})({-|pc',t}).
  Lemma tau_star_to_star:
    forall (A:Type) step (s1:A) fp (s2:A),
      tau_star step s1 fp s2 ->
      exists l,star step s1 l fp s2.
  Lemma cons_star_star:
    forall (A:Type) step (s1 s2 s3:A) l1 l2 fp1 fp2,
      star step s1 l1 fp1 s2 ->
      star step s2 l2 fp2 s3 ->
      star step s1 (app l1 l2)(FP.union fp1 fp2) s3.
  Lemma npnsw_star_glob_star:
    forall ge pc l fp pc',
      star (@glob_npnsw_step ge) pc l fp pc'->
      star glob_step pc l fp pc'.

  Lemma extended_glob_reorder_case1:
    forall x t1 t2 l1 l2 pc pc1 pc2 fp1 fp2,
      @type_glob_step GE core ({-|pc,t1}) l1 fp1 pc1->
      @type_glob_step GE x ({-|pc1,t2}) l2 fp2 pc2->
      atom_bit pc1 = atom_bit pc2 ->
      t1 <> t2->
      FP.smile fp1 fp2 ->
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      exists pc1',type_glob_step x ({-|pc,t2}) l2 fp2 pc1' /\
             exists pc2',type_glob_step core ({-|pc1',t1}) l1 fp1 pc2' /\
                    mem_eq_pc pc2 ({-|pc2',cur_tid pc2}).

  Ltac clear_ands:=
    try match goal with
        | H : _ |- _ /\ _ => split
        | H : _ |- exists _, _ => eexists
        end.
  
  Ltac gettop_simpl:=
    try match goal with
          H:_|-ThreadPool.get_top _ _ = _ =>
          try (eapply gettop_preserve;eauto;try (left;eauto;fail);try(right;left;eauto;fail);try(right;right;eauto;fail);fail);
          try (eapply gettop_backwards_preserve;eauto;try (left;eauto;fail);try(right;left;eauto;fail);try(right;right;eauto;fail);fail) end.

  Ltac build_step:=
    try match goal with
        | H : _ |- type_glob_step ?a _ _ _ _ => econstructor;gettop_simpl;eauto;gettop_simpl end.
  Ltac valid_tid_simpl:=
    try match goal with
          H:_|- ThreadPool.valid_tid _ _ =>
          try (eapply valid_tid_preserve;eauto;try (left;eauto;fail);try(right;left;eauto;fail);try(right;right;eauto;fail);fail);
          try (eapply valid_tid_backwards_preserve;eauto;try (left;eauto;fail);try(right;left;eauto;fail);try(right;right;eauto;fail);fail) end.
  Ltac halted_preserve_auto':=
    try match goal with
          | H: _ |- ThreadPool.halted _ _ =>
            try (eapply halted_backwards_preserve;eauto;try (left;eauto;fail);try(right;left;eauto;fail);try(right;right;eauto;fail);fail);
            try (eapply halted_preserve;eauto;try (left;eauto;fail);try(right;left;eauto;fail);try(right;right;eexists;eexists;eexists;eexists;esplit;eauto;fail);fail)
          | H: ~ ThreadPool.halted _ ?t |- ~ ThreadPool.halted _ ?t =>
            intro;contradict H;
            try (eapply halted_backwards_preserve;eauto;try (left;eauto;fail);try(right;left;eauto;fail);try(right;right;eauto;fail);fail);
            try (eapply halted_preserve;eauto;try (left;eauto;fail);try(right;left;eauto;fail);try(right;right;eexists;eexists;eexists;eexists;esplit;eauto;fail);fail)
        end.
  
  Ltac mem_eq_tactic:=
    simpl;
    try match goal with H:_|-mem_eq_pc ?a ?a => apply mem_eq_pc_refl end.
                    
  Lemma extended_glob_reorder_case2:
    forall x t1 t2 l1 l2 pc pc1 pc2 fp1 fp2,
      @type_glob_step GE call ({-|pc,t1}) l1 fp1 pc1->
      @type_glob_step GE x ({-|pc1,t2}) l2 fp2 pc2->
      atom_bit pc1 = atom_bit pc2->
      t1 <> t2->
      FP.smile fp1 fp2 ->
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      exists pc1',type_glob_step x ({-|pc,t2}) l2 fp2 pc1'/\
             exists pc2',type_glob_step call ({-|pc1',t1}) l1 fp1 pc2' /\
                    mem_eq_pc pc2 ({-|pc2',cur_tid pc2}).
  Ltac steptac:=
    do 2 clear_ands;build_step;valid_tid_simpl;halted_preserve_auto';mem_eq_tactic.
  Lemma extended_glob_reorder_case3:
    forall x t1 t2 l1 l2 pc pc1 pc2 fp1 fp2,
      @type_glob_step GE ret ({-|pc,t1}) l1 fp1 pc1->
      @type_glob_step GE x ({-|pc1,t2}) l2 fp2 pc2->
      atom_bit pc1 = atom_bit pc2->
      t1 <> t2->
      FP.smile fp1 fp2 ->
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      exists pc1',type_glob_step x ({-|pc,t2}) l2 fp2 pc1'/\
             exists pc2',type_glob_step ret ({-|pc1',t1}) l1 fp1 pc2' /\
                    mem_eq_pc pc2 ({-|pc2',cur_tid pc2}).
    
  Lemma extended_glob_reorder_case4:
    forall x t1 t2 l1 l2 pc pc1 pc2 fp1 fp2,
      @type_glob_step GE efprint ({-|pc,t1}) l1 fp1 pc1->
      @type_glob_step GE x ({-|pc1,t2}) l2 fp2 pc2->
      atom_bit pc1 = atom_bit pc2->
      t1 <> t2->
      FP.smile fp1 fp2 ->
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      exists pc1',type_glob_step x ({-|pc,t2}) l2 fp2 pc1'/\
             exists pc2',type_glob_step efprint ({-|pc1',t1}) l1 fp1 pc2' /\
                    mem_eq_pc pc2 ({-|pc2',cur_tid pc2}).
  
  Lemma multisw:
    forall pc pc1 pc2,
      @type_glob_step GE glob_sw pc sw FP.emp pc1->
      type_glob_step glob_sw pc1 sw FP.emp pc2->
      type_glob_step glob_sw pc sw FP.emp pc2.
  Lemma uselesssw:
    forall pc1 pc2,
      @glob_step GE pc1 sw FP.emp pc2->
      cur_tid pc1 = cur_tid pc2->
      pc1 = pc2.

  Lemma extended_glob_reorder_case5:
    forall x t1 t2 l1 l2 pc pc1 pc2 fp1 fp2,
      @type_glob_step GE glob_halt ({-|pc,t1}) l1 fp1 pc1->
      @type_glob_step GE x ({-|pc1,t2}) l2 fp2 pc2->
      atom_bit pc1 = atom_bit pc2->
      t1 <> t2->
      FP.smile fp1 fp2 ->
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      l2 <> sw->
      exists pc1',type_glob_step x ({-|pc,t2}) l2 fp2 pc1'/\
             exists pc2',type_glob_step glob_halt ({-|pc1',t1}) l1 fp1 pc2' /\
                    mem_eq_pc pc2 ({-|pc2',cur_tid pc2}).



  Lemma globstep_reorder_rule:
     forall x y t1 t2 l1 l2 pc pc1 pc2 fp1 fp2,
      @type_glob_step GE y ({-|pc,t1}) l1 fp1 pc1->
      @type_glob_step GE x ({-|pc1,t2}) l2 fp2 pc2->
      atom_bit pc = atom_bit pc1 ->
      atom_bit pc1 = atom_bit pc2->
      t1 <> t2->
      FP.smile fp1 fp2 ->
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      l1 <> sw->
      l2 <> sw->
      exists pc1',type_glob_step x ({-|pc,t2}) l2 fp2 pc1'/\
             exists pc2',type_glob_step y ({-|pc1',t1}) l1 fp1 pc2' /\
                    mem_eq_pc pc2 ({-|pc2',cur_tid pc2}).

   Lemma corestar_reorder_rule:
    forall t1 t2 pc pc1 pc2 fp1 fp2,
      @type_glob_step GE core ({-|pc,t1}) tau fp1 pc1 ->
      tau_star (@type_glob_step GE core) ({-|pc1,t2}) fp2 pc2 ->
      t1 <> t2 ->
      FP.smile fp1 fp2 ->
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      exists pc1',tau_star (type_glob_step core) ({-|pc,t2}) fp2 pc1' /\
             exists pc2', type_glob_step core ({-|pc1',t1}) tau fp1 pc2' /\
                     mem_eq_pc pc2 ({-|pc2',t2}).


  Lemma glob_npnsw_step_type:
    forall pc l fp pc',
      @glob_npnsw_step GE pc l fp pc'->
      exists x,type_glob_step x pc l fp pc' /\ (x = core \/ x = call \/ x = ret).

  Lemma npnswstep_reorder:
    forall t1 t2 pc pc1 pc2 fp1 fp2,
      @glob_npnsw_step GE ({-|pc,t1}) tau fp1 pc1->
      glob_npnsw_step ({-|pc1,t2}) tau fp2 pc2->
      t1 <> t2 ->
      FP.smile fp1 fp2->
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      exists pc1',glob_npnsw_step ({-|pc,t2}) tau fp2 pc1' /\
             exists pc2',glob_npnsw_step ({-|pc1',t1}) tau fp1 pc2' /\
                    mem_eq_pc pc2 ({-|pc2',cur_tid pc2}).

  Lemma npnswstep_star_reorder:
    forall t1 t2 pc pc1 pc2 fp1 fp2,
      @glob_npnsw_step GE ({-|pc,t1}) tau fp1 pc1->
      tau_star glob_npnsw_step ({-|pc1,t2}) fp2 pc2->
      t1 <> t2 ->
      FP.smile fp1 fp2->
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      exists pc1',tau_star glob_npnsw_step ({-|pc,t2}) fp2 pc1'/\
             exists pc2',glob_npnsw_step ({-|pc1',t1}) tau fp1 pc2' /\
                    mem_eq_pc pc2 ({-|pc2',cur_tid pc2}).


  Lemma npnswstep_corestar_reorder:
    forall t1 t2 pc pc1 pc2 fp1 fp2,
      @glob_npnsw_step GE ({-|pc,t1}) tau fp1 pc1->
      tau_star (type_glob_step core) ({-|pc1,t2}) fp2 pc2->
      t1 <> t2 ->
      FP.smile fp1 fp2->
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      exists pc1',tau_star (type_glob_step core) ({-|pc,t2}) fp2 pc1'/\
             exists pc2',glob_npnsw_step ({-|pc1',t1}) tau fp1 pc2' /\
                    mem_eq_pc pc2 ({-|pc2',cur_tid pc2}).


  Lemma outofatom_glob_reorder_rule:
    forall pc pc1 pc2 pc3 fp1 fp2 x y l1 l2,
      atom_bit pc = O ->
      atom_bit pc1 = O->
      atom_bit pc2 = O ->
      atom_bit pc3 = O->
      cur_tid pc1 <> cur_tid pc2->
      l1 <> sw ->
      l2 <> sw ->
      @type_glob_step GE x pc l1 fp1 pc1->
      type_glob_step glob_sw pc1 sw FP.emp pc2->
      type_glob_step y pc2 l2 fp2 pc3->
      FP.smile fp1 fp2 ->
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      type_glob_step glob_sw pc sw FP.emp ({-|pc,cur_tid pc2})/\
      exists pc',type_glob_step y ({-|pc,cur_tid pc2}) l2 fp2 pc' /\
            type_glob_step glob_sw pc' sw FP.emp ({-|pc',cur_tid pc})/\
            exists pc'',type_glob_step x ({-|pc',cur_tid pc}) l1 fp1 pc'' /\
                   mem_eq_pc pc3 ({-|pc'',cur_tid pc3}).
 


  Inductive stepN:(@ProgConfig GE->glabel->FP.t->@ProgConfig GE->Prop)->nat->@ProgConfig GE->list glabel->FP.t->@ProgConfig GE->Prop:=
  | stepN_emp:forall step pc,stepN step 0 pc nil FP.emp pc
  | stepN_cons:forall step i pc l fp l' fp' pc' pc'',
      stepN step i pc' l' fp' pc''->
      step pc l fp pc'->
      stepN step (S i) pc (cons l l')(FP.union fp fp') pc''.

  Lemma stepN_star:
    forall step i pc l fp pc',
      stepN step i pc l fp pc'->star step pc l fp pc'.
  Lemma star_stepN:
    forall step pc l fp pc',
      star step pc l fp pc'->exists i,stepN step i pc l fp pc'.
  Lemma mem_eq_corestepN:
    forall i pc l fp pc' pc1,
      mem_eq_pc pc pc1->
      stepN (type_glob_step core) i pc l fp pc'->
      exists pc1',stepN (type_glob_step core) i pc1 l fp pc1' /\ mem_eq_pc pc' pc1'.
    

  Lemma entat_afterstep:
    forall pc pc' x l fp,
      atom_bit pc = I ->
      @type_glob_step GE x pc l fp pc' ->
      x = core \/ x = extat.


  Lemma mem_eq_pc_change:
    forall t pc pc',
      mem_eq_pc pc pc'->
      mem_eq_pc ({-|pc,t})({-|pc',t}).

 

  Definition atom_block (pc:@ProgConfig GE)(l:list glabel)(fp:FP.t)(pc':@ProgConfig GE):Prop:=
    exists pc1 l' pc2,
      type_glob_step entat pc tau FP.emp pc1 /\
      star (type_glob_step core) pc1 l' fp pc2 /\
      type_glob_step extat pc2 tau FP.emp pc' /\
      l = app (cons tau l') (cons tau nil).
  Definition half_atom_block (pc:@ProgConfig GE)(l:list glabel)(fp:FP.t)(pc':@ProgConfig GE):Prop:=
    exists pc1 l1,
      type_glob_step entat pc tau FP.emp pc1 /\
      star (type_glob_step core) pc1 l1 fp pc' /\
      l = cons tau l1.
   
  Lemma adjust_list_order:
    forall l1 l2,
      app(app (cons tau l1)(cons tau nil)) l2 = (cons tau(app l1(cons tau l2))).


  Lemma changepc_curtid: forall pc:@ProgConfig GE,({-|pc,cur_tid pc}) = pc.
  Lemma appnil:forall A l,@app A l nil = l.



  Lemma atomblock_open_reorderstep1:
    forall x l t1 t2 pc pc1 pc2 fp,
      @type_glob_step GE x ({-|pc,t1}) l fp pc1->
      atom_bit pc = atom_bit pc1 ->
      l <> sw ->
      t1 <> t2 ->
      type_glob_step entat ({-|pc1,t2}) tau FP.emp pc2 ->
      exists pc1',type_glob_step entat ({-|pc,t2}) tau FP.emp pc1' /\
             exists pc2',type_glob_step x (changepc pc1' t1 O) l fp pc2' /\
                    thread_pool pc2' = thread_pool pc2 /\
                    gm pc2' = gm pc2.
  
  Lemma atomblock_open_reorderstep2:
    forall x l t1 t2 pc pc1 pc2 fp,
      @type_glob_step GE x (changepc pc t1 O) l fp pc1->
      atom_bit pc1 = O ->
      l <> sw ->
      t1 <> t2 ->
      type_glob_step extat (changepc pc1 t2 I) tau FP.emp pc2 ->
      exists pc1',type_glob_step extat (changepc pc t2 I) tau FP.emp pc1' /\
             exists pc2',type_glob_step x (changepc pc1' t1 O) l fp pc2' /\
                    thread_pool pc2' = thread_pool pc2 /\
                    gm pc2' = gm pc2.
  
  Lemma atomblock_open_reorder_corestep:
    forall x l t1 t2 pc pc1 pc2 fp1 fp2,
      @type_glob_step GE x (changepc pc t1 O) l fp1 pc1 ->
      atom_bit pc1 = O ->
      l <> sw ->
      t1 <> t2 ->
      type_glob_step core (changepc pc1 t2 I) tau fp2 pc2 ->
      FP.smile fp1 fp2 ->
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      exists pc1',type_glob_step core (changepc pc t2 I) tau fp2 pc1'/\
             exists pc2',type_glob_step x (changepc pc1' t1 O) l fp1 pc2' /\
                    thread_pool pc2' = thread_pool pc2 /\
                    GMem.eq' pc2'.(gm) pc2.(gm).

  




    
  Lemma atomblock_open_reorder_core_tauN:
    forall i x l t1 t2 pc pc1 pc2 fp1 fp2,
      @type_glob_step GE x (changepc pc t1 O) l fp1 pc1 ->
      atom_bit pc1 = O ->
      l <> sw ->
      t1 <> t2 ->
      tau_N (type_glob_step core) i (changepc pc1 t2 I) fp2 pc2 ->
      FP.smile fp1 fp2 ->
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      exists pc1',tau_N (type_glob_step core) i (changepc pc t2 I) fp2 pc1'/\
             exists pc2',type_glob_step x (changepc pc1' t1 O) l fp1 pc2' /\
                    thread_pool pc2' = thread_pool pc2 /\
                    GMem.eq' pc2'.(gm) pc2.(gm).
  Lemma atomblock_open_reorder_corestar:
    forall x l t1 t2 pc pc1 pc2 fp1 fp2,
      @type_glob_step GE x (changepc pc t1 O) l fp1 pc1 ->
      atom_bit pc1 = O ->
      l <> sw ->
      t1 <> t2 ->
      tau_star (type_glob_step core) (changepc pc1 t2 I) fp2 pc2 ->
      FP.smile fp1 fp2 ->
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      exists pc1',tau_star (type_glob_step core) (changepc pc t2 I) fp2 pc1'/\
             exists pc2',type_glob_step x (changepc pc1' t1 O) l fp1 pc2' /\
                    thread_pool pc2' = thread_pool pc2 /\
                    GMem.eq' pc2'.(gm) pc2.(gm).
  
  Lemma taustar_fpconflict_split:
    forall A step pc pc' fp1,
      @tau_star A step pc fp1 pc'->
      forall fp2,
        FP.conflict fp1 fp2 ->
        exists fp10 fp11 pc10 pc11,
          tau_star step pc fp10 pc10 /\
          step pc10 tau fp11 pc11 /\
          FP.smile fp2 fp10 /\ FP.conflict fp2 fp11 /\
          FP.subset fp10 fp1 /\ FP.subset fp11 fp1.
    
    
    


  Lemma changeatombit_corestep_preserve:
    forall pc fp pc',
      (@type_glob_step GE core) pc tau fp pc'->
      type_glob_step core (changepc pc (cur_tid pc) O) tau fp (changepc pc'(cur_tid pc) O).
  Lemma changeatombit_corestar_preserve:
    forall pc fp pc',
      tau_star (@type_glob_step GE core) pc fp pc'->
      tau_star (type_glob_step core) (changepc pc (cur_tid pc) O) fp (changepc pc'(cur_tid pc) O).
  Lemma changeatombitI_corestar_preserve:
    forall pc fp pc',
      tau_star (@type_glob_step GE core) pc fp pc'->
      tau_star (type_glob_step core) (changepc pc (cur_tid pc) I) fp (changepc pc'(cur_tid pc) I).






  Lemma changepc_again:
    forall pc t i t' i',
      changepc (changepc pc t' i') t i = changepc pc t i .
  Lemma mem_eq_pc_changepc:
    forall pc pc' t x,
      mem_eq_pc pc pc'->
      mem_eq_pc (changepc pc t x)(changepc pc' t x).
    

  Lemma corestar_taustar:
    forall pc l fp pc',
      star (@type_glob_step GE core) pc l fp pc'->
      tau_star (type_glob_step core) pc fp pc'.
  Lemma corestep_changebit:
    forall pc l fp pc' x,
      @type_glob_step GE core pc l fp pc'->
      type_glob_step core (changepc pc (cur_tid pc) x) l fp (changepc pc'(cur_tid pc) x).
  Lemma corestar_changebit:
    forall pc l fp pc' x,
      star (@type_glob_step GE core) pc l fp pc'->
      star (@type_glob_step GE core) (changepc pc (cur_tid pc) x) l fp (changepc pc' (cur_tid pc) x).
  Lemma corestepN_changebit:
    forall i pc l fp pc' x,
      stepN (@type_glob_step GE core) i pc l fp pc'->
      stepN (@type_glob_step GE core) i (changepc pc (cur_tid pc) x) l fp (changepc pc' (cur_tid pc) x).


  Lemma half_atom_block_glob_predict_star_alter:
    forall t pc l fp pc',
      half_atom_block ({-|pc,t}) l fp pc'->
      glob_predict_star_alter pc t I fp .


  Definition atomblockN (i:nat)(pc:@ProgConfig GE)(fp:FP.t)(pc':ProgConfig):Prop:=
    exists pc1,type_glob_step entat pc tau FP.emp pc1 /\
          exists pc2,tau_N (type_glob_step core) i pc1 fp pc2 /\
                type_glob_step extat pc2 tau FP.emp pc'.
  Lemma step_equiv_tau_star_equiv:
    forall (step1:@ProgConfig GE->glabel->FP.t-> @ProgConfig GE->Prop) step2,
      (forall fp pc pc',step1 pc tau fp pc' <-> step2 pc tau fp pc')->
      forall fp pc pc',tau_star step1 pc fp pc' <-> tau_star step2 pc fp pc'.
  Lemma corestar_tid_bit_preserve:
    forall pc pc' fp,
      tau_star (@type_glob_step GE core) pc fp pc'->
      cur_tid pc = cur_tid pc' /\
      atom_bit pc = atom_bit pc'.
  Lemma step_memeqpc_preserve:
    forall pc pc' l fp x pc1 pc1',
      @type_glob_step GE x pc l fp pc'->
      @type_glob_step GE x pc1 l fp pc1' ->
      x <> core ->
      x <> glob_sw ->
      mem_eq_pc pc pc1 ->
      mem_eq_pc pc' pc1'.
    
  Lemma atomblock_reorder:
    forall x i l t1 t2 pc pc1 pc2 fp1 fp2,
      @type_glob_step GE x ({-|pc,t1}) l fp1 pc1 ->
      atom_bit pc = atom_bit pc1 ->
      l <> sw ->
      t1 <> t2 ->
      atomblockN i ({-|pc1,t2}) fp2 pc2 ->
      FP.smile fp1 fp2 ->
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      exists pc',atomblockN i ({-|pc,t2}) fp2 pc' /\ exists pc'',type_glob_step x ({-|pc',t1}) l fp1 pc'' /\ mem_eq_pc pc2 ({-|pc'',cur_tid pc2}).

  Lemma List_i_split:
    forall (A:Type)(i:nat)(l:list A)(p:A),
      List.nth_error l i = Some p->
      exists l1 l2,
        l=app l1 (cons p l2) /\ length l1 = i .
           

End Reorder.


Section PRaceLemmas.
  Variable GE:GlobEnv.t.
  Definition invpc (pc:@ProgConfig GE):Prop:=ThreadPool.inv pc.(thread_pool).
  Definition cur_valid_id (pc:@ProgConfig GE):=pc_valid_tid pc pc.(cur_tid).
  Lemma pc_cur_tid :
    forall pc:@ProgConfig GE,
      ({-|pc,cur_tid pc}) = pc.
  Lemma cur_valid_id_sw:
    forall pc,atom_bit pc = O->cur_valid_id pc->
         forall t,type_glob_step glob_sw ({-|pc,t}) sw FP.emp pc.
  Lemma cur_valid_id_nohalt:
    forall pc,
      invpc pc ->
      cur_valid_id pc->
      forall pc' l fp,
        ~ type_glob_step glob_halt pc' l fp pc.
  Lemma npnsw_step_cur_valid_id:
    forall pc l fp pc',
      glob_npnsw_step pc l fp pc'->
      invpc pc ->
      cur_valid_id pc.
  Lemma npnsw_star_fpnotemp_cur_valid_id:
    forall pc fp pc',
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool) ->
      tau_star (@glob_npnsw_step GE) pc fp pc' ->
      fp<> FP.emp ->
      cur_valid_id pc.
 Lemma glob_predict_fpnotemp_validtid:
    forall pc b t fp,
      glob_predict pc t b fp ->
      ThreadPool.inv pc.(thread_pool)->
      fp<>FP.emp ->
      @pc_valid_tid GE pc t.
  Lemma GE_mod_wd_star_tp_inv2:
    forall GE pc l fp pc',
      GlobEnv.wd GE ->
      @ThreadPool.inv GE (thread_pool pc) ->
      star glob_step pc l fp pc' -> ThreadPool.inv (thread_pool pc').
  Lemma GE_mod_wd_npstar_tp_inv:
    forall pc l fp pc',
      star (@np_step GE) pc l fp pc' ->
      GlobEnv.wd GE ->
      ThreadPool.inv pc.(thread_pool) ->
      ThreadPool.inv pc'.(thread_pool).
  Lemma lang_wd_mod_wd:
    forall NL L p gm ge pc t,
      wd_langs (fst p)->
      @init_config NL L p gm ge pc t->
      forall ix,mod_wd (GlobEnv.modules ge ix).

  Lemma npnswstep_cur_valid_tid:
    forall pc l fp pc',
      invpc pc->
      @glob_npnsw_step GE pc l fp pc'->
      cur_valid_id pc.

  Lemma glob_tau_no_atom_type:
    forall x pc fp pc',
      @type_glob_step GE x pc tau fp pc'->
      atom_bit pc' = atom_bit pc ->
      x = glob_halt \/ x = core \/ x = call \/ x = ret.
  
  Lemma npnswstep_taustep:
    forall pc l fp pc',@glob_npnsw_step GE pc l fp pc'->l = tau.
  Lemma npnswstep_l1:
    forall pc l fp pc',@glob_npnsw_step GE pc l fp pc'->exists i,type_glob_step i pc l fp pc' /\ (i=core \/ i=call \/ i = ret).
  Lemma npnswstep_l3:
    forall pc l fp pc' i,@type_glob_step GE i pc l fp pc'->(i=core\/i=call\/i=ret)->glob_npnsw_step pc l fp pc'.
  Lemma npnswstep_l2:
    forall pc l fp pc',@glob_npnsw_step GE pc l fp pc'->atom_bit pc = atom_bit pc'.
  Lemma npnswstar_bit:
    forall pc fp pc',tau_star (@glob_npnsw_step GE) pc fp pc'->atom_bit pc = atom_bit pc'.
  Lemma core_tau_star_star:
    forall ge pc fp pc',
      tau_star (@type_glob_step ge core) pc fp pc'->
      exists l,star glob_step pc l fp pc'.
  Lemma core_tau_star_tau_star:
    forall ge pc fp pc',
      tau_star (@type_glob_step ge core) pc fp pc'->
      tau_star glob_step pc fp pc'.

  Lemma predict_step_ex:
    forall x y pc t1 t2 l1 fp1 pc1 l2 fp2 pc2,
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      (forall ix,mod_wd (GlobEnv.modules GE ix))->
      @type_glob_step GE x ({-|pc,t1}) l1 fp1 pc1 ->
      type_glob_step y ({-|pc,t2}) l2 fp2 pc2->
      FP.smile fp1 fp2 ->
      x=core\/x=call\/x=ret -> l2 <> sw ->
      t2 <> t1->
      exists pc',type_glob_step y ({-|pc1,t2}) l2 fp2 pc'.

  Lemma predict_step_ex_alt:
    forall x pc t1 t2 fp1 pc1 pc2,
      GlobEnv.wd GE->
      ThreadPool.inv pc.(thread_pool)->
      (forall ix,mod_wd (GlobEnv.modules GE ix))->
      @type_glob_step GE x (changepc GE pc t1 O) tau fp1 pc1 ->
      type_glob_step extat ({-|pc,t2}) tau FP.emp pc2->
      x=core\/x=call\/x=ret ->
      t2 <> t1->
      exists pc', type_glob_step extat (changepc GE pc1 t2 I) tau FP.emp pc'.
    
    
   Lemma npnswstep_changebitO:
    forall pc l fp pc',
      glob_npnsw_step pc l fp pc'->
      glob_npnsw_step (changepc GE pc (cur_tid pc) O) l fp (changepc GE pc'(cur_tid pc) O).

   Lemma tauN_I_split:
    forall i pc fp pc',
      tau_N (@glob_step GE) i pc fp pc'->
      atom_bit pc = I->
      (tau_N (type_glob_step core) i pc fp pc') \/
      (exists pc1 j fp1 pc2 fp2 k,
          tau_N (type_glob_step core) j pc fp1 pc1 /\
          type_glob_step extat pc1 tau FP.emp pc2 /\
          tau_N glob_step k pc2 fp2 pc' /\
          FP.union fp1 fp2 = fp /\ j+k+1=i).
  Lemma coretauN_globtauN:
    forall i pc fp pc',
      tau_N (@type_glob_step GE core) i pc fp pc'->
      tau_N glob_step i pc fp pc'.
  Lemma thdp_inv_npstar:
    forall pc l fp pc',
      GlobEnv.wd GE->
      star (@np_step GE) pc l fp pc'->
      ThreadPool.inv pc.(thread_pool) ->
      ThreadPool.inv pc'.(thread_pool).

    Lemma init_property_1:
    forall NL L p gm ge pc t,
      @init_config NL L p gm ge pc t->
      ThreadPool.valid_tid pc.(thread_pool) t.

  
  Lemma config_thdp_init_property1:
    forall NL L p gm pc t,
      @init_config NL L p gm GE pc t->
      forall i,
        ThreadPool.valid_tid pc.(thread_pool) i->
        ~ThreadPool.halted pc.(thread_pool) i.


  Corollary init_property_1_alt :
    forall NL L p gm pc t,
      @init_config NL L p gm GE pc t->
      pc_valid_tid pc t.
    


  Lemma thdp_inv_race_config_equiv:
    forall pc,
      ThreadPool.inv pc.(thread_pool) ->
      race_config pc -> @np_race_config_base GE pc.

End PRaceLemmas.
  



Section Race_Proof.
  Lemma np_race_config_base_case0_star_race:
    forall ge (pc:@ProgConfig ge) id1 id2 fp1 fp2 pc1 pc2,
      (forall ix : fintype.ordinal (GlobEnv.M ge), mod_wd (GlobEnv.modules ge ix)) ->
      GlobEnv.wd ge ->
      ThreadPool.inv pc.(thread_pool)->
      atom_bit pc = O ->
      GSimDefs.pc_valid_tid pc id1 ->
      GSimDefs.pc_valid_tid pc id2 ->
      id1 <> id2 ->
      tau_star np_step ({-|pc, id1}) fp1 pc1->
      atom_bit pc = atom_bit pc1 ->
      tau_star np_step ({-|pc, id2}) fp2 pc2 ->
      atom_bit pc = atom_bit pc2 ->
      FP.conflict fp1 fp2 ->
    
      star_race glob_predict pc.
  Lemma np_race_config_base_star_race:
    forall ge (pc:@ProgConfig ge),
      (forall ix : fintype.ordinal (GlobEnv.M ge), mod_wd (GlobEnv.modules ge ix)) ->
      GlobEnv.wd ge ->
      np_race_config_base pc -> atom_bit pc = O ->
      ThreadPool.inv pc.(thread_pool)->
      star_race glob_predict pc.

  Lemma NPRace_Race_Config:
    forall NL L p gm ge pc t
    (H1:True),
    @wd_langs NL L (fst p) ->
    init_config p gm ge pc t->
    np_race_config pc \/ np_star_race_config pc->
    star_race_config pc.
  Lemma NPRace_Race:
    forall NL L p,
      @wd_langs NL L (fst p)->
      np_race_prog p ->
      race_prog p.

  
End Race_Proof.