Module RefineEquiv

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

Require Import DRF USimDRF NPDRF.

Require Import Classical Wf Arith ListDom.

Require Import FPLemmas PRaceLemmas Init SmileReorder ConflictReorder Init DRFLemmas SimEtr.
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).

Section Refinement.
  Hypothesis init_free:
    forall NL (L:@langs NL)(p:prog L) gm ge pc t,
      init_config p gm ge pc pc.(cur_tid) ->
      pc_valid_tid pc t->
      init_config p gm ge ({-|pc,t}) t.
  Definition p_np_config_refine {ge:GlobEnv.t}(s:@ProgConfig ge):Prop:=
    forall B,Etr np_step np_abort final_state s B->
        Etr glob_step abort final_state s B.

  Definition p_np_prog_refine {NL:nat}{L:@langs NL}(P:@prog NL L):Prop:=
    forall gm ge pc,
      init_config P gm ge pc pc.(cur_tid) ->
      p_np_config_refine pc.
  Definition np_p_config_refine_weak {ge:GlobEnv.t}(s:@ProgConfig ge):Prop:=
    forall B, Etr glob_step abort final_state s B->
         exists t,Etr np_step np_abort final_state ({-|s,t}) B /\ pc_valid_tid s t.
  
  Definition np_p_prog_refine_weak {NL:nat}{L:@langs NL}(P:@prog NL L):Prop:=
    forall gm ge pc,
      init_config P gm ge pc pc.(cur_tid)->
      np_p_config_refine_weak pc.
  Lemma threadpool_spawn_domadd:
    forall ge t mid c sg ,
      let t' := @ThreadPool.spawn ge t mid c sg in
      ThreadPool.next_tid t' = BinPos.Psucc (ThreadPool.next_tid t).
  Lemma threadpool_init_domeq:
    forall e ge1 ge2 t1 t2,
      @ThreadPool.init ge1 e t1->
      @ThreadPool.init ge2 e t2->
      t1.(ThreadPool.next_tid) = t2.(ThreadPool.next_tid).
  Lemma threadpool_init_domeq':
    forall e ge1 ge2 t1 t2,
      @ThreadPool.init ge1 e t1->
      @ThreadPool.init ge2 e t2->
      (forall t,ThreadPool.valid_tid t1 t<->ThreadPool.valid_tid t2 t).
  Lemma switchable_glob_config_refine:
    forall ge pc t,
      @pc_valid_tid ge pc pc.(cur_tid)->
      atom_bit pc = O ->
      forall B,
        Etr glob_step abort final_state pc B->
        Etr glob_step abort final_state ({-|pc,t}) B.

    
  Lemma Etr_cons_globsw:
    forall ge pc pc',
      @glob_step ge pc sw FP.emp pc'->
      forall B,
        Etr glob_step abort final_state pc' B->
        Etr glob_step abort final_state pc B.
    
    
    
  Lemma init_pair_valid_tid:
    forall NL L sc tc e sgm sge spc tgm tge tpc i i',
      @init_config NL L (sc,e) sgm sge spc i->
      @init_config NL L (tc,e) tgm tge tpc i'->
      forall j,
        pc_valid_tid spc j-> pc_valid_tid tpc j.
  Lemma P_NP_Refine_adjusted:
    forall NL L scus tcus e,
      @np_prog_refine NL L (scus,e)(tcus,e)->
      np_p_prog_refine_weak (tcus,e)->
      p_np_prog_refine (scus,e)->
      prog_refine (scus,e)(tcus,e).
    
    
  Lemma tau_np_p:
    forall ge pc fp pc',
      @np_step ge pc tau fp pc'->
      glob_step pc tau fp pc'.
  Lemma sw_np_p:
    forall ge pc fp pc',
      @np_step ge pc sw fp pc'->
          exists pc'',
            glob_step pc tau fp pc'' /\ glob_step pc'' sw FP.emp pc'.
  Lemma non_evt_star_equiv:
    forall ge pc fp state',
      non_evt_star (@np_step ge) pc fp state'->
      non_evt_star glob_step pc fp state'.
  Inductive non_evt_starN {State:Type}:(State->glabel->FP.t->State->Prop)->nat->State->FP.t->State->Prop:=
  | ne_star_refl: forall step s,
      @non_evt_starN State step 0 s FP.emp s
  | ne_star_step: forall step n s1 fp1 s2 fp2 s3,
      step s1 tau fp1 s2 \/ step s1 sw fp1 s2 ->
      @non_evt_starN State step n s2 fp2 s3 ->
      non_evt_starN step (S n)s1 (FP.union fp1 fp2) s3.
  Lemma non_evt_star_N_equiv{State:Type}:
    forall step s fp s',
      @non_evt_star State step s fp s' <-> exists n,non_evt_starN step n s fp s'.

  Lemma mem_eq_non_evt_starN:
    forall ge pc pc',
      (forall ix,mod_wd (GlobEnv.modules ge ix))->
      mem_eq_pc ge pc pc'->
      forall i fp pc2,
        non_evt_starN glob_step i pc fp pc2->
        exists pc'',non_evt_starN glob_step i pc' fp pc'' /\ mem_eq_pc ge pc2 pc''.
  Lemma non_evt_star_Sn_split{State:Type}:
    forall step n s fp s',
      @non_evt_starN State step (S n) s fp s'->
      exists fp1 fp2 s1,
        non_evt_starN step n s fp1 s1 /\
        (step s1 tau fp2 s' \/ step s1 sw fp2 s') /\
        FP.union fp1 fp2 = fp.

  Lemma non_evt_star_thdp_inv:
    forall ge pc fp pc',
      GlobEnv.wd ge->
      ThreadPool.inv pc.(thread_pool)->
      non_evt_star (@np_step ge) pc fp pc'->
      ThreadPool.inv pc'.(thread_pool).

  Lemma no_npstep_no_globstep:
    forall ge pc,
      ThreadPool.inv pc.(thread_pool)->
      (forall l fp pc',~ @np_step ge pc l fp pc')->
      (forall l' fp' pc'',glob_step pc l' fp' pc''->l'=sw).

  
                                 
  Lemma init_abort_np_p:
    forall NL L P gm ge pc t,
      @init_config NL L P gm ge pc t->
      np_abort pc->
      abort pc.
    
    
  Definition np_accepted {ge}(pc:@ProgConfig ge):Prop:=
    exists NL L P gm pc0,
      @init_config NL L P gm ge pc0 pc0.(cur_tid) /\
      exists l fp,
        star np_step pc0 l fp pc.
  Lemma np_accepted_inv_thdp:
    forall ge pc,
      @np_accepted ge pc->
      ThreadPool.inv pc.(thread_pool).
  Fixpoint add(l:list glabel)(l':glabel):list glabel:=
    match l with
    | nil => cons l' nil
    | cons x y => cons x (add y l')
    end.
  Lemma star_npstep_inv:
    forall ge pc l fp pc',
      star (@np_step ge) pc l fp pc'->
      (pc = pc' /\ l = nil /\ fp=FP.emp) \/
      (exists pc'' l' fp' l'' fp'',star np_step pc l' fp' pc'' /\ np_step pc'' l'' fp'' pc' /\ l = add l' l'' /\ fp = FP.union fp' fp'').
  Lemma star_abort_np_p:
    forall ge pc,
      @np_accepted ge pc->
      np_abort pc->
      abort pc.
  Lemma sw_diverge:
    forall State step s s',
      @silent_diverge State step s'->
      step s sw FP.emp s'->
      silent_diverge step s.

  Inductive lstep{ge}:@Step ge->@Step ge:=
  | build:
      forall step s0 s1 fp s2,
        sw_star step s0 s1->
        step s1 tau fp s2 ->
        lstep step s0 tau fp s2.

  Lemma sw_star_lstep_lemma{ge}: forall (step:@Step ge) s s',sw_star (lstep step) s s'-> s=s'.
  Inductive tau_plus'{ge}:@Step ge->@Step ge:=
  | plus'_1:
      forall (step:Step ge) s fp s',
        step s tau fp s'->
        tau_plus' step s tau fp s'
  | plus'_cons:
      forall (step:Step ge) s fp s' fp' s'',
        step s tau fp s'->
        tau_plus' step s' tau fp' s''->
        tau_plus' step s tau (FP.union fp fp') s''.
  Lemma sw_star_tau_plus'_lemma{ge}: forall (step:@Step ge) s s',sw_star (tau_plus' step) s s'-> s=s'.
  Lemma silent_diverge_lstep_equiv{ge}:
    forall (step:@Step ge) s,
      silent_diverge step s<->silent_diverge (lstep step) s.
  Lemma sw_lstep_cons{ge}:
    forall (step:@Step ge) s s' fp s'',
      step s sw FP.emp s'->
      lstep step s' tau fp s''->
      lstep step s tau fp s''.
  Lemma lnpstep_taupluslglobstep{ge}:
    forall s fp s',
      lstep (@np_step ge) s tau fp s'->
      tau_plus' (lstep glob_step) s tau fp s'.
    
  Lemma silent_diverge_lstep_npstep_tauplus_lstep_pstep{ge}:
    forall s,
      silent_diverge (lstep (@np_step ge)) s->silent_diverge (tau_plus'(lstep glob_step)) s.


  Lemma tauplus'_diverge_inv{ge}:
  forall (step:@Step ge) s,
    silent_diverge (tau_plus' step) s ->
    exists s' fp, step s tau fp s' /\ silent_diverge (tau_plus' step) s'.
  
  Lemma tau_plus'_diverge_lemma{ge}:
    forall (step:@Step ge) s,
      silent_diverge (tau_plus' step) s->silent_diverge step s.
  Lemma silent_diverge_np_p{ge}:
    forall pc,
      silent_diverge (@np_step ge) pc -> silent_diverge glob_step pc.

  Lemma Etr_p_sw{ge}:
    forall pc B t,
      Etr (@glob_step ge) abort final_state pc B->
      glob_step ({-|pc,t}) sw FP.emp pc ->
      Etr glob_step abort final_state ({-|pc,t}) B.


  Lemma np_evtstep_inv:
    forall ge pc v pc',
      @np_step ge pc (evt v) FP.emp pc'->
      glob_step pc (evt v) FP.emp ({-|pc',cur_tid pc}) /\
      glob_step ({-|pc',cur_tid pc}) sw FP.emp pc'.
  Lemma np_accepted_add_step:
    forall ge pc l fp pc',
      @np_accepted ge pc->
      np_step pc l fp pc'->
      np_accepted pc'.
  Lemma np_accepted_add_star:
    forall ge pc l fp pc',
      @np_accepted ge pc->
      star np_step pc l fp pc'->
      np_accepted pc'.
  Lemma Etr_np_p_done:
    forall ge pc,
      Etr (@np_step ge) np_abort final_state pc Behav_done->
      Etr glob_step abort final_state pc Behav_done.
  Lemma Etr_np_p_diverge:
    forall ge pc,
      Etr (@np_step ge) np_abort final_state pc Behav_diverge->
      Etr glob_step abort final_state pc Behav_diverge.
  Lemma Etr_np_p_abort:
    forall ge pc,
      @np_accepted ge pc->
      Etr (@np_step ge) np_abort final_state pc Behav_abort->
      Etr glob_step abort final_state pc Behav_abort.
  Lemma Etr_np_cons_inv:
    forall ge pc v b,
      np_accepted pc->
      Etr (@np_step ge) np_abort final_state pc (Behav_cons v b)->
      exists fp pc' pc'',non_evt_star np_step pc fp pc'/\np_step pc' (evt v) FP.emp pc'' /\ Etr np_step np_abort final_state pc'' b /\ np_accepted pc''.
  Inductive limited_etr {ge}:nat->@Step ge->(@ProgConfig ge->Prop)->(@ProgConfig ge->Prop)-> @ProgConfig ge->behav->Prop:=
  | done_0: forall step abort final pc,
      Etr step abort final pc Behav_done->
      limited_etr 0 step abort final pc Behav_done
  | abort_0: forall step abort final pc,
      Etr step abort final pc Behav_abort->
      limited_etr 0 step abort final pc Behav_abort
  | diverge_0: forall step abort final pc,
      Etr step abort final pc Behav_diverge->
      limited_etr 0 step abort final pc Behav_diverge
  | cons': forall step abort final pc fp pc' pc'' v i b,
      limited_etr i step abort final pc'' b->
      non_evt_star step pc fp pc'->
      step pc' (evt v) FP.emp pc'' ->
      limited_etr (S i) step abort final pc (Behav_cons v b).
                   
  Lemma limited_etr_npetr:
    forall ge i pc b,
      @limited_etr ge i np_step np_abort final_state pc b->
      Etr np_step np_abort final_state pc b.

  Lemma Etr_np_p_limited:
    forall ge i pc b,
      @np_accepted ge pc->
      limited_etr i np_step np_abort final_state pc b->
      Etr glob_step abort final_state pc b.

  CoInductive inf_etr {ge}(step:@Step ge)(abort final:@ProgConfig ge->Prop):@ProgConfig ge->behav->Prop:=
  | build_infetr:
      forall pc fp pc' v pc'' b,
        inf_etr step abort final pc'' b->
        non_evt_star step pc fp pc'->
        step pc' (evt v) FP.emp pc'' ->
        inf_etr step abort final pc (Behav_cons v b).
  Definition inf_etr_alt {ge}(step:@Step ge)(abort final:@ProgConfig ge->Prop)(pc:@ProgConfig ge)(b:behav):Prop:=
    Etr step abort final pc b /\ ~ exists i,limited_etr i step abort final pc b.

  Lemma inf_etr_alt_inv:
    forall ge step abort final pc b,
      @inf_etr_alt ge step abort final pc b->
      exists fp pc' pc'' v b',
        b = Behav_cons v b' /\
        non_evt_star step pc fp pc' /\
        step pc' (evt v) FP.emp pc'' /\
        inf_etr_alt step abort final pc'' b'.

  Lemma inf_etr_alt_sound:
    forall ge step abort final pc b,
      @inf_etr_alt ge step abort final pc b->
      inf_etr step abort final pc b.
    
  CoInductive inf_etr_alt2 {ge}(step:@Step ge)(abort final:@ProgConfig ge->Prop):@ProgConfig ge->behav->Prop:=
  | build_infetr':
      forall pc fp pc' v pc'' pc''' b,
        inf_etr_alt2 step abort final pc''' b->
        non_evt_star step pc fp pc'->
        step pc' (evt v) FP.emp pc'' ->
        step pc'' sw FP.emp pc''' ->
        inf_etr_alt2 step abort final pc (Behav_cons v b).
  
  Lemma sw_step_non_evt_star:
    forall ge (step:@Step ge) s s',
      step s sw FP.emp s'->
      non_evt_star step s FP.emp s'.
  Lemma non_evt_star_cons_inf_etr_alt2:
    forall ge (step:@Step ge) s fp s' b abort final,
      non_evt_star step s fp s'->
      inf_etr_alt2 step abort final s' b->
      inf_etr_alt2 step abort final s b.

  Lemma inf_etr_alt2_p:
    forall ge a f pc b,
      GlobEnv.wd ge->
      invpc ge pc->
      inf_etr glob_step a f pc b->
      @inf_etr_alt2 ge glob_step a f pc b.
    
    
  Lemma inf_etr_alt2_sound:
    forall ge step abort final pc b,
      @inf_etr_alt2 ge step abort final pc b->
      inf_etr step abort final pc b.

  Lemma np_inf_etr_glob_inf_etr_alt2:
    forall ge pc b,
      @inf_etr ge np_step np_abort final_state pc b->
      inf_etr_alt2 glob_step abort final_state pc b.

  Lemma inf_etr_np_p:
    forall ge pc b,
      @inf_etr ge np_step np_abort final_state pc b->
      inf_etr glob_step abort final_state pc b.

  Lemma inf_etr_etr:
    forall ge step abort final pc b,
      @inf_etr ge step abort final pc b->
      Etr step abort final pc b.

  
  Lemma Etr_np_p:
    forall ge pc b,
      @np_accepted ge pc->
      Etr np_step np_abort final_state pc b->
      Etr glob_step abort final_state pc b.

  Lemma p_np_refine{NL}{L}:
    forall P,@p_np_prog_refine NL L P.

  Definition drf_pc{ge:GlobEnv.t} (pc:@ProgConfig ge):=
    exists NL L p gm, drfpc pc /\ @init_config NL L p gm ge pc pc.(cur_tid) /\ wd_langs (fst p) /\ safe_state glob_step abort pc.

  Definition drf_pc_glob {ge}(pc:@ProgConfig ge):=
    atom_bit pc = O /\
    exists pc0 l fp,drf_pc pc0 /\ star glob_step pc0 l fp pc.
  Lemma drf_pc_glob_cons:
    forall ge pc l fp pc',
      @drf_pc_glob ge pc->
      star glob_step pc l fp pc'->
      atom_bit pc' = O ->
      drf_pc_glob pc'.


  Lemma drf_pc_glob_l1:
    forall ge pc,
      @drf_pc_glob ge pc->
      ThreadPool.inv pc.(thread_pool)/\
      GlobEnv.wd ge.
  Lemma drf_pc_glob_l2:
    forall ge pc,
      @drf_pc_glob ge pc->
      (forall ix,
        mod_wd (GlobEnv.modules ge ix)).

  Lemma stepN_SN_split_weak:
    forall i ge pc l fp pc',
      stepN ge glob_step (S i) pc l fp pc'->
      exists l1 fp1 pc1,stepN ge glob_step i pc l1 fp1 pc1 /\
                   exists l2 fp2,glob_step pc1 l2 fp2 pc'.

  Lemma valid_tid_preserve':
    forall ge pc l fp pc',
      GlobEnv.wd ge->
      ThreadPool.inv pc.(thread_pool)->
      @glob_step ge pc l fp pc'->
      ThreadPool.valid_tid pc'.(thread_pool) pc'.(cur_tid) \/ ThreadPool.halted pc'.(thread_pool) pc'.(cur_tid).

  Lemma pc_glob_l3:
    forall NL L p gm ge pc0 pc l fp,
      @init_config NL L p gm ge pc0 pc0.(cur_tid)->
      star glob_step pc0 l fp pc->
      ThreadPool.valid_tid pc.(thread_pool) pc.(cur_tid)\/
      ThreadPool.halted pc.(thread_pool) pc.(cur_tid).

  Definition non_evt_thrd_globstar (ge:GlobEnv.t)(pc:@ProgConfig ge)(fp:FP.t)(pc':@ProgConfig ge):Prop:=
    exists i l fp1 pc1,
      atomblockstarN ge i l pc fp1 pc1 /\
      exists fp2,
        tau_star glob_npnsw_step pc1 fp2 pc' /\
        FP.union fp1 fp2 = fp.

   Lemma atomblockstep_star:
    forall ge pc fp pc' l0,
      atomblockstep ge pc l0 fp pc'->
      exists l,star glob_step pc l fp pc'.
  Lemma swstar_star:
    forall ge pc pc',
      sw_star (@glob_step ge) pc pc'->
      exists l,star glob_step pc l FP.emp pc'.
  Lemma atomblockstarN_star:
    forall ge i l pc fp pc',
      atomblockstarN ge i l pc fp pc'->
      exists l',star glob_step pc l' fp pc'.
  Lemma non_evt_thrd_globstar_star:
    forall ge pc fp pc',
      @non_evt_thrd_globstar ge pc fp pc'->
      exists l,star glob_step pc l fp pc'.

    
  Lemma pc_valid_tid_nonevtstar_cons_evtstep:
    forall ge pc fp pc' v pc'',
      drf_pc_glob pc->
      non_evt_star (@glob_step ge) pc fp pc'->
      glob_step pc' (evt v) FP.emp pc''->
      pc_valid_tid pc (cur_tid pc'').

  Definition drf_pc_glob_weak (ge:GlobEnv.t)(pc:@ProgConfig ge):=
    exists p l fp,drf_pc p /\ star glob_step p l fp pc.
  Lemma drf_pc_glob_weaken:
    forall ge pc,
      drf_pc_glob pc->
      drf_pc_glob_weak ge pc.
  Lemma drf_pc_glob_strengthen:
    forall ge pc,
      drf_pc_glob_weak ge pc ->
      atom_bit pc = O->
      drf_pc_glob pc.

  Lemma non_evt_star_IO:
    forall ge pc fp pc',
      non_evt_star (@glob_step ge) pc fp pc'->
      atom_bit pc = I->
      atom_bit pc' = O->
      exists fp1 pc1,tau_star (type_glob_step core) pc fp1 pc1 /\
                exists pc2,type_glob_step extat pc1 tau FP.emp pc2 /\
                      exists fp2,non_evt_star glob_step pc2 fp2 pc' /\
                             FP.union fp1 fp2 = fp.
  Lemma non_evt_starN_IO:
    forall ge i pc fp pc',
      non_evt_starN (@glob_step ge) i pc fp pc'->
      atom_bit pc = I->
      atom_bit pc' = O->
      exists j fp1 pc1,tau_N (type_glob_step core) j pc fp1 pc1 /\ j <= i /\
                exists pc2,type_glob_step extat pc1 tau FP.emp pc2 /\
                      exists fp2,non_evt_starN glob_step (i-j-1) pc2 fp2 pc' /\
                             FP.union fp1 fp2 = fp.
  Lemma tau_star_IO:
    forall ge pc fp pc',
      tau_star (@glob_step ge) pc fp pc'->
      atom_bit pc = I->atom_bit pc' = O->
      exists fp1 pc1,tau_star (type_glob_step core) pc fp1 pc1/\
                exists pc2,type_glob_step extat pc1 tau FP.emp pc2/\
                      exists fp2,tau_star glob_step pc2 fp2 pc'/\
                            FP.union fp1 fp2= fp.

  Lemma tau_N_IO:
    forall i ge pc fp pc',
      tau_N (@glob_step ge) i pc fp pc'->
      atom_bit pc = I->atom_bit pc' = O->
      exists j fp1 pc1,tau_N (type_glob_step core) j pc fp1 pc1/\ j < i /\
                exists pc2,type_glob_step extat pc1 tau FP.emp pc2/\
                      exists fp2,tau_N glob_step (i-j-1) pc2 fp2 pc'/\
                            FP.union fp1 fp2= fp.

  Lemma drf_pc_glob_stepfpsmile:
    forall ge pc fp pc' t fp' pc'',
      @drf_pc_glob ge pc->
      glob_step pc tau fp pc'->
      t <> cur_tid pc->
      glob_step ({-|pc',t}) tau fp' pc''->
      FP.smile fp fp'.

  Lemma type_glob_step_atomOpreserve:
    forall ge i pc l fp pce,
      @type_glob_step ge i pc l fp pce->
      atom_bit pce = atom_bit pc->
      forall GE pc' l' fp' pc'',
        @type_glob_step GE i pc' l' fp' pc''->
        atom_bit pc'' = atom_bit pc'.

  Lemma tid_change_bit_eq:forall ge (pc:@ProgConfig ge) t, atom_bit ({-|pc,t}) = atom_bit pc.

  Lemma drf_pc_glob_taustep_ex:
    forall ge pc fp pc' t fp' pc'',
      drf_pc_glob pc->
      glob_step pc tau fp pc'->
      t <> cur_tid pc->
      glob_step ({-|pc',t}) tau fp' pc''->
      atom_bit pc' = O ->
      atom_bit pc'' = O->
      exists pc1,glob_step ({-|pc,t}) tau fp' pc1/\ atom_bit pc1 = O /\
            exists pc2,glob_step ({-|pc1,cur_tid pc}) tau fp pc2 /\
                  mem_eq_pc ge pc'' ({-|pc2,t}) /\
                  drf_pc_glob pc2.


  Lemma drf_pc_glob_taustep_halfatomblock_fpsmile:
    forall ge pc fp pc' t pc1 fp2 pc2,
      @drf_pc_glob ge pc->
      glob_step pc tau fp pc'->
      t <> cur_tid pc->
      type_glob_step entat ({-|pc',t}) tau FP.emp pc1 ->
      tau_star (type_glob_step core) pc1 fp2 pc2->
      FP.smile fp fp2.


  Lemma drf_pc_glob_taustep_atomblock_ex:
    forall ge pc fp pc' t pc1 i fp2 pc2 pc3,
      @drf_pc_glob ge pc->
      glob_step pc tau fp pc'->
      atom_bit pc' = O->
      t <> cur_tid pc->
      type_glob_step entat ({-|pc',t}) tau FP.emp pc1->
      tau_N (type_glob_step core) i pc1 fp2 pc2->
      type_glob_step extat pc2 tau FP.emp pc3->
      exists pc1',
        type_glob_step entat ({-|pc,t}) tau FP.emp pc1'/\
        exists pc2',
          tau_N (type_glob_step core) i pc1' fp2 pc2'/\
          exists pc3',
            type_glob_step extat pc2' tau FP.emp pc3'/\
            exists pc4',
              glob_step ({-|pc3',cur_tid pc}) tau fp pc4' /\
              mem_eq_pc ge pc3 ({-|pc4',cur_tid pc3}) /\
              drf_pc_glob pc3'.


  Lemma drf_pc_glob_taustep_taustar_ex:
    forall x ge pc fp pc' t fp2 pc'',
      @drf_pc_glob ge pc->
      glob_step pc tau fp pc'->
      atom_bit pc' = O ->
      tau_N glob_step x ({-|pc',t}) fp2 pc''->
      atom_bit pc'' = O->
      t <> cur_tid pc->
      exists pc1,
        tau_N glob_step x ({-|pc,t}) fp2 pc1 /\
        atom_bit pc1 = O /\
        exists pc2,
          glob_step ({-|pc1,cur_tid pc}) tau fp pc2 /\
          atom_bit pc2 = O /\
          mem_eq_pc ge pc'' ({-|pc2,t})/\
          drf_pc_glob pc2.

  Lemma globstep_conflict_corestep:
    forall ge pc l fp pc' fp'',
      @glob_step ge pc l fp pc'->
      FP.conflict fp fp''->
      type_glob_step core pc tau fp pc'.
      
  Lemma drf_pc_l4:
    forall ge pc,
      @drf_pc_glob ge pc->
      forall l fp pc',
        star glob_step pc l fp pc'->
        race glob_predict_star_alter pc'->
        False.



  Lemma predicted_abort1_star_abort:
    forall ge pc,
      predicted_abort1 ge pc ->
      exists l fp pc',
        star glob_step pc l fp pc'/\
        abort pc'.
  Lemma swstar_globstar:
    forall ge pc pc',
      sw_star (@glob_step ge) pc pc'->
      exists l fp, star glob_step pc l fp pc'.
  Lemma drf_pc_non_evt_star_evt_step_inv:
    forall ge pc fp pc' pc'' v,
      drf_pc_glob pc ->
      non_evt_star glob_step pc fp pc'->
      glob_step pc' (evt v) FP.emp pc'' ->
      exists t,
        pc_valid_tid pc t /\
        exists fp1 pc1,non_evt_thrd_globstar ge ({-|pc,t}) fp1 pc1 /\ cur_tid pc1 = cur_tid pc' /\
                exists pc2, glob_step pc1 (evt v) FP.emp pc2 /\
                       exists fp2 pc3, non_evt_star glob_step pc2 fp2 pc3 /\
                                  mem_eq_pc ge pc'' pc3.
  
  Lemma non_evt_thrd_globstar_np_nonevt_star:
    forall ge pc fp pc',
      (forall ix,mod_wd (GlobEnv.modules ge ix))->
      non_evt_thrd_globstar ge pc fp pc'->
      pc_valid_tid pc' (cur_tid pc')->
      ThreadPool.inv pc.(thread_pool)->
      GlobEnv.wd ge->
      non_evt_star np_step pc fp pc'.
  

  Lemma final_state_step:
    forall ge x pc l fp pc',
      invpc ge pc' ->
      @type_glob_step ge x pc l fp pc'->
      final_state pc'->
      x = glob_halt.

  Lemma final_state_npnsw_or_sw_star:
    forall ge pc fp pc',
      invpc ge pc->GlobEnv.wd ge->
      npnsw_or_sw_star ge pc fp pc'->
      final_state pc'->
      pc = pc' /\ fp = FP.emp.

  Lemma final_state_atom:
    forall ge pc l fp pc',
      GlobEnv.wd ge ->@invpc ge pc-> atom_bit pc = O->
      star glob_step pc l fp pc'->
      @final_state ge pc'->
      atom_bit pc' = O.

  Lemma non_evt_star_done_inv:
    forall ge pc,
      @drf_pc_glob ge pc->
      forall fp pc',
        non_evt_star glob_step pc fp pc'->
        final_state pc'->
        final_state pc \/
        (exists pc1,
            sw_star glob_step pc pc1 /\
            exists i l fp1 pc2,
              atomblockstarN ge i l pc1 fp1 pc2 /\ mem_eq_pc ge pc' ({-|pc2,cur_tid pc'})).
  
  Lemma Etr_p_np_done:
    forall ge pc,
      drf_pc_glob pc ->
      Etr (@glob_step ge) abort final_state pc Behav_done->
      Etr np_step np_abort final_state pc Behav_done \/
      exists t,Etr np_step np_abort final_state ({-|pc,t}) Behav_done /\ pc_valid_tid pc t .
    
  Lemma np_p_abort_equiv:
    forall NL L p gm ge pc0 l fp pc,
      @init_config NL L p gm ge pc0 pc0.(cur_tid) /\ star glob_step pc0 l fp pc ->
      @abort ge pc->
      np_abort pc.

  Lemma npnsw_abort_preserve:
    forall ge pc l fp pc',
      @drf_pc_glob ge pc ->
      forall t,
        t <> cur_tid pc->
        glob_npnsw_step ({-|pc,t}) l fp pc'->
        abort ({-|pc',cur_tid pc})->
        abort pc.



 
  Lemma drf_pc_glob_cons_npnsw:
    forall ge pc l fp pc' t,
      @drf_pc_glob ge pc ->
      glob_npnsw_step ({-|pc,t}) l fp pc'->
      drf_pc_glob ({-|pc,t}) /\ drf_pc_glob pc'.
  Lemma drf_pc_glob_cons_validid:
    forall ge pc t,
      @drf_pc_glob ge pc->
      pc_valid_tid pc t->
      drf_pc_glob ({-|pc,t}).


  Lemma npnsw_step_taustar_ex:
    forall ge pc l fp pc',
      @drf_pc_glob ge pc ->
      forall t,
        t<>cur_tid pc->
        glob_npnsw_step ({-|pc,t}) l fp pc'->
        forall fp' pc'',
          tau_star glob_step ({-|pc',cur_tid pc}) fp' pc''->
          exists pc1 pc2,
            tau_star glob_step pc fp' pc1 /\
            glob_npnsw_step (changepc ge pc1 t O) l fp pc2 /\
            mem_eq_pc ge pc'' (changepc ge pc2 (cur_tid pc'') (atom_bit pc'')).
  Lemma tau_N_OI:
    forall i ge pc fp pc',
      tau_N (@glob_step ge) i pc fp pc'->
      atom_bit pc = O->
      atom_bit pc' = I->
      exists j fp1 pc1,tau_N glob_step j pc fp1 pc1 /\ j<i /\
                exists pc2,type_glob_step entat pc1 tau FP.emp pc2 /\
                      exists k fp2,tau_N (type_glob_step core)k pc2 fp2 pc'/\
                            FP.union fp1 fp2 = fp /\ j+k+1=i.
 
    
  Lemma npnsw_or_sw_stepN_validid:
    forall ge i l pc fp pc',
      invpc ge pc-> GlobEnv.wd ge->
      @npnsw_or_sw_stepN ge i l pc fp pc'->
      (pc = pc' \/ pc_valid_tid pc pc'.(cur_tid )).
  Lemma mem_eq_abort:
    forall ge pc pc',
      (forall ix,mod_wd (GlobEnv.modules ge ix))->
      mem_eq_pc ge pc pc'->
      abort pc'->
      abort pc.


  Lemma npnswstep_halfatomblock_abort:
    forall ge pc l fp pc' t fp' pc'',
      drf_pc_glob pc->
      glob_npnsw_step pc l fp pc'->
      t <> cur_tid pc ->
      halfatomblockstep ge ({-|pc',t}) tau fp' pc''->
      abort pc''->
      exists pc1,halfatomblockstep ge({-|pc,t}) tau fp' pc1/\ abort pc1.
    
    

  Lemma drf_pc_glob_l3:
    forall ge pc,
      drf_pc_glob pc->
      exists NL L p gm pc0 t l fp,
        @init_config NL L p gm ge pc0 t /\ drfpc pc0 /\ star glob_step pc0 l fp pc.
  Lemma init_star_abort_validid:
    forall NL L p gm ge pc t l fp pc',
      @init_config NL L p gm ge pc t ->
      star glob_step pc l fp pc'->
      abort pc'->
      cur_valid_id ge pc'.
  Lemma drf_pc_glob_weak_abort_validid:
    forall ge pc,
      @drf_pc_glob_weak ge pc -> abort pc ->ThreadPool.valid_tid pc.(thread_pool) pc.(cur_tid).
  Lemma corestar_globstar:
    forall ge pc fp pc',
      tau_star (@type_glob_step ge core) pc fp pc'->
      tau_star glob_step pc fp pc'.
  Lemma corestar_npstar:
    forall ge pc fp pc',
      tau_star (@type_glob_step ge core) pc fp pc'->
      non_evt_star np_step pc fp pc'.
  Lemma abort_eq:
    forall ge pc,
      @abort ge pc ->
      ThreadPool.valid_tid pc.(thread_pool) pc.(cur_tid) ->
      np_abort pc.



    
  Lemma Etr_p_np_abort:
    forall ge pc,
      @drf_pc_glob ge pc->
      Etr glob_step abort final_state pc Behav_abort->
      Etr np_step np_abort final_state pc Behav_abort \/
      exists t,Etr np_step np_abort final_state ({-|pc,t}) Behav_abort /\ pc_valid_tid pc t .
  Lemma silent_diverge_cons_glob_non_evt_star:
    forall ge pc fp pc',
      non_evt_star (@glob_step ge) pc fp pc'->
      silent_diverge glob_step pc'->
      silent_diverge glob_step pc.
  Section silent_diverge.
    Variable GE:GlobEnv.t.
    Hypothesis wdge: GlobEnv.wd GE.
    Hypothesis modwdge: forall ix, mod_wd (GlobEnv.modules GE ix).
    Local Arguments cur_valid_id [GE].
    Local Arguments changepc [GE].
    Local Arguments mem_eq_pc [GE].
    Local Arguments ProgConfig [GE].
    Local Arguments noevt_stepN [GE].
    Local Arguments Sdiverge [GE].
    Local Arguments Pdiverge [GE].
    
    Definition psilent_diverge := silent_diverge (@glob_step GE).
    Definition npsilent_diverge := silent_diverge (@np_step GE).
    
  Lemma noevt_stepN_cons:
    forall i pc fp pc' j fp' pc'',
      noevt_stepN (@glob_step GE) i pc fp pc'->
      noevt_stepN glob_step j pc' fp' pc''->
      noevt_stepN glob_step (i+j) pc (FP.union fp fp') pc''.
    
  Lemma psilent_diverge_inv:
    forall pc,
      psilent_diverge pc->
      exists i fp pc',
        noevt_stepN glob_step (S i) pc fp pc' /\ psilent_diverge pc'.

  Lemma psilent_diverge_O_inv1:
    forall pc,
      psilent_diverge pc->
      (exists i fp pc',atom_bit pc' = O /\noevt_stepN glob_step (S i) pc fp pc' /\ psilent_diverge pc' )
      \/
      (~ ( exists i fp pc', atom_bit pc' = O /\noevt_stepN glob_step (S i) pc fp pc' /\ psilent_diverge pc')).

  Definition I_psilent_diverge :=
    fun pc =>
      @atom_bit GE pc = I /\ psilent_diverge pc /\
      ~ ( exists i fp pc', atom_bit pc' = O /\noevt_stepN glob_step (S i) pc fp pc' /\ psilent_diverge pc').
                                    
  Lemma psilent_diverge_foreverI_inv1:
    forall pc,
      atom_bit pc = O->
      psilent_diverge pc ->
      (~ ( exists i fp pc', atom_bit pc' = O /\noevt_stepN glob_step (S i) pc fp pc' /\ psilent_diverge pc')) ->
       exists pc1 fp pc2,
         sw_star glob_step pc pc1 /\
         glob_step pc1 tau fp pc2 /\
         I_psilent_diverge pc2.

  Lemma I_psilent_diverge_inv:
    forall pc,
      I_psilent_diverge pc ->
      exists fp pc',
        type_np_step core pc tau fp pc'/\
        I_psilent_diverge pc'.
  CoInductive core_Idiverge:@ProgConfig GE->Prop:=
    cons_core_Idiv:
      forall pc fp pc',
        atom_bit pc = I->
        type_np_step core pc tau fp pc'->
        core_Idiverge pc'->
        core_Idiverge pc.
  Lemma core_Idiverge_I_psilent_diverge_exists:
    forall pc,
      I_psilent_diverge pc->
      core_Idiverge pc.
  Lemma sw_step_I_psilent_diverge:
    forall pc pc',
      glob_step pc sw FP.emp pc'->
      core_Idiverge pc'->
      core_Idiverge ({-|pc,cur_tid pc'}).

  
  Lemma core_Idiverge_npsilent_diverge:
    forall pc,
      core_Idiverge pc ->
      npsilent_diverge pc.

  Definition O_psilent_diverge:=
    fun pc =>
      atom_bit pc = O /\
      psilent_diverge pc /\
      ~ (exists i fp pc', noevt_stepN glob_step (S i) pc fp pc' /\ I_psilent_diverge pc').
  Lemma psilent_diverge_inv2:
    forall pc,
      atom_bit pc = O ->
      psilent_diverge pc ->
      O_psilent_diverge pc \/ (exists i fp pc', noevt_stepN glob_step (S i) pc fp pc' /\ I_psilent_diverge pc').

  Ltac unfolds := unfold O_psilent_diverge,I_psilent_diverge,psilent_diverge,npsilent_diverge in *.

  Lemma O_psilent_diverge_inv:
    forall pc,
      O_psilent_diverge pc ->
      exists i fp pc',
        noevt_stepN glob_step (S i) pc fp pc'/\ O_psilent_diverge pc'.

  Lemma O_globtaustep:
    forall pc fp pc',
      glob_step pc tau fp pc'-> atom_bit pc = atom_bit pc' ->
      glob_npnsw_step pc tau fp pc' \/ haltstep GE pc tau fp pc'.
  Lemma atomblockstep_noevtstar:
    forall pc fp pc',
      atomblockstep GE pc tau fp pc'->
      non_evt_star glob_step pc fp pc'.
  Lemma O_psilent_diverge_inv':
    forall pc,
      ThreadPool.inv pc.(thread_pool)->
      O_psilent_diverge pc ->
      exists pc' fp pc'',
        sw_star glob_step pc pc'/\
        (glob_npnsw_step pc' tau fp pc'' \/ haltstep GE pc' tau fp pc'' \/ atomblockstep GE pc' tau fp pc'') /\ O_psilent_diverge pc'' /\ ThreadPool.inv pc''.(thread_pool).

  CoInductive Odiverge:@ProgConfig GE->Prop:=
  | cons_Otau:
      forall pc fp pc' pc'',
        ThreadPool.inv pc.(thread_pool)->
        glob_step pc sw FP.emp pc'->
        glob_npnsw_step pc' tau fp pc'' ->
        Odiverge pc''->
        Odiverge pc
  | cons_block:
      forall pc fp pc' pc'',
        ThreadPool.inv pc.(thread_pool)->
        glob_step pc sw FP.emp pc'->
        atomblockstarN GE 1 (cons (cur_tid pc') nil) pc' fp pc''->
        Odiverge pc''->
        Odiverge pc.

  Lemma Odiverge_O: forall pc, Odiverge pc ->atom_bit pc = O /\ ThreadPool.inv pc.(thread_pool).
  Lemma non_evt_star_cons_Odiverge:
    forall pc fp pc',
      non_evt_star glob_step pc fp pc'->
      atom_bit pc = O ->
      ThreadPool.inv pc.(thread_pool)->
      Odiverge pc'->
      Odiverge pc.
  Lemma O_psilent_diverge_Odiverge:
    forall pc,
      ThreadPool.inv pc.(thread_pool)->
      O_psilent_diverge pc->
      Odiverge pc.


  Definition neverIdiverge (pc:@ProgConfig GE):Prop:=
    Odiverge pc /\
    ~ (exists fp pc' fp' pc'', non_evt_star glob_step pc fp pc' /\ atomblockstarN GE 1 (cons(cur_tid pc') nil) pc' fp' pc'' /\ Odiverge pc'').

  Definition will_neverIdiverge (pc:@ProgConfig GE):Prop:=
    Odiverge pc /\
    exists fp pc', non_evt_star glob_step pc fp pc' /\ neverIdiverge pc'.

  CoInductive npnswdiverge:@ProgConfig GE->Prop:=
  | cons_npnsw_div:
      forall pc fp pc' pc'',
        ThreadPool.inv pc.(thread_pool)->
        glob_step pc sw FP.emp pc'->
        glob_npnsw_step pc' tau fp pc'' ->
        npnswdiverge pc''->
        npnswdiverge pc.
  Lemma Odiverge_neverIdiverge_npnswdiverge:
    forall pc,
      neverIdiverge pc ->
      npnswdiverge pc.
  Lemma npnsw_taustar_non_evt_star:
    forall pc fp pc',
      tau_star glob_npnsw_step pc fp pc'->
      non_evt_star (@glob_step GE) pc fp pc'.
  Lemma atomblockstarN_non_evt_star:
    forall i l pc fp pc',
      atomblockstarN GE i l pc fp pc'->
      non_evt_star glob_step pc fp pc'.
  Lemma Odiverge_not_will_neverIdiverge_inv:
    forall pc,
      Odiverge pc ->
      ~ will_neverIdiverge pc ->
      exists fp pc' fp' pc'',
        npnsw_or_sw_star GE pc fp pc' /\
        atomblockstarN GE 1 (cons (cur_tid pc') nil) pc' fp' pc'' /\
        Odiverge pc'' /\
        ~ will_neverIdiverge pc''.


  CoInductive blockdiverge:@ProgConfig GE->Prop:=
    cons_npnsw_or_sw_star_block:
      forall pc fp pc' fp' pc'',
        atom_bit pc = O ->
        ThreadPool.inv pc.(thread_pool)->
        npnsw_or_sw_star GE pc fp pc'->
        atomblockstarN GE 1 (cons (cur_tid pc') nil) pc' fp' pc'' ->
        blockdiverge pc''->
        blockdiverge pc.
  Lemma Odiverge_not_will_neverIdiverge_atomblockdiverge:
    forall pc,
      Odiverge pc ->
      ~ will_neverIdiverge pc ->
      blockdiverge pc.
  Lemma psilent_diverge_case:
    forall pc,
      atom_bit pc = O ->
      ThreadPool.inv pc.(thread_pool)->
      psilent_diverge pc ->
      (exists i fp pc', noevt_stepN glob_step (S i) pc fp pc' /\ core_Idiverge pc') \/
      (exists fp pc', non_evt_star glob_step pc fp pc' /\ npnswdiverge pc')\/
      blockdiverge pc.
End silent_diverge.
Section diverge_proof.
  Lemma noevt_stepN_Si_Iinv_drfsafe:
    forall ge pc i fp pc',
      @drf_pc_glob ge pc ->
      noevt_stepN ge glob_step (S i) pc fp pc'->
      atom_bit pc' = I->
      exists i l fp1 fp2 pc0 pc1 pc2 pc3 t pc4 fp3,
        sw_star glob_step pc pc0 /\
        atomblockstarN ge i l pc0 fp1 pc1 /\
        npnsw_or_sw_star ge pc1 fp2 pc2 /\
        type_glob_step entat ({-|pc2,t}) tau FP.emp pc3 /\ tau_star (type_glob_step core) pc3 fp3 pc4 /\ mem_eq_pc ge pc' pc4.
  Lemma noevt_stepN_Si_Oinv_drfsafe:
    forall ge pc i fp pc',
      @drf_pc_glob ge pc ->
      noevt_stepN ge glob_step (S i) pc fp pc'->
      atom_bit pc' = O->
      exists i l fp1 fp2 pc0 pc1 pc2,
        sw_star glob_step pc pc0 /\
        atomblockstarN ge i l pc0 fp1 pc1 /\
        npnsw_or_sw_star ge pc1 fp2 pc2 /\
        mem_eq_pc ge pc' ({-|pc2,cur_tid pc'}).

  Lemma glob_npnsw_step_atomblockstarN_inv_ex_drfsafe:
    forall ge pc l fp pc',
      drf_pc_glob pc ->
      glob_npnsw_step pc l fp pc'->
      forall t fp1 pc1 ltids,
        t <> cur_tid pc->
        atomblockstarN ge 1 ltids ({-|pc',t}) fp1 pc1->
        FP.smile fp fp1 /\ exists pc',atomblockstarN ge 1 ltids ({-|pc,t}) fp1 pc'/\ exists pc'',glob_npnsw_step pc' l fp pc'' /\ mem_eq_pc ge pc1 ({-|pc'',cur_tid pc1}) /\ cur_tid pc'' = cur_tid pc.

  Lemma npnsw_or_sw_star_atomblockstarN_ex_drfsafe:
    forall i l ge pc fp pc' fp' pc'' ltids (drfsafe:drf_pc_glob pc),
      npnsw_or_sw_stepN ge i l pc fp pc'->
      atomblockstarN ge 1 ltids pc' fp' pc''->
      exists fp1 pc1,
        atomblockstarN ge 1 ltids ({-|pc,cur_tid pc'}) fp1 pc1 /\
        exists fp2 pc2,
          npnsw_or_sw_star ge pc1 fp2 pc2 /\ mem_eq_pc ge ({-|pc'',cur_tid pc2}) pc2.


  CoInductive blockdiverge_tid{ge:GlobEnv.t} :@ProgConfig ge->tid->Prop:=
  | cons_blockdiverge_tid:
      forall pc fp pc' fp' pc'' t,
        atom_bit pc = O->
        ThreadPool.inv pc.(thread_pool)->
        npnsw_or_sw_star ge pc fp pc'->
        atomblockstarN ge 1 (cur_tid pc'::nil) pc' fp' pc''->
        blockdiverge_tid pc'' t->
        blockdiverge_tid pc (cur_tid pc').

  Lemma blockdiverge_tid_exists_lemma:
    forall ge pc fp pc' fp' pc'',
       atom_bit pc = O->
       ThreadPool.inv pc.(thread_pool)->
       npnsw_or_sw_star ge pc fp pc'->
       atomblockstarN ge 1 (cur_tid pc'::nil) pc' fp' pc''->
       blockdiverge ge pc'' ->
       blockdiverge_tid pc (cur_tid pc').

  Lemma blockdiverge_tid_exists:
    forall ge pc,
      blockdiverge ge pc->
      exists t,blockdiverge_tid pc t.
  Lemma non_evt_star_cons_step:
    forall ge pc fp pc' fp' pc'',
      non_evt_star np_step pc fp pc'->
      non_evt_plus np_step pc' fp' pc''->
      non_evt_plus (@np_step ge) pc (FP.union fp fp') pc''.
  Lemma atomblockstarN_NP_drfsafe:
    forall ge l pc fp pc' t,
      drf_pc_glob pc ->
      atomblockstarN ge 1 l pc fp pc'->
      blockdiverge_tid pc' t->
      exists pc1,non_evt_star np_step pc fp pc1/\
            ((exists t,np_step pc1 sw FP.emp ({-|pc',t}) )).
  Lemma npnsw_or_sw_star_cons_blockdiverge:
    forall ge pc fp pc' t,
      ThreadPool.inv pc.(thread_pool)-> atom_bit pc = O->
      npnsw_or_sw_star ge pc fp pc' ->
      blockdiverge_tid pc' t->
      blockdiverge_tid pc t.
  Lemma mem_eq_blockdiverge_tid:
    forall ge pc pc' t (wdge:GlobEnv.wd ge)(modwdge:forall ix,mod_wd (GlobEnv.modules ge ix)),
      mem_eq_pc ge pc pc'->
      blockdiverge_tid pc t->
      blockdiverge_tid pc' t.

  Lemma blockdiverge_changetid:
    forall ge pc t (wdge:GlobEnv.wd ge),
      blockdiverge_tid pc t->
      forall i,
        @blockdiverge_tid ge ({-|pc,i}) t.
  Lemma blockdiverge_valid_tid:
    forall ge pc t,
      ThreadPool.inv pc.(thread_pool)->
      GlobEnv.wd ge->
      blockdiverge_tid pc t->
      @pc_valid_tid ge pc t.
    
  Lemma blockdiverge_tid_npdiverge:
    forall ge pc t,
      drf_pc_glob pc ->
      blockdiverge_tid pc t ->
      Pdiverge ge ({-|pc,t}).

  Lemma blockdiverge_npsilent_diverge:
    forall ge pc,
      drf_pc_glob pc ->
      blockdiverge ge pc->
      exists t, npsilent_diverge ge ({-|pc,t}) /\ pc_valid_tid pc t.

  


  Lemma npnsw_or_sw_stepN_last_valid:
    forall i l ge pc fp pc' (wdge:GlobEnv.wd ge),
      ThreadPool.inv pc.(thread_pool)->
      npnsw_or_sw_stepN ge (S i) l pc fp pc'->
      cur_valid_id ge pc'.

  Lemma npnsw_cons_npnsw_or_sw_stepN_sw:
    forall ge pc fp pc' t fp' pc'' i l,
      GlobEnv.wd ge->
      ThreadPool.inv pc.(thread_pool)->
      atom_bit pc = O->
      @glob_npnsw_step ge pc tau fp pc'->
      npnsw_or_sw_stepN ge (S i) l ({-|pc',t}) fp' pc''->
      npnsw_or_sw_stepN ge (S (S i)) (cons (cur_tid pc) l) pc (FP.union fp fp') pc''.
  Lemma npnsw_or_sw_star_div:
    forall k lt ge pc fp pc' ,
      drf_pc_glob pc->
      npnsw_or_sw_stepN ge k lt pc fp pc' ->
      exists i l fp1 pc1 fp2 pc2,
        tau_star glob_npnsw_step ({-|pc,cur_tid pc'}) fp1 pc1 /\
        npnsw_or_sw_stepN ge i l pc1 fp2 pc2 /\ mem_eq_pc ge pc' pc2 /\
        ~ list_matched l (cur_tid pc').


  Lemma npnsw_or_sw_stepN_last_valid_alt:
    forall i l ge pc fp pc' (wdge:GlobEnv.wd ge),
      ThreadPool.inv pc.(thread_pool)->
      npnsw_or_sw_stepN ge (S i) l pc fp pc'->
      pc_valid_tid pc (cur_tid pc').
  Lemma thread_sim_refl:
    forall ge pc, thread_sim ge pc pc.
  Lemma thread_sim_comm:
    forall ge pc pc',
      thread_sim ge pc pc'->
      thread_sim ge pc' pc.
  Lemma thread_sim_trans:
    forall ge pc pc1 pc2,
      thread_sim ge pc pc1->
      thread_sim ge pc1 pc2 ->
      thread_sim ge pc pc2.
  Lemma thread_sim_preserve:
    forall ge x pc pc' t fp pc1,
      thread_sim ge ({-|pc,t}) pc'->
      cur_tid pc <> t->
      type_glob_step x pc tau fp pc1->
      x = core \/ x = call \/ x = ret ->
      thread_sim ge ({-|pc1,t}) pc'.
  Lemma thread_sim_preserve2:
    forall ge x pc pc' t fp pc1,
      thread_sim ge pc ({-|pc',t})->
      cur_tid pc' <> t->
      type_glob_step x pc' tau fp pc1->
      x = core \/ x = call \/ x = ret ->
      thread_sim ge pc ({-|pc1,t}).
  Lemma npnsw_or_sw_stepN_thread_sim:
    forall i l ge pc fp pc' t,
      GlobEnv.wd ge->
      (forall ix, mod_wd (GlobEnv.modules ge ix))->
      ThreadPool.inv pc.(thread_pool)->
      npnsw_or_sw_stepN ge i l pc fp pc'->
      ~ list_matched l t->
      thread_sim ge ({-|pc,t}) ({-|pc',t}).
    
    

  Lemma npnsw_or_sw_stepN_atomO:
    forall i l ge pc fp pc',
      npnsw_or_sw_stepN ge i l pc fp pc'->
      atom_bit pc = O /\ atom_bit pc' = O.
  Lemma npnsw_or_sw_stepN_i_1_split:
    forall i l ge pc fp pc',
      npnsw_or_sw_stepN ge (S i) l pc fp pc'->
      exists l1 fp1 pc1 l2 fp2,
        npnsw_or_sw_stepN ge i l1 pc fp1 pc1 /\
        npnsw_or_sw_stepN ge 1 l2 pc1 fp2 pc' /\
        app l1 l2 = l /\ FP.union fp1 fp2 = fp.

  Lemma drf_pc_glob_safe:
    forall ge pc ,
      @drf_pc_glob ge pc->
      safe_state glob_step abort pc.
  Lemma drf_pc_glob_drf:
    forall ge pc,
      @drf_pc_glob ge pc ->
      ~ race glob_predict_star_alter pc.

  Lemma npnsw_step_halfatomblockstep_ex:
    forall ge pc l fp pc' t fp2 pc2,
      drf_pc_glob pc->
      glob_npnsw_step pc l fp pc'-> invpc ge pc ->
      t <> cur_tid pc->
      halfatomblockstep ge ({-|pc',t}) tau fp2 pc2->
      FP.smile fp fp2 /\ exists pc1,halfatomblockstep ge ({-|pc,t}) tau fp2 pc1 .

  Lemma npnsw_star_halfatomblockstep_ex:
    forall ge pc fp pc' t fp2 pc2,
      drf_pc_glob pc->
      tau_star glob_npnsw_step pc fp pc'-> invpc ge pc ->
      t <> cur_tid pc->
      halfatomblockstep ge ({-|pc',t}) tau fp2 pc2->
      FP.smile fp fp2 /\ exists pc1,halfatomblockstep ge ({-|pc,t}) tau fp2 pc1.

  Lemma drfsafe_npnsw_step_fpsmile:
    forall ge pc fp pc' t fp2 pc2,
      @drf_pc_glob ge pc->
      glob_npnsw_step pc tau fp pc'->
      t <> cur_tid pc->
      glob_npnsw_step ({-|pc',t}) tau fp2 pc2->
      FP.smile fp fp2 /\ exists pc1,glob_npnsw_step ({-|pc,t}) tau fp2 pc1 /\ exists pc2',
  glob_npnsw_step ({-|pc1,cur_tid pc}) tau fp pc2' /\ mem_eq_pc ge pc2 ({-|pc2',cur_tid pc2}).

  Lemma drfsafe_npnsw_or_sw_stepN_npnswstep_fpsmile:
    forall i l ge pc fp pc' fp' t pc'',
      drf_pc_glob pc ->
      npnsw_or_sw_stepN ge i l pc fp pc'->
      ~ list_matched l t->
      glob_npnsw_step ({-|pc',t}) tau fp' pc''->
      FP.smile fp fp' /\ exists pc1,glob_npnsw_step ({-|pc,t}) tau fp' pc1 /\
                               exists pc2, npnsw_or_sw_stepN ge i l pc1 fp pc2 /\
                                      mem_eq_pc ge pc'' pc2.
  Lemma drfsafe_npnsw_or_sw_stepN_halfatomblockstep_fpsmile:
    forall i l ge pc fp pc' fp' t pc'',
      drf_pc_glob pc ->
      npnsw_or_sw_stepN ge i l pc fp pc'->
      ~ list_matched l t->
      halfatomblockstep ge ({-|pc',t}) tau fp' pc''->
      FP.smile fp fp'.

  Lemma halfatomblockstep_cons:
    forall ge pc fp pc' fp' pc'',
      halfatomblockstep ge pc tau fp pc'->
      type_glob_step core pc' tau fp' pc''->
      halfatomblockstep ge pc tau (FP.union fp fp') pc''.

  Lemma drfsafe_npnsw_or_sw_stepN_thread_sim:
    forall i l ge pc fp pc' t ,
      drf_pc_glob pc ->
      npnsw_or_sw_stepN ge i l pc fp pc'->
      ~ list_matched l t->
      thread_sim ge ({-|pc,t}) ({-|pc',t}).

  Lemma GPre_trans:
    forall ge m1 m2 m3 fp t,
      GPre ge m1 m2 fp t->
      GPre ge m2 m3 fp t->
      GPre ge m1 m3 fp t.
  Lemma GPre_refl:
    forall ge m fp t,GPre ge m m fp t.
  Lemma list_not_matched_split:
    forall A l a b,
      @list_matched A l b ->
      list_matched (cons a l) b.
  Lemma drfsafe_npnsw_or_sw_stepN_fpsmile_GPre:
    forall i l ge pc fp pc' t fp0,
      drf_pc_glob pc ->
      npnsw_or_sw_stepN ge i l pc fp pc'->
      ~ list_matched l t->
      FP.smile fp fp0->
      GPre ge pc.(gm) pc'.(gm) fp0 t.


  Lemma thread_sim_coreIdiverge:
    forall ge pc pc' (inv1:ThreadPool.inv pc.(thread_pool))(inv2 :ThreadPool.inv pc'.(thread_pool)),
      GlobEnv.wd ge->
      (forall ix, mod_wd (GlobEnv.modules ge ix))->
      thread_sim ge pc pc'->
      (forall fp pc1,
          tau_star (type_glob_step core) pc fp pc1->
          GPre ge pc.(gm) pc'.(gm) fp pc.(cur_tid))->
      core_Idiverge ge pc->
      core_Idiverge ge pc'.


 Lemma mem_eq_coreIdiverge:
    forall ge pc pc' (H_modwdge:forall ix, mod_wd (GlobEnv.modules ge ix)),
      mem_eq_pc ge pc pc'->
      core_Idiverge ge pc->
      core_Idiverge ge pc'.
  Lemma silent_diverge_cons_np_non_evt_star:
    forall (ge : GlobEnv.t) (pc : @ProgConfig ge) (fp : FP.t) (pc' : ProgConfig),
      non_evt_star np_step pc fp pc' ->
      silent_diverge np_step pc' ->
      silent_diverge np_step pc.
  Lemma core_Idiverge_cons_corestar:
    forall ge pc fp pc',
      tau_star (type_glob_step core) pc fp pc'->
      core_Idiverge ge pc'->
      core_Idiverge ge pc.
  Lemma case_coreIdiverge:
    forall ge pc i fp pc',
      drf_pc_glob pc->
      noevt_stepN ge glob_step (S i) pc fp pc' ->
      core_Idiverge ge pc' ->
      npsilent_diverge ge pc \/
      exists t,npsilent_diverge ge ({-|pc,t}) /\ pc_valid_tid pc t.
    

  CoInductive AO_psilent_diverge{ge}:tid->@ProgConfig ge->Prop:=
    AO_mk:
      forall pc fp pc1 fp1 pc2,
        npnsw_or_sw_star ge pc fp pc1 ->
        glob_npnsw_step pc1 tau fp1 pc2 ->
        AO_psilent_diverge (cur_tid pc1) pc2 ->
        AO_psilent_diverge (cur_tid pc1)pc.

  Lemma AO_psilent_diverge_valid_t:
    forall ge pc t,
      @drf_pc_glob ge pc ->
      AO_psilent_diverge t pc->
      pc_valid_tid pc t.

  Lemma npnsw_or_sw_stepN_pc_valid_tid_preserve:
    forall i l ge pc fp pc' t (wdge:GlobEnv.wd ge)(v1:invpc ge pc),
      @npnsw_or_sw_stepN ge i l pc fp pc'->
      pc_valid_tid pc t->
      pc_valid_tid pc' t.
    
  Lemma npnsw_star_cons_npnsw_or_sw_star:
    forall (GE : GlobEnv.t) (pc : ProgConfig)
      (fp : FP.t) (pc' : ProgConfig),
      tau_star glob_npnsw_step pc fp pc' ->
      forall (fp2 : FP.t) (pc'' : ProgConfig),
        npnsw_or_sw_star GE pc' fp2 pc'' -> npnsw_or_sw_star GE pc (FP.union fp fp2) pc''.
  Lemma mem_eq_AO_psilent_diverge:
    forall ge pc pc' t,
      GlobEnv.wd ge->
      (forall ix, mod_wd (GlobEnv.modules ge ix))->
      ThreadPool.inv pc.(thread_pool)->
      mem_eq_pc ge pc pc'->
      AO_psilent_diverge t pc ->
      AO_psilent_diverge t pc'.
  Lemma AO_psilent_diverge_cons_npnsw_or_sw_star:
    forall ge pc fp pc' t,
      npnsw_or_sw_star ge pc fp pc'->
      AO_psilent_diverge t pc'->
      AO_psilent_diverge t pc.
  Lemma drf_safe_AO_psilent_diverge_inv:
    forall ge pc t,
      @drf_pc_glob ge pc ->
      AO_psilent_diverge t pc ->
      (exists fp pc1 , drf_pc_glob pc1 /\ glob_npnsw_step ({-|pc,t}) tau fp pc1 /\ AO_psilent_diverge t pc1).

  
Definition no_rep (l:list tid):Prop:=
    forall i j,
      i <> j ->
      i < length l ->
      j < length l ->
      List.nth_error l i <> List.nth_error l j.

  Definition pcvalid{ge}(pc:@ProgConfig ge)(l:list tid):Prop:=
    forall t, List.In t l ->pc_valid_tid pc t.
  Definition isdone {ge}(pc:@ProgConfig ge)(t:list tid):Prop:=
    forall fp pc' fp' pc'',
        npnsw_or_sw_star ge pc fp pc'->
        glob_npnsw_step pc' tau fp' pc'' ->
        npnswdiverge ge pc'' ->
        ~ List.In (cur_tid pc') t.

  Lemma notalldone:
    forall ge pc lt,
      drf_pc_glob pc->
      npnswdiverge ge pc ->
      isdone pc lt->
      (forall t,
          pc_valid_tid pc t->
          list_matched lt t)
      ->
      False.

  Lemma npnsw_or_sw_star_cons:
    forall ge pc fp pc' fp' pc'',
      npnsw_or_sw_star ge pc fp pc'->
      npnsw_or_sw_star ge pc' fp' pc''->
      npnsw_or_sw_star ge pc (FP.union fp fp') pc''.

  Definition willdone := fun ge pc lt t=> (exists fp pc1, tau_star glob_npnsw_step ({-|pc,t}) fp pc1 /\ npnswdiverge ge ({-|pc1,cur_tid pc}) /\ isdone pc1 (cons t lt)).

  Lemma isdone_nil: forall ge pc , @isdone ge pc nil.
  Lemma isdone_app:
    forall ge pc t t',
      @isdone ge pc t->
      @isdone ge pc t'->
      @isdone ge pc (app t t').
  Lemma mem_eq_npnswstep:
    forall ge pc pc' fp pc1 (modwdge:forall ix, mod_wd (GlobEnv.modules ge ix)),
      mem_eq_pc ge pc pc'->
      glob_npnsw_step pc tau fp pc1 ->
      exists pc2, mem_eq_pc ge pc1 pc2 /\
             glob_npnsw_step pc' tau fp pc2.

  Lemma drf_pc_glob_cons_npnsw_star:
    forall (ge : GlobEnv.t) (pc : ProgConfig)(fp : FP.t) (pc' : ProgConfig) ,
      @drf_pc_glob ge pc ->
      tau_star glob_npnsw_step pc fp pc' ->
      drf_pc_glob pc'.
 
  Lemma mem_eq_npnswdiverge:
    forall ge pc pc' t (modwdge:forall ix ,mod_wd (GlobEnv.modules ge ix))(wdge:GlobEnv.wd ge),
      ThreadPool.inv pc.(thread_pool)->
      mem_eq_pc ge pc ({-|pc',t}) ->
      npnswdiverge ge pc ->
      npnswdiverge ge pc'.
  Lemma npnsw_or_sw_star_cons_npnsw_diverge:
    forall i l ge pc fp pc'(wdge:GlobEnv.wd ge),
      ThreadPool.inv pc.(thread_pool)-> atom_bit pc = O->
      npnsw_or_sw_stepN ge i l pc fp pc'->
      npnswdiverge ge pc'->
      npnswdiverge ge pc.
  Lemma npnswdiverge_notdone:
    forall ge pc pc' fp lt,
      drf_pc_glob pc->
      glob_npnsw_step pc tau fp pc'->
      npnswdiverge ge pc'->
      isdone pc lt ->
      ~ willdone ge pc lt (cur_tid pc)->
      exists fp1 pc1,
        tau_plus glob_npnsw_step pc' fp1 pc1/\
        npnswdiverge ge pc1/\
        isdone pc' lt /\
        ~ willdone ge pc' lt (cur_tid pc').

  Lemma npnswdiverge_notdone_tbc:
    forall ge pc pc' fp lt,
      drf_pc_glob pc->
      tau_plus glob_npnsw_step pc fp pc'->
      npnswdiverge ge pc'->
      isdone pc lt ->
      ~ willdone ge pc lt (cur_tid pc)->
      exists fp1 pc1,
        glob_npnsw_step pc tau fp1 pc1/\
        npnswdiverge ge pc1/\
        isdone pc lt /\
        ~ willdone ge pc lt (cur_tid pc).
    
  Lemma npnsw_tauplus_nonevtplus_np:
    forall ge pc fp pc',
      tau_plus glob_npnsw_step pc fp pc'->
      tau_plus (@np_step ge) pc fp pc'.

  CoInductive npnsw_diverge'{ge}:@ProgConfig ge->Prop:=
    mk_npnsw_diverge':
      forall pc fp pc',
        atom_bit pc = O ->
        glob_npnsw_step pc tau fp pc'->
        npnsw_diverge' pc'->
        npnsw_diverge' pc.

  
  Lemma npnswdiverge_cur_tid_not_done_forever:
    forall ge pc pc' fp lt,
      drf_pc_glob pc->
      glob_npnsw_step pc tau fp pc'->
      npnswdiverge ge pc'->
      isdone pc lt ->
      ~ willdone ge pc lt (cur_tid pc)->
      npnsw_diverge' pc.

  Lemma cur_not_done:
    forall ge pc pc' fp lt,
      drf_pc_glob pc->
      glob_npnsw_step pc tau fp pc'->
      npnswdiverge ge pc'->
      isdone pc lt ->
      ~ List.In (cur_tid pc) lt.

  Lemma norep_split:
    forall l t,
      no_rep (cons t l)->
      no_rep l.
  Lemma norep_cons:
    forall l t,
      ~ List.In t l ->
      no_rep l->
      no_rep (cons t l).
    
 


  Lemma if_will_cur_done:
    forall ge pc lt,
      drf_pc_glob pc-> cur_valid_id ge pc ->
      isdone pc lt ->
      pcvalid pc lt->
      no_rep lt ->
      ~ List.In (cur_tid pc) lt ->
      willdone ge pc lt (cur_tid pc)->
      exists fp pc',
        drf_pc_glob pc'/\ cur_valid_id ge pc' /\ cur_tid pc = cur_tid pc' /\
        tau_star glob_npnsw_step pc fp pc'/\ npnswdiverge ge pc' /\
        isdone pc' (cons (cur_tid pc) lt) /\
        pcvalid pc' (cons (cur_tid pc) lt) /\
        no_rep (cons (cur_tid pc) lt).

  Lemma if_will_cur_done_tbc:
    forall ge pc lt,
      drf_pc_glob pc ->
      npnswdiverge ge pc ->
      isdone pc (cons (cur_tid pc) lt) ->
      pcvalid pc (cons (cur_tid pc) lt) ->
      no_rep (cons (cur_tid pc) lt)->
      exists fp pc1 pc2,
        glob_step pc sw FP.emp pc1 /\
        glob_npnsw_step pc1 tau fp pc2 /\
        ~ List.In (cur_tid pc2) (cons (cur_tid pc) lt) /\
        drf_pc_glob pc1 /\ cur_valid_id ge pc1/\
        npnswdiverge ge pc1/\npnswdiverge ge pc2/\
        isdone pc1 (cons (cur_tid pc) lt)/\
        pcvalid pc1 (cons (cur_tid pc) lt)/\
        no_rep (cons (cur_tid pc) lt).
    
  Lemma if_will_cur_done_tbc2:
    forall ge pc lt,
      drf_pc_glob pc-> cur_valid_id ge pc ->
      isdone pc lt ->
      pcvalid pc lt->
      no_rep lt ->
      ~ List.In (cur_tid pc) lt ->
      willdone ge pc lt (cur_tid pc)->
      exists fp fp2 pc' pc1 pc2,
        tau_star glob_npnsw_step pc fp pc'/\
        glob_step pc' sw FP.emp pc1 /\
        glob_npnsw_step pc1 tau fp2 pc2 /\
        ~ List.In (cur_tid pc2) (cons (cur_tid pc) lt) /\
        drf_pc_glob pc1 /\ cur_valid_id ge pc1/\
        npnswdiverge ge pc1/\npnswdiverge ge pc2/\
        isdone pc1 (cons (cur_tid pc) lt)/\
        pcvalid pc1 (cons (cur_tid pc) lt)/\
        no_rep (cons (cur_tid pc) lt).

  Definition thread_nums {ge}(pc:@ProgConfig ge):nat:=
    BinPos.Pos.to_nat pc.(thread_pool).(ThreadPool.next_tid).

  Lemma thread_nums_preserve:
    forall ge pc l fp pc',
      star (@glob_step ge) pc l fp pc'->
      thread_nums pc' = thread_nums pc.

  Lemma norep_nodup:
    forall l,
      no_rep l ->
      List.NoDup l.
  Lemma maxi:
    forall ge pc lt,
     @pcvalid ge pc lt->
     no_rep lt ->
     length lt < thread_nums pc.
       

  Lemma if_will_cur_done_tbc3:
    forall i ge pc lt fp pc',
      drf_pc_glob pc-> cur_valid_id ge pc ->
      glob_npnsw_step pc tau fp pc'->
      npnswdiverge ge pc'->
      isdone pc lt ->
      pcvalid pc lt->
      no_rep lt ->
      ~ List.In (cur_tid pc) lt ->
      i = thread_nums pc - length lt ->
      exists fp1 pc1 lt' fp2 pc2,
        drf_pc_glob pc1/\ npnswdiverge ge pc2 /\
        npnsw_or_sw_star ge pc fp1 pc1 /\
        glob_npnsw_step pc1 tau fp2 pc2 /\
        isdone pc1 lt'/\
        ~ willdone ge pc1 lt' (cur_tid pc1).

  Lemma npnswdiverge_will_forever:
    forall ge pc fp pc',
      drf_pc_glob pc-> cur_valid_id ge pc ->
      glob_npnsw_step pc tau fp pc'->
      npnswdiverge ge pc'->
      exists fp1 pc1 ,
        drf_pc_glob pc1 /\
        npnsw_or_sw_star ge pc fp1 pc1 /\
        npnsw_diverge' pc1.

  Lemma npnswdiverge_AO_psilent_diverge:
    forall ge pc fp1 pc1,
      drf_pc_glob pc1->
      npnsw_or_sw_star ge pc fp1 pc1 ->
      npnsw_diverge' pc1->
      AO_psilent_diverge (cur_tid pc1) pc.
End diverge_proof.

Lemma AO_psilent_diverge_exists:
  forall ge pc,
    drf_pc_glob pc->
    npnswdiverge ge pc->
    exists t,AO_psilent_diverge t pc.
 Lemma npnswdiverge_npdiverge:
  forall ge pc,
    drf_pc_glob pc->
    npnswdiverge ge pc ->
    exists t, pc_valid_tid pc t /\ npsilent_diverge ge ({-|pc,t}).
  
  Lemma Etr_p_np_diverge:
    forall ge pc,
      drf_pc_glob pc->
      Etr (@glob_step ge) abort final_state pc Behav_diverge->
      Etr np_step np_abort final_state pc Behav_diverge \/ exists t,Etr np_step np_abort final_state ({-|pc,t}) Behav_diverge /\ pc_valid_tid pc t .


  Lemma limited_etr_p_cons_non_evt_star:
     forall ge i pc b,
       limited_etr i (@glob_step ge) abort final_state pc b->
       forall pc0 fp,
         non_evt_star glob_step pc0 fp pc->
         limited_etr i glob_step abort final_state pc0 b.

  Lemma glob_evt_step_sw:
    forall ge pc v pc',
      @glob_step ge pc (evt v) FP.emp pc'->
      ThreadPool.inv pc.(thread_pool)->
      GlobEnv.wd ge->
      glob_step pc' sw FP.emp pc'.
  Lemma glob_evt_step_np:
    forall ge pc v pc',
      @glob_step ge pc (evt v) FP.emp pc'->
      ThreadPool.inv pc.(thread_pool)->
      GlobEnv.wd ge->
      np_step pc (evt v) FP.emp pc'.
      


  
  Definition mod_wd_ge (ge:GlobEnv.t):Prop:=
    forall ix,
      mod_wd (GlobEnv.modules ge ix).
  Lemma mem_eq_pc_limited_etr_p:
    forall i ge pc pc' b,
      mod_wd_ge ge->
      mem_eq_pc ge pc pc'->
      limited_etr i glob_step abort final_state pc b->
      limited_etr i glob_step abort final_state pc' b.


  Lemma limited_etr_p_np_base:
    forall ge pc B,
      drf_pc_glob pc->
      limited_etr 0 (@glob_step ge) abort final_state pc B->
      (limited_etr 0 np_step np_abort final_state pc B) \/ (exists t,limited_etr 0 np_step np_abort final_state ({-|pc,t}) B /\ pc_valid_tid pc t ) .
  Lemma limited_etr_p_np_ind:
    forall i ge pc B,
      drf_pc_glob pc->
      atom_bit pc = O->
      limited_etr (S i) (@glob_step ge) abort final_state pc B->
      exists t,limited_etr (S i) np_step np_abort final_state ({-|pc,t}) B /\ pc_valid_tid pc t.

  Lemma limited_etr_p_np:
    forall i ge pc B,
      drf_pc_glob pc ->
      atom_bit pc = O->
      limited_etr i (@glob_step ge) abort final_state pc B->
      (limited_etr i np_step np_abort final_state pc B) \/
      (exists t,limited_etr i np_step np_abort final_state ({-|pc,t}) B /\ pc_valid_tid pc t).


  CoInductive glob_inf_etr {ge}:@ProgConfig ge->behav->Prop:=
  | build_inf_etr_glob:
      forall pc b,
        glob_inf_etr pc b->
        forall pc0 pc01 fp0 pc1 v,
          glob_step pc0 sw FP.emp pc01 ->
          non_evt_thrd_globstar ge pc01 fp0 pc1 ->
          glob_step pc1 (evt v)FP.emp pc ->
          glob_inf_etr pc0 (Behav_cons v b).
  Lemma mem_eq_inf_etr:
    forall ge,
      (forall ix,mod_wd (GlobEnv.modules ge ix))->
      forall a f pc b,
      inf_etr_alt2 (@glob_step ge) a f pc b->
      forall pc',
        mem_eq_pc ge pc pc'->
        inf_etr_alt2 glob_step a f pc' b.
    
  Lemma inf_etr_glob_inf_etr:
    forall ge ab fn pc b,
      drf_pc_glob pc->
      inf_etr_alt2 (@glob_step ge) ab fn pc b->
      glob_inf_etr pc b.
    

  CoInductive glob_inf_etr_2 {ge}:@ProgConfig ge->behav->Prop:=
  | build_inf_etr_glob2:
      forall pc b,
        glob_inf_etr_2 pc b->
        forall pc0 fp0 pc1 v pc2,
          non_evt_thrd_globstar ge pc0 fp0 pc1 ->
          glob_step pc1 (evt v)FP.emp pc2 ->
          glob_step pc2 sw FP.emp pc ->
          glob_inf_etr_2 pc0 (Behav_cons v b).

  Lemma glob_inf_etr_l1:
    forall ge pc pc',
      @glob_step ge pc sw FP.emp pc'->
      forall b,
        glob_inf_etr_2 pc' b->
        glob_inf_etr pc b.
  Lemma glob_inf_etr_l2:
    forall ge pc0 fp0 pc1 v pc2 b,
      non_evt_thrd_globstar ge pc0 fp0 pc1 ->
      glob_step pc1 (evt v)FP.emp pc2 ->
      glob_inf_etr pc2 b->
      glob_inf_etr_2 pc0 (Behav_cons v b).

  Lemma glob_inf_etr_l3:
    forall ge pc b,
      @glob_inf_etr ge pc b->
      exists pc',
        glob_step pc sw FP.emp pc' /\ glob_inf_etr_2 pc' b.

  


  Lemma non_evt_thrd_globstar_inv_preserve:
    forall ge pc fp pc',
      GlobEnv.wd ge->
      @non_evt_thrd_globstar ge pc fp pc'->
      invpc ge pc->
      invpc ge pc'.
  Lemma glob_inf_etr_np:
    forall ge pc pc' b,
      GlobEnv.wd ge ->
      (forall ix,mod_wd (GlobEnv.modules ge ix))->
      invpc ge pc->
      @glob_step ge pc sw FP.emp pc'->
      glob_inf_etr_2 pc' b->
      inf_etr np_step np_abort final_state pc' b.

  Lemma config_refine_alt:
    forall sge spc tge tpc t,
      @config_refine tge sge tpc spc->
      atom_bit tpc = O->
      pc_valid_tid tpc t->
      config_refine ({-|tpc,t}) spc.
  Lemma init_pair_config_refine:
    forall NL L sc tc e sgm sge spc tgm tge tpc i i',
      @init_config NL L (sc,e) sgm sge spc i->
      @init_config NL L (tc,e) tgm tge tpc i'->
      config_refine ({-|tpc,i}) spc->
      config_refine tpc spc.
    
  Lemma np_p_config_refine_weak_proof{NL L}:
    forall P (H:True),
      wd_langs (fst P) ->
      forall (gm : gmem) (ge : GlobEnv.t) (pc : ProgConfig),
        @init_config NL L P gm ge pc (cur_tid pc) ->
        forall (B : behav) (HSafe:safe_state glob_step abort pc)(Hdrf:drfpc pc),
          Etr glob_step abort final_state pc B ->
          exists t : tid,
            Etr np_step np_abort final_state ({-|pc, t}) B /\ pc_valid_tid pc t.

  Lemma np_p_refine_weak {NL}{L}:
    forall P,
      wd_langs (fst P)->
      safe_prog P->
      drf P->
      @np_p_prog_refine_weak NL L P.
  Lemma DRF_NP_Refine_Config_Proof:
    forall NL L mu su tu e sgm sge spc st tgm tge tpc tt,
      @wd_langs NL L su ->
      @wd_langs NL L tu ->
      (forall t : tid, DRFLemmas.pc_valid_tid tpc t -> np_safe_config ({-|tpc, t})) ->
      InitRel mu sge tge sgm tgm->
      init_config (su,e) sgm sge spc st->
      init_config (tu,e) tgm tge tpc tt->
      drf (su,e)->
      drfpc tpc->
      np_prog_refine (su,e)(tu,e)->
      config_refine tpc spc.

  Definition np_p_equiv {NL}{L} (p: prog L):=
    forall m ge pc t,
      @init_config NL L p m ge pc t ->
      forall B,
        Etr glob_step abort final_state pc B <-> exists t, Etr np_step np_abort final_state ({-|pc,t}) B /\ pc_valid_tid pc t.
  Lemma NP_P_Equiv{NL}{L}:
    forall P,
      wd_langs (fst P)->
      safe_prog P->
      drf P->
      @np_p_equiv NL L P.

End Refinement.